Verification of Infinite State Systems Based on Finite Automata

Název v češtině:Verifikace nekonečně stavových systémů založená na konečných automatech
Hlavní řešitel:Holík Lukáš
Další řešitelé:Lengál Ondřej
Agentura:Grantová agentura České republiky - Postdoktorandské granty
Kód:GP13-37876P
Zahájení:2013-02-01
Ukončení:2015-12-31
Klíčová slova:
formální verifikace
nekonečně stavové systémy
programy s ukazateli
programy manipulující řetězce
symbolická reprezentace
regulární model checking
konečné automaty
jazyková inkluze
minimalizace
relace simulace
Anotace:
Projekt je zaměřen na formální verifikaci programů s nekonečnými stavovými prostory, zvláště pak na programy s dynamicky alokovanými ukazatelovými strukturami a programy manipulující řetězce neohraničené délky. Verifikační nástroje pro obě třídy programů jsou žádoucí. Programy s ukazateli jsou notoricky náchylné k výskytům těžko odhalitelných chyb, programy s řetězci jsou jádrem webových aplikací, kde chyba snadno vede ke kritickým bezpečnostním rizikům. Projekt staví na metodách využívajících konečné automaty jako prostředek symbolické reprezentace nekonečných množin stavů. V souvislosti s tím budeme také vyvíjet technologii umožňující využití nedeterministických konečných automatů v praxi, zejména algoritmy pro testování jazykové inkluze, minimalizaci, a rozhodovací procedury logik MSO a WSkS. Práce na projektu bude vedena rigorózními matematickými metodami a bude zahrnovat implementaci a experimentální vyhodnocení navržených technik a algoritmů.

Produkty

2015dWiNA - Implementace rozhodovací procedury pro WS1S, software, 2015
Autoři: Fiedor Tomáš, Lengál Ondřej, Holík Lukáš, Vojnar Tomáš

Publikace

2017ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt a REZINE Ahmed. An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures. International Journal on Software Tools for Technology Transfer. 2017, roč. 5, č. 19, s. 549-563. ISSN 1433-2779.
2016HAZIZA Frédéric, HOLÍK Lukáš, MEYER Roland a WOLF Sebastian. Pointer Race Freedom. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin: Springer Verlag, 2016, s. 393-412. ISBN 978-3-662-49121-8.
 HOLÍK Lukáš, MEYER Roland a MUSKALLA Sebastian. Antichains for the Verification of Recursive Programs. In: Proceedings of International Conference on Networked Systems. Cham: Springer International Publishing, 2016, s. 322-336. ISBN 978-3-319-26849-1.
2015ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed, RUMMER Philipp a STENMAN Jari. Norn: An SMT Solver for String Constraints. In: Computer Aided Verification. Cham: Springer International Publishing, 2015, s. 462-469. ISBN 978-3-319-21689-8.
 ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer. 2015, roč. 2016, č. 5, s. 495-516. ISSN 1433-2779.
 ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. View Abstraction - A Tutorial. In: 2nd International Workshop on Synthesis of Complex Parameters. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015, s. 1-15. ISBN 978-3-939897-82-8.
 ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica. 2015, roč. 53, č. 4, s. 357-385. ISSN 0001-5903.
 FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, s. 658-674. ISBN 978-3-662-46680-3.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, s. 431-434. ISBN 978-3-662-46680-3.
 HOLÍK Lukáš, ISBERNER Malte a JONSSON Bengt. Mediator Synthesis in a Component Algebra with Data. In: Correct System Design. Berlin: Springer Verlag, 2015, s. 238-259. ISBN 978-3-319-23505-9.
2014ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, RUMMER Philipp a STENMAN Jari. String Constraints for Verification. In: 26th International Conference on Computer Aided Verification. Berlin: Springer Verlag, 2014, s. 150-166. ISBN 978-3-319-08866-2.
 ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science. Paris: Elsevier Science, 2014, roč. 2014, č. 552, s. 26-43. ISSN 0304-3975.
2013ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Fakulta informačních technologií VUT v Brně, 2013.
 ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, s. 224-239. ISBN 978-3-319-02443-1.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Fakulta informačních technologií VUT v Brně, 2013.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, s. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.

Vaše IPv4 adresa: 34.237.75.18
Přepnout na https