Automated Reasoning for Software Verification

Relatore:  Viktor Kuncak - School of Computer and Communication Sciences Ecole Polytechnique Federale de Lausanne
  martedì 17 giugno 2008 alle ore 16.15 Inizio alle 16:30, Caffè e biscotti alle 16:15.

 I will present our software verification system, Jahob, which we used to prove the correctness of imperative Java data structures such as array list, association list, binary search tree, circular list, hash table, priority queue, and space subdivision tree.  I will describe our automated reasoner for expressive constraints that made this verification effort possible.  I will then describe new automated reasoning procedures that can be used in such verification tasks: 1) a decision procedure for constraints on collections of objects in the presence of the cardinality operator, and the related 2) decision procedure for integer linear arithmetic with a 'star' operator.

Ca' Vignal - Piramide, Piano 0, Sala Verde

Maria Paola Bonacina

Referente esterno
Data pubblicazione
28 gennaio 2008

Offerta formativa