We are holding the 3rd seminar in this traveling seminar series at Heriot-Watt university just outside Edinburgh. This page gives details of how to get to the venue and the programme for the afternoon.
Room 2.33,
Department of computing and
Electrical Engineering,
Mountbatten Building, Heriot-Watt
University,
Riccarton, Edinburgh.
| 14:00: | Welcome | |
| 14:10-14:40: | "Hoare Logic and VDM: Mechanising Soundness and Completeness Proofs." Thomas Schreiber (University of Edinburgh) | |
| 14:50-15:20: | "On the Automatic Discovery of Loop Invariants." Andrew Ireland (Heriot-Watt University) | |
| 15:30: | Coffee and Tea | |
| 16:00-16:30: | "Generation of invariants for finite-state automata using gap graphs." Julian Richardson (University of Edinburgh) | |
| 16:40 | Close | |
We present a technique for automating the discovery of loop invariants based upon the analysis of failed proof attempts. Previously we have shown how failure analysis may be used productively in the search for inductive proofs. This work had direct application to the verification of functional programs. Here we show how these ideas can also play an important role in the formal verification of imperative programs. While presented as an automatic technique we believe that our approach may be easily integrated within an interactive proof environment.
Finite state automata with counters are useful for modeling systems with discrete parameters. The calculation of state invariants is an important tool for the analysis of such systems. Previous authors have presented techniques for the calculation of state invariants based on their approximation by convex polyhedra or periodic sets.
I will present a method for the calculation of invariants for finite state automata with counters, based on their representation by gap-order constraints. This method differs from previous approaches by exploiting existing techniques for the calculation of least fixed points. The use of least fixed points reduces the need for approximation and allows the generation of non-convex invariants. The initial inputs to the automaton do not need to specified, but can be left as uninstantiated parameters, or partially specified using gap-order constraints. The method not only provides a new tool for program analysis, but is also an interesting application of logic programming techniques.
Employing operational semantics, one can succinctly axiomatise the behaviour of imperative programs. However, it is not feasible to reason about the correctness of real programs on the level of states. Verification calculi such as Hoare logic and VDM are better suited for this task. Instead of states, they focus on predicates and relations on states.
Unfortunately, when considering more interesting language features such as local variables, recursive procedures, parameter passing, exceptions,... it is well known that many proposed verification calculi are unsound or incomplete despite authors backing up claims to the contrary by "proofs".
Are theorem provers suitable for research in verification frameworks?
| Return to Scottish Theorem Proving page. |