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.