Project Details

Metody a nástroje pro automatizované odhalování softwarových chyb

Project Period: 1. 1. 2006 - 31. 12. 2008

Project Type: grant

Code: GP102/06/P076

Agency: Czech Science Foundation

Program:

English title
Methods and Tools for Automated Bug Detection in Software
Type
grant
Keywords

Formal analysis and verification, software, Java, Object-Oriented Petri Nets

Abstract

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.

Team members
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT) , research leader
Publications

2008

  • LETKO Zdeněk, VOJNAR Tomáš and KŘENA Bohuslav. AtomRace: data race and atomicity violation detector and healer. In: PADTAD '08. Proceedings of the 6th workshop on Parallel and distributed systems. Seattle: Association for Computing Machinery, 2008, pp. 1-10. ISBN 978-1-60558-052-4. Detail
  • BRAIONE Pietro, DENARO Giovanni, PEZZE Mauro and KŘENA Bohuslav. Verifying LTL Properties of Bytecode with Symbolic Execution. In: Bytecode 2008. Budapest: Elsevier Science, 2008, pp. 1-14. ISSN 1571-0661. Detail

2007

  • KŘENA Bohuslav, LETKO Zdeněk, TZOREF-BRILL Rachel, UR Shmuel and VOJNAR Tomáš. 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, pp. 54-64. ISBN 978-1-59593-734-6. Detail
  • DUDKA Vendula, KŘENA Bohuslav and VOJNAR Tomáš. 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, pp. 67-73. ISBN 978-80-7355-077-6. Detail

2006

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

2008

  • Java Atomicity Violation Detector & Healer, software, 2008
    Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav Detail
  • Model checking Using Symbolic Execution, software, 2008
    Authors: Křena Bohuslav, Braione Pietro, Denaro Giovanni, Pezze Mauro Detail

2007

  • Java Race Detector & Healer, software, 2007
    Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav Detail
Back to top