Automated logical veri cation based on traceabstractionsNils Klarlund Mogens

We propose a new and practical framework for integrating the behav-ioral 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 speciication. We show that for nite-state systems such symbolic abstractions can be speciied conveniently in Monadic Second-Order Logic (M2L). Model-checking is then made possible by the reduction of non-determinism implied by the trace abstraction. Our method has been applied to a recent veriication problem by Broy and Lamport. We have transcribed their behavioral description of a distributed program into temporal logic and veriied it against another distributed system without constructing the global program state space. The reasoning is expressed entirely within M2L and is carried out by a decision procedure. Thus M2L is a practical vehicle for handling complex temporal logic speciications, where formulas decided by a push of a button are as long as 10-15 pages.