Project detail

Methods and Tools for Automated Bug Detection in Software

Duration: 01.01.2006 — 31.12.2008

Funding resources

Czech Science Foundation - Postdoktorandské granty

- whole funder (2006-01-01 - 2008-12-31)

On the project

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.

Description in English
This project belongs to the area of software analysis and verification which is currently a very important and live research area. Correctness of software is nowadays crucial as software is widely used  in many safety critical roles. The first goal of this project is to use a real-life software case study for evaluating and comparing currently available tools for automated detection of bugs in software. The case study will be taken from the case studies available within the project SegraVis or from the open-source software community. Consequently, based on the results obtained from the case study, we will improve our currently developed tools (i.e., the tools associated with the formalism of Object-Oriented Petri Nets which has been developed at applicant's home faculty since 1996, and tools based on symbolic execution of Java byte-code which are developed at the University Milano-Bicocca) to be more useful in practice. Another significant benefit of this project is allowing the applicant to continue his intensive cooperation with the foreign research team.

Keywords
Formální analýza a verifikace, software, Java, objektově orientované Petriho sítě

Key words in English
Formal analysis and verification, software, Java, Object-Oriented Petri Nets

Mark

GP102/06/P076

Default language

Czech

People responsible

Křena Bohuslav, Ing., Ph.D. - principal person responsible

Units

Department of Intelligent Systems
- co-beneficiary (2006-01-01 - 2008-12-31)

Results

KŘENA, B. Computer Go as a Verification Case Study. In Proceedings of XXVIIIth International Autumn Colloquium ASIS 2006: Advanced Simulation of Systems. Ostrava: 2006. p. 95-100. ISBN: 80-86840-26-3.
Detail

HRUBÁ, V.; KŘENA, B.; VOJNAR, T. Using JavaPathFinder for Self-healing Assurance. In 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. In 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

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

LETKO, Z.; VOJNAR, T.; KŘENA, B.: JRDH; Java Race Detector & Healer. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/. URL: https://www.fit.vut.cz/research/product/49/. (software)
Detail

LETKO, Z.; VOJNAR, T.; KŘENA, B.: JRDH-AT; Java Atomicity Violation Detector & Healer. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/racedetect/. URL: https://www.fit.vut.cz/research/product/90/. (software)
Detail

KŘENA, B.; BRAIONE, P.; DENARO, G.; PEZZE, M.: MUSE; Model checking Using Symbolic Execution. http://www.fit.vutbr.cz/research/groups/verifit/tools/muse/. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/muse/. (software)
Detail

Responsibility: Křena Bohuslav, Ing., Ph.D.