Automated Logical Verification Based on Trace Abstractions

Nils Klarlund, Mogens Nielsen, and Kim Sunesen


We propose a practical framework for integrating the behavioral reasoning about distributed systems with model-checking methods.

Our proof methods are based on trace abstractions, which relate the behaviors of the program and the specification. We show that for finite-state systems such symbolic abstractions can be specified conveniently in a Monadic Second-Order Logic (M2L), which allows the concise expression of many temporal properties. Model-checking is then made possible by the reduction of non-determinism implied by the trace abstraction.

We outline how our method can be applied to a recent verification problem by Broy and Lamport. In an accompanying paper, we give a detailed account. The resulting complex temporal logic formulas are as long as 10-15 pages and are decided automatically within minutes.