[Club2] 14.09. 14.00-Uhr

[Norbert Schirmer]

N=E4chste Woche kommen Besucher aus Frankreich und halten einen Vortrag:

Towards a Combination of Heterogenous Deductive Tools
for System Verification

by Pascal Fontaine, Kamal Gupta, Jean-Yves Marion, Stephan Merz,
   Leonor Prensa Nieto and Alwen Tiu

Zeit: Mittwoch 14.9.; 14:00
Ort: John v. Neumann -  Zimmer 00.11.038


Abstract:

We present an ongoing work at LORIA on combining Isabelle/HOL with
different automatic deductive tools for system verification.
The main case study is the verification of distributed
algorithms, in particular the fault-tolerant clock synchronization
algorithms. We will talk about our current implementation of
interfaces between Isabelle, using the oracle facility,
with the automatic tools ICS, CVC-Lite and harVey,
and the interface with SAT solvers.
=46or the latter part, we show how to reconstruct the proof of
unsatisfiability from the SAT solver. This is done by first
transforming the formula to be proved into CNF (while generating
proofs at the same time), which is then given to the SAT solver.
The transformation is done within Isabelle, where, given a formula
phi, one gets the theorem phi =3D phi', where phi' is the CNF
formula. With the help of the proof trace produced by the SAT solver,
an Isabelle proof of the original formula is then reconstructed based
on simple resolution steps. We will also discuss several experiments
on CNF transformation and proof reconstruction to improve efficiency.

  Norbert