Overview Team Projects Publications Contact Back to ReleaseLab
Description Objectives Contributions Publications

Formally Verified Bug-free Implementations of (Logical) Algorithms

Soundness is presently a major challenge for programmers - the societal tolerance to software bugs and hacker infiltrations is decreasing rapidly, with prominent cases making shocking news almost daily. Surprisingly, there are effective methodologies and tools to ensure strong guarantees about the safety and the reliability of programs, as witnessed by several successful industrial cases:

The vast majority of developers, however, have little training in developing bug-free and hacker-proofed program. Moreover, most companies lack the know-how and practices to deal with these software soundness challenges. The challenging is at the same time huge and urgent. This thesis proposal is a (quite) small step to face it.

Objectives

The aim of this project is to develop formally verified functional implementations of classical logical algorithms like the Horn satisfiability. Concretely, the objective is twofold: - the functional implementation of classical logical algorithms as showcases of clean and clear code close to specifications; - the development of correctness proofs of the implementations as showcases of the feasibility and usability of machine-checked program proof systems.

Expected Contributions

A suitcase of functional implementations of classical logical algorithms, with pedagogical value because they will illustrate how close the code is to the mathematical specification and how readable the code is; correctness proofs of the implementations that will also serve as pedagogical examples and showcases of the effort required and of the usability of the proof-assistance platforms to machine-check programs; scientific papers presenting the work developed.

Publications

NOVA-LINCS / ReleaseLab