Automated Reasoning for Software Verification

 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.