Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

INFORMATIK 2011 Informatik schafft Communities P-192, 352-352 (2011).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Geilmann A dual-engine for early analysis of critical systems

Aboubakr Achraf El Ghazi , Mana Taghdiri , Mattias Ulbrich and Ulrich


This paper presents a framework for modeling, simulating, and checking properties of critical systems 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 using an SMT solver, which provides a better support for numerical expressions than the existing Alloy Analyzer. Proofs, however, cannot always be found automatically since the Alloy language is undecidable. Our engine offers an economical approach by first trying to prove properties using a fully-automatic, SMT-based analysis, 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.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-88579-286-4

Last changed 21.02.2014 20:08:11