Combining Bisimulation and Predicate Inference for Equivalence Proofs

Forschungsthema:	Regression Verification
Typ:	MA / PdF
Datum:	2022-08-24
Betreuer:	Mattias Ulbrich
Aushang:	PDF

Background

When verifying that a program is correct, one definitely needs a description of what “correct” means and coming up with good such descriptions is a very difficult task. An alternative approach is to provide a reference implementation and to check that your optimised implementation is functionally equivalent to the reference implementation (which might for instance be taken from a text book). But formally proving program equivalence is also a hard problem – it is known to be undecidable in general.

Problem Description

Nonetheless, there exist several approaches to prove program equivalence for certain classes of input programs. At KIT, we have developed the approach “LLRêve” with which structurally similar C programs can be proved equivalent using a predicate-inference technique. Colleagues at BITS have investigated how coloured petri nets can be used to verify equivalence of C programs. Both approaches have their strengths, but also their weaknesses.

Goal

Your goal in this project is to come up with and implement a novel program equivalence verification technique that combines the two approaches. This approach will combine the flexibity in control flow synchronisation obtained from bisimulation with the flexibility of data synchronisation of LLRêve.

Requirements

You should be familiar with first order logic and program verification as taught, e.g., in the course Formale Systeme at KIT. Since we plan to collaborate with colleagues from BITS in India, you should feel confident discussing in English.

Contact

This thesis will be conducted in collaboration with Dr. A. Mathews from the Birla Institute of Technology and Science, Pilani. If you are interested, contact Mattias Ulbrich ulbrich@kit.edu.