Verlässliche Software für kritische Infrastrukturen at INFORMATIK 2011 - Informatik schafft Communities
Berlin 2011

Abstract: This paper presents a framework for specifying, modeling, and checking properties of critical infrastructure protocols based on the Alloy language -- a declarative, first-order, relational logic with a built-in transitive closure operator. The paper introduces a new dual-analysis engine that is capable of providing both counterexamples and proofs. Counterexamples are found fully automatically, in a more scalable fashion than by existing tools. Proofs, however, cannot always be found automatically since the Alloy language is undecidable. Our engine provides an economical analysis by first trying to prove properties using an SMT-based, fully automatic approach, and switches to an interactive theorem prover only if the first attempt fails. This paper also reports on applying our framework to Microsoft's COM standard and the mark-and-sweep garbage collection algorithm.