Tenth and final Meeting
- Radu Iosif (VERIMAG)
-
Title: An Effective Calculus for the Verification of Aliasing Properties
- Abstract:
In this work we develop a deductive verification method
based on a logic that describes pointer aliasing.
The user has to annotate the program with loop invariants,
pre- and post-conditions. The annotations are then automatically
checked for validity by computing weakest preconditions in our
effectively decidable logic. We start by discussing the undecidability
of a very expressive program logic (wAL), then define a decidable
subset (pAL) that is closed under the weakest precondition operators.
For the latter logic we give two sound and complete proof systems,
one based on natural deduction system, and another based on the
effective method of analytic tableaux.
This is joint work with Marius Bozga and Yassine Lakhnech.