Detail projektu
Metody a nástroje pro automatizované odhalování softwarových chyb
Období řešení: 1. 1. 2006 – 31. 12. 2008
Typ projektu: grant
Kód: GP102/06/P076
Agentura: Grantová agentura České republiky
Program: Postdoktorandské granty
Formální analýza a verifikace, software, Java, objektově orientované Petriho
sítě
Tento projekt spadá do oblasti analýzy a verifikace softwaru, která je dlouhodobě
aktuálním výzkumným tématem, protože na správnost a spolehlivost softwaru jsou
vzhledem k jeho dnešnímu rozšíření prakticky do všech oblastí lidské činnosti
kladeny značné požadavky. Prvním cílem projektu je pomocí případové studie
zhodnotit a porovnat aktuálně dostupné nástroje pro automatickou detekci chyb
v softwaru. Jako případová studie bude použita některá případová studie
z projektu SegraVis nebo bude vybrána z oblasti open-source software. Na základě
výsledků této případové studie pak budou programové nástroje, do jejichž vývoje
je navrhovatel zapojen (tedy nástroje založené na objektove orientovaných Petriho
sítích dlouhodobe vyvíjené na pracovišti navrhovatele a nástroje založené na
symbolickém provádení Java programu, které jsou vyvíjeny na univerzite
Miláno-Bicocca), rozvíjeny směrem k jejich lepší využitelnosti v praxi.
Pokračování současné intenzivní spolupráce navrhovatele se zahraničním týmem je
dalším významným přínosem tohoto projektu.
2008
- BRAIONE, P.; DENARO, G.; PEZZE, M.; KŘENA, B. Verifying LTL Properties of Bytecode with Symbolic Execution. Bytecode 2008. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. Budapest: Elsevier Science, 2008.
p. 1-14. ISSN: 1571-0661. Detail - LETKO, Z.; VOJNAR, T.; KŘENA, B. AtomRace: Data Race and Atomicity Violation Detector and Healer. PADTAD '08. Proceedings of the 6th workshop on Parallel and distributed systems. Seattle: Association for Computing Machinery, 2008.
p. 1-10. ISBN: 978-1-60558-052-4. Detail
2007
- DUDKA, V.; KŘENA, B.; VOJNAR, T. Using JavaPathFinder for Self-healing Assurance. Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007. Znojmo: Ing. Zdeněk Novotný, CSc., 2007.
p. 67-73. ISBN: 978-80-7355-077-6. Detail - KŘENA, B.; LETKO, Z.; TZOREF-BRILL, R.; UR, S.; VOJNAR, T. Healing Data Races On-The-Fly. Proceedings of 5th International Workshop on Parallel and Distributed Systems: Testing and Debugging Modelling - PADTAD'07. London: Association for Computing Machinery, 2007.
p. 54-64. ISBN: 978-1-59593-734-6. Detail
2006
- KŘENA, B. Computer Go as a Verification Case Study. Proceedings of XXVIIIth International Autumn Colloquium ASIS 2006: Advanced Simulation of Systems. Ostrava: 2006.
p. 95-100. ISBN: 80-86840-26-3. Detail
2008
- MUSE - model checking s využitím symbolického provádění, software, 2008
Autoři: KŘENA, B.; BRAIONE, P.; DENARO, G.; PEZZE, M. - Nástroj pro detekci a opravu chyb v atomicitě programů, software, 2008
Autoři: LETKO, Z.; VOJNAR, T.; KŘENA, B.
2007
- Nástroj pro detekci a opravu časově závislých chyb v Javě, software, 2007
Autoři: LETKO, Z.; VOJNAR, T.; KŘENA, B.