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

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. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, s. 224-239. ISBN 978-3-319-02443-1.
 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. FIT-TR-2013-02, 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.
 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.

Vaše IPv4 adresa: 54.225.47.94
Přepnout na IPv6 spojení

DNSSEC [dnssec]