Decision procedures for verification of computer systems

Relatore
Dr. Calogero G. Zarba - REACT Group, Universitaet des Saarlandes
Data e ora
martedì 21 novembre 2006 alle ore 17.30 - caffè, tè & C. ore 17.00
Luogo
Ca' Vignal - Piramide, Piano 0, Sala Verde
Referente
Maria Paola Bonacina
Referente esterno
Data pubblicazione
12 ottobre 2006
Dipartimento
 

Riassunto

Safety-critical computer systems are used more and more inside aircrafts, trains, cars, and other artifacts whose failure can endanger human life.
The rigorous mathematical analysis and verification of safety-critical computer systems ultimately relies on the availability of robust, general, and fast decision procedures for logical theories modelling simple data types (such as integer, reals, and bit-vectors), functional data structures (such as lists, arrays, sets, multisets, and graphs), and pointer-based data structures (such as linked lists and binary search trees).
In this talk we describe how decision procedures are used in the verification of safety-critical computer systems. Furthermore, we present a general algorithm that can decide the satisfiability of every quantifier-free verification condition spanning over simple data types, functional data structures, and pointer-based data structures. This algorithm is based on the eager approach to decision procedures: the verification condition to be checked for satisfiability is converted into an equisatisfiable propositional formula, which can be sent to a state-of-the-art BDD package or SAT solver.





© 2002 - 2021  Università degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234