Automated logical verification based on trace abstractions

Abstract

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 [11], we give a detailed account. The resulting complex temporal logic formulas are as long as 10-15 pages and are decided automatically within minutes.