HomePublicationsPhD Thesis

Towards Certified Program Logics for the Verification of Imperative Programs
Ref: CISTER-TR-130408       Publication Date: 2013

Abstract:
Modern proof assistants are mature tools with which several important mathematical problems were proved correct, and which are also being used as a support for the development of program logics libraries that can be used to certify software developments. Using the Coq proof assistant we have formalised a library for regular languages, which contains a sound and complete procedure for deciding the equivalence of regular expressions. We also formalised a library for the language theoretical model of Kleene algebra with tests, the algebraic system that considers regular expressions extended with Boolean tests and that is particularly suited to the verification of imperative programs. Also using the Coq proof assistant, we have developed a library for reasoning about shared- variable parallel programs in the context of Rely-Guarantee reasoning. This library includes a sound proof system, and can be used to prove the partial correctness of simple parallel programs. The goal of the work presented in this dissertation is to contribute to the set of available libraries that help performing program verification tasks relying in the trusted base provided by the safety of the Coq proof system.

David Pereira

Document:

View
PDF Download
PDF