Languages

Automated Theorem Proving in Building High-confidence Software

strict warning: Only variables should be passed by reference in /var/www/drupal/modules/book/book.module on line 559.

 
 

Tony Hoare proposed Hoare logic as a formal system which has axioms and inference rules for all the constructs of a simple imperative programming language. It oriented program verification and researchers have developed rules for other language constructs ever since.
 
Typically verification conditions will be generated according Hoare logic rules. If they are valid, the verification will terminate successfully. So to make such a formal verification system into practice, theorem proving is the key technique in building high-confidence software by program verification. There are two aspects to evaluate a theorem prover. One is the expressivity that the logic it supports, the other is that the automaticity.
 
There are many state-of-the-art theorem provers. The proof assistant Coq supports high order logic but need human interaction. The benefits are the proof terms that can be used in building proof-carrying code. Z3 of Microsoft Research is a typical automated theorem prover. But it only reports Yes/No with no solid proof term.


Fig 1. A Typical Theorem Prover
 
Our research goal of this project is that to study the techniques of automated theorem proving in building high-confidence software with proof terms output. Currently the following researches are carrying on:

  • An automated theorem prover for integer arithmetic based on Simplex algorithm It outputs proof terms which can be checked by Coq.
  • An automated theorem prover for fragment of separation logic.
  • Techniques on theory combination in building multi-theory-support theorem prover.

 This project tightly relates with our certifying compiler project (namely CComp). in our laboratory. These results and tools will be used directly in CComp.
 The future work is to research on generation of theorem prover based on the experiences of this project. It will be a core part as the generation techniques of certifying compilers.