Detail projektu
Verification of Infinite State Systems Based on Finite Automata
Období řešení: 1. 2. 2013 – 31. 12. 2015
Typ projektu: grant
Kód: GP13-37876P
Agentura: Grantová agentura České republiky
Program: Postdoktorandské granty
formální verifikacenekonečně stavové systémyprogramy s ukazateliprogramy
manipulující řetězcesymbolická reprezentaceregulární model checkingkonečné
automatyjazyková inkluzeminimalizacerelace simulace
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ů.
2017
- HOLÍK, L.; ABDULLA, P.; HAZIZA, F.; JONSSON, B.; REZINE, A. 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, vol. 5, no. 19,
p. 549-563. ISSN: 1433-2779. Detail
2016
- HOLÍK, L.; MEYER, R.; MUSKALLA, S. Antichains for the Verification of Recursive Programs. In Proceedings of International Conference on Networked Systems. Lecture Notes in Computer Science (LNCS). Cham: Springer International Publishing, 2016.
p. 322-336. ISBN: 978-3-319-26849-1. Detail - HOLÍK, L.; MEYER, R.; WOLF, S.; HAZIZA, F. Pointer Race Freedom. In Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Berlin: Springer Verlag, 2016.
p. 393-412. ISBN: 978-3-662-49121-8. Detail
2015
- FIEDOR, T.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Nested Antichains for WS1S. In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015.
p. 658-674. ISBN: 978-3-662-46680-3. Detail - HOLÍK, L.; ABDULLA, P.; HAZIZA, F. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer, 2015, vol. 2016, no. 5,
p. 495-516. ISSN: 1433-2779. Detail - HOLÍK, L.; HAZIZA, F.; ABDULLA, P. View Abstraction - A Tutorial. In 2nd International Workshop on Synthesis of Complex Parameters. OpenAccess Series in Informatics (OASIcs). OpenAccess Series in Informatics. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015.
p. 1-15. ISBN: 978-3-939897-82-8. ISSN: 2190-6807. Detail - HOLÍK, L.; CHEN, Y.; REZINE, A.; RUMMER, P.; STENMAN, J.; ABDULLA, P.; ATIG, M. Norn: An SMT Solver for String Constraints. In Computer Aided Verification. Lecture Notes in Computer Science Volume 9206. Cham: Springer International Publishing, 2015.
p. 462-469. ISBN: 978-3-319-21689-8. Detail - HOLÍK, L.; ISBERNER, M.; JONSSON, B. Mediator Synthesis in a Component Algebra with Data. In Correct System Design. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2015.
p. 238-259. ISBN: 978-3-319-23505-9. Detail - HOLÍK, L.; LENGÁL, O.; VOJNAR, T.; JONSSON, B.; TRINH, Q.; ABDULLA, P. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica, 2015, vol. 53, no. 4,
p. 357-385. ISSN: 0001-5903. Detail - HRUŠKA, M.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.; HOLÍK, L.; ROGALEWICZ, A. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015.
p. 432-435. ISBN: 978-3-662-46680-3. Detail
2014
- ABDULLA, P.; HAZIZA, F.; HOLÍK, L. Block Me If You Can! Context-Sensitive Parameterized Verification. In 21st International Static Analysis Symposium. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2014.
p. 1-17. ISBN: 978-3-319-10935-0. ISSN: 0302-9743. Detail - HOLÍK, L.; ABDULLA, P.; ATIG, M.; CHEN, Y.; RUMMER, P.; STENMAN, J. String Constraints for Verification. In 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Volume 8559. Berlin: Springer Verlag, 2014.
p. 150-166. ISBN: 978-3-319-08866-2. Detail - HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science, 2014, vol. 2014, no. 552,
p. 26-43. ISSN: 0304-3975. Detail
2013
- HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013.
p. 1-35. Detail - HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013.
p. 224-239. ISBN: 978-3-319-02443-1. Detail - HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013.
p. 1-25. Detail - HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. Proceedings of CAV'13. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2013.
p. 740-755. ISBN: 978-3-642-39798-1. ISSN: 0302-9743. Detail
2015
- dWiNA - Implementace rozhodovací procedury pro WS1S, software, 2015
Autoři: FIEDOR, T.; LENGÁL, O.; HOLÍK, L.; VOJNAR, T.