Abstract:

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.
(Joint work with Daniele Beauquier)