Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Selected SMT-based model checking methods

2014/15/N/ST6/05079

Keywords:

model checking multi-agent systems real-time systems modal logics SMT-solvers

Descriptors:

  • ST6_4: Formal methods, foundations of computer science, including theoretical computer science, quantum algorithms

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Akademia im. Jana Długosza w Częstochowie, Wydział Matematyczno-Przyrodniczy

woj. śląskie

Other projects carried out by the institution 

Principal investigator (from the host institution):

Agnieszka Zbrzezny 

Number of co-investigators in the project: 2

Call: PRELUDIUM 8 - announced on 2014-09-15

Amount awarded: 99 560 PLN

Project start date (Y-m-d): 2015-07-13

Project end date (Y-m-d): 2017-07-12

Project duration:: 24 months (the same as in the proposal)

Project status: Project settled

Equipment purchased [PL]

  1. Komputer przenośny (5 000 PLN)

Information in the final report

  • Publication in academic press/journals (5)
  • Articles in post-conference publications (12)
  1. COMPARING SAT- AND SMT- BASED BOUNDED MODEL CHECKING FOR ECTL PROPERTIES
    Authors:
    AGNIESZKA M. ZBRZEZNY
    Academic press:
    Scientific Issues Jan Długosz University in Częstochowa Mathematics (rok: 2017, tom: 22, strony: ), Wydawca: Akademia im. Jana Długosza
    Status:
    Submitted
  2. SMT-based reachability analysis for Simply-Timed Systems
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Academic press:
    SCIENTIFIC ISSUES JAN DŁUGOSZ UNIVERSITY in CZĘSTOCHOWA MATHEMATICS (rok: 2015, tom: 20, strony: 83-92), Wydawca: Akademia im. Jana Długosza
    Status:
    Published
    DOI:
    10.16926/m.2015.20.09 - link to the publication
  3. A comparison of SMT-solvers for timed weighted interpreted systems
    Authors:
    Agnieszka M. Zbrzezny
    Academic press:
    SCIENTIFIC ISSUES JAN DŁUGOSZ UNIVERSITY in CZĘSTOCHOWA MATHEMATICS (rok: 2016, tom: 21, strony: 189-206), Wydawca: Akademia im. Jana Długosza
    Status:
    Published
    DOI:
    10.16926/m.2016.21.15 - link to the publication
  4. SMT-based Searching for k-quasi-optimal Runs in Weighted Timed Automata.
    Authors:
    Bożena Woźna-Szcześniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Academic press:
    Fundamenta Informaticae (rok: 2017, tom: 152(4), strony: 411-433), Wydawca: IOS Press
    Status:
    Published
    DOI:
    10.3233/FI-2017-1527 - link to the publication
  5. Comparing SAT-based bounded model checking RTECTL and ECTL properties
    Authors:
    Agnieszka M. Zbrzezny
    Academic press:
    Technical Sciences (rok: 2017, tom: 20(2), strony: ), Wydawca: Uniwersytet Warmińsko-Mazurski
    Status:
    Accepted for publication
  1. SAT-Versus SMT-Based BMC for TWIS and the Existential Fragment of WCTL with Knowledge
    Authors:
    Agnieszka M. Zbrzezny
    Conference:
    Agent and Multi-Agent Systems: Technology and Applications, 11th KES International Conference, KES-AMSTA 2017 (rok: 2017, ), Wydawca: Springer
    Data:
    konferencja 21-23.06.2017
    Status:
    Published
  2. Simple Bounded MTLK Model Checking for Timed Interpreted Systems
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    Agent and Multi-Agent Systems: Technology and Applications, 11th KES International Conference, KES-AMSTA 2017 (rok: 2017, ), Wydawca: Springer
    Data:
    konferencja 21-23.06.2017
    Status:
    Published
  3. Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    PRIMA 2016: Princiles and Practice of Multi-Agent Systems - 19th International Conference, Phuket, Thailand (rok: 2016, ), Wydawca: Springer
    Data:
    konferencja 22-26.08.2016
    Status:
    Published
  4. SMT-based Searching for k-quasi-optimal Runs in Weighted Timed Automata
    Authors:
    Bożena Woźna-Szczesniak, Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    CS&P 2015 Concurrency, Specification and Programming (rok: 2015, ), Wydawca: CEUR Workshop Proceedings
    Data:
    konferencja 28-30.09.2015
    Status:
    Published
  5. Simple SMT-Based Bounded Model Checking for Timed Interpreted Systems.
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    INTERNATIONAL JOINT CONFERENCE ON ROUGH SETS (rok: 2017, ), Wydawca: Springer
    Data:
    konferencja 03-07.07.2017
    Status:
    Published
  6. Checking WECTLK Properties of TRWISs via SMT-based Bounded Model Checking
    Authors:
    Agnieszka M. Zbrzezny and Andrzej Zbrzezny
    Conference:
    2015 Imperial College Computing Student Workshop (ICCSW 2015) (rok: 2015, ), Wydawca: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 24-25.09.2015
    Status:
    Published
  7. Checking WELTLK Properties of Weighted Interpreted Systems via SMT-Based Bounded Model Checking
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    PRIMA 2016: Princiles and Practice of Multi-Agent Systems - 18th International Conference, Bertinoro, Italy (rok: 2015, ), Wydawca: Springer
    Data:
    konferencja 26-30.10.2015
    Status:
    Published
  8. Verifying Properties of Multi-aget Systems via Bounded Model Checking
    Authors:
    Agnieszka M. Zbrzezny
    Conference:
    The 14th Pacific Rim International Conference on Artificial Intelligence (PRICAI Workshop 2016), Phuket, Thailand (rok: 2016, ), Wydawca: Prince of Songkla University (PSU, Thailand) Artificial Intelligence Association of Thailand (AIAT)
    Data:
    konferencja 22-26.08.2016
    Status:
    Published
  9. Checking WECTLK properties of timed real-weighted interpreted systems via SMT-based bounded model checking
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    17th Portuguese Conference on Artificial Intelligence, EPIA 2015, Coimbra, Portugal (rok: 2015, ), Wydawca: Springer International Publishing
    Data:
    konferencja 8-11.09.2015
    Status:
    Published
  10. Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny, Franco Raimondi
    Conference:
    The 10th KES International Conference, KES-AMSTA 2016, Puerto de la Cruz, Tenerife (rok: 2016, ), Wydawca: Springer
    Data:
    konferencja 15-17.06.2016
    Status:
    Published
  11. Simple Bounded MTL Model Checking for Discrete Timed Automata (extended abstract)
    Authors:
    Agnieszka M. Zbrzezny, Andrzej Zbrzezny
    Conference:
    the 25th International Workshop on Concurrency, Specification and Programming Rostock, Germany (rok: 2016, ), Wydawca: CEUR Workshop Proceedings
    Data:
    konferencja 28-30.09.2016
    Status:
    Published
  12. SMT-Based Bounded Model Checking for Weighted Epistemic ECTL
    Authors:
    Agnieszka M. Zbrzezny, Bożena Woźna-Szcześniak, Andrzej Zbrzezny
    Conference:
    17th Portuguese Conference on Artificial Intelligence, EPIA 2015, Coimbra, Portugal (rok: 2015, ), Wydawca: Springer International Publishing
    Data:
    konferencja 8-11.09.2015
    Status:
    Published