Logic and Software Verification

Anatol Slissenko and Daniele Beauquier

University Paris 12

In this talk we will give arguments why logic is not only useful for the verification but even indispensable to do it. We will focus on the verification of real-time reactive systems where continuous time is a particular feature. Realization of logic approaches to the verification poses some new questions: how to describe semantics of programs in a way efficient for logical treatment, how to seek verification proofs and how to extend the verification proofs when refining and implementing initial high-level specifications. Algorithmic questions arising when developing our logic framework will be also discussed.