Project Details

Automates et Logique pour la vérification symbolique de logiciels

Project Period: 1. 1. 2010 – 31. 12. 2011

Project Type: grant

Code: MEB021023

Agency: Ministerstvo školství, mládeže a tělovýchovy ČR

Program: KONTAKT

English title
Automata and Logic for Symbolic Verification of Software
Czech title
Automaty a logiky v symbolické verifikaci software
Type
grant
Keywords

formal verification, infinite-state systems, symbolic representations, automata, logics

Abstract

Among techniques which can be used for verification of infinite-state systems, one can find approaches based on cut-offs, automated induction, or symbolic verification, which is probably the most frequent and which is also the subject of the proposed project. Symbolic verification is based on encoding infinite sets of states of the examined systems (possibly after some abstraction) in a finite way using some suitable formalism. Probably the most commonly used symbolic representations are those built on logics and automata.

The scientific goal of the proposed project is to significantly advance the state of the art in the area of symbolic logic-based and automata-based verification methods for infinite-state software, namely to increase the scalability of these approaches and to broaden the area of their applicability. To achieve this goal we plan to further improve the various individual logic-based as well as automata-based techniques, but also invest a significant amount of research into approaches combining advantages of both automata as well as logics. In the research, we will in particular concentrate on verification of programs with unbounded integers, (parametrised-size) arrays, and complex dynamic linked data structures.

Team members
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS) – research leader
Bozga Marius
Habermehl Peter
Konečný Filip, Ing., Ph.D.
Radu Iosif
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Publications

2012

2011

2010

Back to top