First Munich-Nancy Workshop on
Decision Procedures for Theorem Provers


This workshop is the kick-off meeting in a collaborative project between the groups of Stephan Merz at INRIA Lorraine and Tobias Nipkow at TUM. The focus of this collaboration is the integration of decision procedures and theorem provers with an emphasis on applications to system verification.


March 6 & 7, 2006


TU München, Fakultät für Informatik, Room 00.09.055 (Alan Turing)



Monday, 9.15 Organizational Meeting
Monday, 10.00 John Matthews: "System Verification at Galois Connections"
Monday, 11.30 Stephan Merz: "Interfacing Isabelle/HOL and haRVey"
Tjark Weber: "Integrating a SAT Solver with Isabelle/HOL"
Pascal Fontaine: "The SMT solver haRVey"
Monday, 13.00 Lunch
Monday, 14.00 Discussion
Monday, 15.30 Norbert Schirmer: "Software Verification in Verisoft - Integration of Automatic Tools"
Clemens Ballarin: "Maple's Evaluation Process as Constraint Contextual Rewriting"
Tuesday, 9.15 Amine Chaieb: "Verifying procedures for simple arithmetics"
Tuesday, 10.00 Discussion
Tuesday, 13.00 Lunch
Tuesday, 14.00 Discussion
Tuesday, 19.00 Dinner

 Last modified: 2006-03-10. Send e-mail to Tjark Weber for further information.