Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Frontiers of automatic verification: new methods of analysis of infinite-state systems

2013/09/B/ST6/01575

Keywords:

infinite-state systems form verification reachability problem equivalence problem bisimulation equivalence

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 :

Uniwersytet Warszawski, Wydział Matematyki, Informatyki i Mechaniki

woj. mazowieckie

Other projects carried out by the institution 

Principal investigator (from the host institution):

dr hab. Sławomir Lasota 

Number of co-investigators in the project: 5

Call: OPUS 5 - announced on 2013-03-15

Amount awarded: 409 100 PLN

Project start date (Y-m-d): 2014-03-20

Project end date (Y-m-d): 2017-03-19

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

Project status: Project settled

Equipment purchased [PL]

  1. Baterie do komputerów przenośnych (3 szt.) (1 500 PLN)
  2. Monitory (2 szt.) (3 550 PLN)
  3. Komputery przenośne (3 szt.) (18 522 PLN)

Information in the final report

  • Publication in academic press/journals (4)
  • Articles in post-conference publications (10)
  1. Incremental Test Case Generation Using Bounded Model Checking: an Application to Automatic Rating
    Authors:
    G. Anielak, G. Jakacki, S. Lasota
    Academic press:
    International Journal on Software Tools for Technology Transfer (rok: 2015, tom: 17, strony: 339-349), Wydawca: Springer
    Status:
    Published
    DOI:
    10.1007/s10009-014-0317-2 - link to the publication
  2. Simulation Problems Over One-Counter Nets
    Authors:
    Piotr Hofman, Sławomir Lasota, Richard Mayr, Patrick Totzke
    Academic press:
    Logical Methods in Computer Science (rok: 2016, tom: 12, strony: 16803), Wydawca: Logical Methods in Computer Science e.V.
    Status:
    Published
    DOI:
    10.2168/LMCS-12(1:6)2016 - link to the publication
  3. Undecidability of performance equivalence of Petri nets
    Authors:
    Sławomir Lasota, Marcin Poturalski
    Academic press:
    Theoretical Computer Science (rok: 2016, tom: 655, part B, strony: 109-119), Wydawca: Elsevier
    Status:
    Published
    DOI:
    10.1016/j.tcs.2016.01.034 - link to the publication
  4. Copyless cost-register automata: Structure, expressiveness, and closure properties
    Authors:
    Filip Mazowiecki, Cristian Riveros
    Academic press:
    Journal of Computer and System Sciences (rok: 2019, tom: 100, strony: 45320), Wydawca: Elsevier
    Status:
    Published
    DOI:
    10.1016/j.jcss.2018.07.002 - link to the publication
  1. Reachability Analysis of First-order Definable Pushdown Systems
    Authors:
    Lorenzo Clemente, Sławomir Lasota
    Conference:
    24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (rok: 2015, ), Wydawca: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 7-10.09.2015
    Status:
    Published
  2. Copyless Cost-Register Automata: Structure, Expressiveness, and Closure Properties
    Authors:
    Filip Mazowiecki, Cristian Riveros
    Conference:
    33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016) (rok: 2016, ), Wydawca: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 17-20.02.2016
    Status:
    Published
  3. Coverability Trees for Petri Nets with Unordered Data
    Authors:
    Piotr Hofman, Sławomir Lasota, Ranko Lazic, Jerome Leroux, Sylvain Schmitz, Patrick Totzke
    Conference:
    FOSSACS 2016 (rok: 2016, ), Wydawca: Springer
    Data:
    konferencja 2-8.04.2016
    Status:
    Published
  4. Ordered Tree-Pushdown Systems
    Authors:
    Lorenzo Clemente, Pawel Parys, Sylvain Salvati, Igor Walukiewicz
    Conference:
    35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) (rok: 2015, ), Wydawca: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 16-18.12.2015
    Status:
    Published
  5. Separability of Reachability Sets of Vector Addition Systems
    Authors:
    Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, Charles Paperman
    Conference:
    34th Symposium on Theoretical Aspects of Computer Science (STACS 2017) (rok: 2017, ), Wydawca: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 8-11.03.2017
    Status:
    Published
  6. Timed pushdown automata revisited
    Authors:
    Lorenzo Clemente, Sławomir Lasota
    Conference:
    Thirtieth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS) (rok: 2015, ), Wydawca: IEEE
    Data:
    konferencja 6-10.07.2015
    Status:
    Published
  7. Branching Bisimilarity of Normed BPA Processes is in NEXPTIME
    Authors:
    Wojciech Czerwiński, Petr Jančar
    Conference:
    LICS'2015 (rok: 2015, ), Wydawca: ACM/IEEE
    Data:
    konferencja 7,2015
    Status:
    Published
  8. Shortest paths in one-counter systems
    Authors:
    Dmitry Chistikov, Wojciech Czerwinski, Piotr Hofman, Michal Pilipczuk, Michael Wehar
    Conference:
    FOSSACS 2016 (rok: 2016, ), Wydawca: Springer
    Data:
    konferencja 2-8.04.2016
    Status:
    Published
  9. The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
    Authors:
    Lorenzo Clemente, Paweł Parys, Sylvain Salvati, Igor Walukiewicz
    Conference:
    LICS'2016 (rok: 2016, ), Wydawca: ACM/IEEE
    Data:
    konferencja 7,2016
    Status:
    Published
  10. Trace Inclusion for One-Counter Nets Revisited
    Authors:
    Piotr Hofman, Patrick Totzke
    Conference:
    Reachability Problems 2014 (rok: 2014, ), Wydawca: Springer
    Data:
    konferencja 9,2014
    Status:
    Published