@article{Klarlund_Nielsen_Sunesen_1995, title={Automated Logical Verification based on Trace Abstractions}, volume={2}, url={https://tidsskrift.dk/brics/article/view/19954}, DOI={10.7146/brics.v2i53.19954}, abstractNote={We propose a new and practical framework for integrating the behavioral<br />reasoning about distributed systems with model-checking methods.<br />Our proof methods are based on trace abstractions, which relate the<br />behaviors of the program and the specification. We show that for finite-state<br />systems such symbolic abstractions can be specified conveniently in<br />Monadic Second-Order Logic (M2L). Model-checking is then made possible<br />by the reduction of non-determinism implied by the trace abstraction.<br />Our method has been applied to a recent verification problem by Broy<br />and Lamport. We have transcribed their behavioral description of a distributed<br />program into temporal logic and verified it against another distributed<br />system without constructing the global program state space. The<br />reasoning is expressed entirely within M2L and is carried out by a decision<br />procedure. Thus M2L is a practical vehicle for handling complex temporal<br />logic specifications, where formulas decided by a push of a button are as<br />long as 10-15 pages.}, number={53}, journal={BRICS Report Series}, author={Klarlund, Nils and Nielsen, Mogens and Sunesen, Kim}, year={1995}, month={Nov.} }