Automated Reasoning for Software Verification

Speaker:  Viktor Kuncak - School of Computer and Communication Sciences Ecole Polytechnique Federale de Lausanne
  Tuesday, June 17, 2008 at 4:15 PM 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, Floor 0, Hall Verde

Programme Director
Maria Paola Bonacina

Publication date
January 28, 2008