Projekty finansowane przez NCN


Dane kierownika projektu i jednostki realizującej

Szczegółowe informacje o projekcie i konkursie

Słowa kluczowe

Aparatura

Wyczyść formularz

Granice automatycznej weryfikacji: nowe metody analizy systemów nieskończenie stanowych

2013/09/B/ST6/01575

Słowa kluczowe:

systemy nieskończenie stanowe weryfikacja formalna problem osiągalności problem równoważności równoważność bisymulacyjna

Deskryptory:

  • ST6_4: Metody formalne, teoretyczne podstawy informatyki w tym informatyka teoretyczna

Panel:

ST6 - Informatyka i technologie informacyjne: technologie i systemy informacyjne, informatyka, obliczenia naukowe, systemy inteligentne

Jednostka realizująca:

Uniwersytet Warszawski, Wydział Matematyki, Informatyki i Mechaniki

woj. mazowieckie

Inne projekty tej jednostki 

Kierownik projektu (z jednostki realizującej):

dr hab. Sławomir Lasota 

Liczba wykonawców projektu: 5

Konkurs: OPUS 5 - ogłoszony 2013-03-15

Przyznana kwota: 409 100 PLN

Rozpoczęcie projektu: 2014-03-20

Zakończenie projektu: 2017-03-19

Planowany czas trwania projektu: 36 miesięcy (z wniosku)

Status projektu: Projekt rozliczony

Zakupiona aparatura

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

Dane z raportu końcowego/rocznego

  • Publikacje w czasopismach (4)
  • Teksty w publikacjach pokonferencyjnych (10)
  1. Incremental Test Case Generation Using Bounded Model Checking: an Application to Automatic Rating
    Autorzy:
    G. Anielak, G. Jakacki, S. Lasota
    Czasopismo:
    International Journal on Software Tools for Technology Transfer (rok: 2015, tom: 17, strony: 339-349), Wydawca: Springer
    Status:
    Opublikowana
    Doi:
    10.1007/s10009-014-0317-2 - link do publikacji
  2. Simulation Problems Over One-Counter Nets
    Autorzy:
    Piotr Hofman, Sławomir Lasota, Richard Mayr, Patrick Totzke
    Czasopismo:
    Logical Methods in Computer Science (rok: 2016, tom: 12, strony: 16803), Wydawca: Logical Methods in Computer Science e.V.
    Status:
    Opublikowana
    Doi:
    10.2168/LMCS-12(1:6)2016 - link do publikacji
  3. Undecidability of performance equivalence of Petri nets
    Autorzy:
    Sławomir Lasota, Marcin Poturalski
    Czasopismo:
    Theoretical Computer Science (rok: 2016, tom: 655, part B, strony: 109-119), Wydawca: Elsevier
    Status:
    Opublikowana
    Doi:
    10.1016/j.tcs.2016.01.034 - link do publikacji
  4. Copyless cost-register automata: Structure, expressiveness, and closure properties
    Autorzy:
    Filip Mazowiecki, Cristian Riveros
    Czasopismo:
    Journal of Computer and System Sciences (rok: 2019, tom: 100, strony: 45320), Wydawca: Elsevier
    Status:
    Opublikowana
    Doi:
    10.1016/j.jcss.2018.07.002 - link do publikacji
  1. Reachability Analysis of First-order Definable Pushdown Systems
    Autorzy:
    Lorenzo Clemente, Sławomir Lasota
    Konferencja:
    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:
    Opublikowana
  2. Copyless Cost-Register Automata: Structure, Expressiveness, and Closure Properties
    Autorzy:
    Filip Mazowiecki, Cristian Riveros
    Konferencja:
    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:
    Opublikowana
  3. Coverability Trees for Petri Nets with Unordered Data
    Autorzy:
    Piotr Hofman, Sławomir Lasota, Ranko Lazic, Jerome Leroux, Sylvain Schmitz, Patrick Totzke
    Konferencja:
    FOSSACS 2016 (rok: 2016, ), Wydawca: Springer
    Data:
    konferencja 2-8.04.2016
    Status:
    Opublikowana
  4. Ordered Tree-Pushdown Systems
    Autorzy:
    Lorenzo Clemente, Pawel Parys, Sylvain Salvati, Igor Walukiewicz
    Konferencja:
    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:
    Opublikowana
  5. Separability of Reachability Sets of Vector Addition Systems
    Autorzy:
    Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, Charles Paperman
    Konferencja:
    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:
    Opublikowana
  6. Timed pushdown automata revisited
    Autorzy:
    Lorenzo Clemente, Sławomir Lasota
    Konferencja:
    Thirtieth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS) (rok: 2015, ), Wydawca: IEEE
    Data:
    konferencja 6-10.07.2015
    Status:
    Opublikowana
  7. Branching Bisimilarity of Normed BPA Processes is in NEXPTIME
    Autorzy:
    Wojciech Czerwiński, Petr Jančar
    Konferencja:
    LICS'2015 (rok: 2015, ), Wydawca: ACM/IEEE
    Data:
    konferencja 7,2015
    Status:
    Opublikowana
  8. Shortest paths in one-counter systems
    Autorzy:
    Dmitry Chistikov, Wojciech Czerwinski, Piotr Hofman, Michal Pilipczuk, Michael Wehar
    Konferencja:
    FOSSACS 2016 (rok: 2016, ), Wydawca: Springer
    Data:
    konferencja 2-8.04.2016
    Status:
    Opublikowana
  9. The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
    Autorzy:
    Lorenzo Clemente, Paweł Parys, Sylvain Salvati, Igor Walukiewicz
    Konferencja:
    LICS'2016 (rok: 2016, ), Wydawca: ACM/IEEE
    Data:
    konferencja 7,2016
    Status:
    Opublikowana
  10. Trace Inclusion for One-Counter Nets Revisited
    Autorzy:
    Piotr Hofman, Patrick Totzke
    Konferencja:
    Reachability Problems 2014 (rok: 2014, ), Wydawca: Springer
    Data:
    konferencja 9,2014
    Status:
    Opublikowana