Write a Blog >>
Thu 22 Nov 2018 16:05 - 16:30 at Boothzaal - 3 Chair(s): Robbert Krebbers

First-order theorem provers based on superposition, such as E, SPASS, and Vampire, play an important role in formal software verification. They are based on sophisticated logical calculi that combine ordered resolution and equality reasoning. They also employ advanced algorithms, data structures, and heuristics.

As a step towards verifying the correctness of state-of-the-art provers, we specify, using the Isabelle/HOL proof assistant, a purely functional ordered resolution prover and formally establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract specification of a nondeterministic prover, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.

(See http://matryoshka.gforge.inria.fr/pubs/fun_rp_paper.pdf for details.)

Thu 22 Nov

15:40 - 17:20: PLNL - 3 at Boothzaal
Chair(s): Robbert KrebbersDelft University of Technology
plnl-2018-papers15:40 - 16:05
Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel, Belgium
plnl-2018-papers16:05 - 16:30
Anders SchlichtkrullTechnical University of Denmark, Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich
plnl-2018-papers16:30 - 16:55
Alen ArslanagićUniversity of Groningen
plnl-2018-papers16:55 - 17:20
Alejandro SerranoUtrecht University, Netherlands