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
- Clemens Ballarin
- Stefan Berghofer
- Amine Chaieb
- Pascal Fontaine
- John Matthews
- Stephan Merz
- Leonor Prensa Nieto
- Tobias Nipkow
- Stéphane Riedweg
- Norbert Schirmer
- Tjark Weber
- Makarius Wenzel
|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, 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"|