Tools to make formal models


The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.


mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.

The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.

TLA+ Proof System

The TLA+ Proof System (TLAPS) is a platform for computerized verification of TLA+ proofs using formal reasoning systems such as automated theorem provers, proof-assistants, SMT/SAT solvers, and decision procedures. TLA+ is a specification language designed for concurrent, distributed, reactive and real-time systems, but it can also be used to formalize any discrete algorithm. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various “backend” verifiers. The current release of TLAPS handles just enough temporal reasoning to check safety properties; an extension to the full TLA+ language is under active development.


ProofPoweris a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. The suite comprises the following packages:

  • PPDev * The ProofPowerdeveloper kit, mainly comprising SLRP, a parser generator for Standard ML.
  • PPTex * The ProofPowerinterface to TeXand LaTeX.
  • PPXpp - The X Windows/Motif front-end for ProofPower.
  • PPHol - The HOL specification and proof development system.
  • PPZed - The Z specification and proof development system.
  • PPDaz - The Compliance Tool for specifying and verifying Ada programs.

All the ProofPowerpackages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License.

ProofPowerhas been under ongoing development since 1989. It was originally designed and implemented by International Computers Ltd. to support proofs of specification-to-model correspondence for high-assurance secure systems. It has since played an important role in approaches to specifying and verifying safety-critical systems in work by the Defence and Evaluation Research Agency, now QinetiQ, and others. Since 1997, on-going developments to the product have been undertaken by Lemma 1 Ltd. In Spring 2000, International Computers Ltd. transferred its rights in ProofPowerto Lemma 1 Ltd who now maintain this web site and support and distribute the software.


K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program. Computations extend the original language abstract syntax. K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions or call/cc.


Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Supported provers: Alt-Ergo, Z3, CVC3, Yices 1, Simplify, Gappa, Coq


Focal (formerly known as FoC) is a language for software-proof codesign. In Focal, code, specifications, and proofs are developped together in the same source files, using a novel object-oriented module system. The compiler analyses the dependencies in order to ensure the consistency of the source, then translates the code to Objective Caml, and the proofs to Coq.


The FoCaLizedevelopment effort started in 2006: it was clearly a continuation of the Focand Focal efforts. The new system was rewritten from scratch. A new language and syntax was designed and carefully implemented, with in mind ease of use, expressivity, and programmer friendyness. The addition of powerful data structure definitions together with the corresponding pattern matching facility, lead to new expressing power.

The Zenon automatic theorem prover was also integrated in the compiler and natively interfaced within the FoCaLizelanguage. New developments for recursive functions support is on the way (in particular for termination proofs).

A formal specification can be built by declaring names of functions and values and introducing properties. Then, design and implementation can incrementally be done by adding definitions of functions and proving that the implementation meets the specification or design requirements. Thus, developing in FoCaLizeis a kind of refinement process from formal model to design and code, completely done within FoCaLize. Taking the global development in consideration within the same environment brings some conciseness, helps documentation and reviewing. Thus a FoCaLizedevelopment is organised as a hierarchy that may have several roots. The upper levels of the hierarchy are built along the specification stage while the lower ones correspond to implementation and each node of the hierarchy corresponds to a progress toward a complete implementation.

The FoCaLizesystem provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation while proving that such an implementation meets its specification or design requirements. The FoCaLizelanguage offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically done relies on formal proof verification. FoCaLizealso provides some automation of documentation production and management.


Boogie is an Intermediate Verification Language (IVL) for describing proof obligations to be discharged by a reasoning engine, typically an SMT solver. The language is especially suitable when the proof obligations arise in the context of programs with control flow and imperative state. The intermediate language is easy to target from source languages such as C# or C. Boogie is also a verification engine that takes the Boogie language as input, generates verification conditions (VCs) for the proof obligations, and passes the VCs to a reasoning engine. In the Boogie pipeline, there is room for various Boogie-to-Boogie transforms that either encode certain features (like parallelism) or make the checking more effective or efficient.

Rodin environment for Event B

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.

The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.


ProR is a tool for requirements engineering that supports the ReqIF 1.0.1 Standard natively. It is part of the Eclipse RMF project and is built for extensibility. ProR is the result of the European Union FP7 Research Project Deploy, where it is used to provide traceability between requirements and formal models.


To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems.

The heart of SAL is a language, developed in collaboration with Stanford and Berkeley, for specifying concurrent systems in a compositional way. It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental “Witness” model checker, and a unique “infinite” bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator.

CPN Tools

CPN Tools is a tool for editing, simulating, and analyzing Colored Petri nets.

The tool features incremental syntax checking and code generation, which take place while a net is being constructed. A fast simulator efficiently handles untimed and timed nets. Full and partial state spaces can be generated and analyzed, and a standard state space report contains information, such as boundedness properties and liveness properties.

formal_models_environments.txt · Dernière modification: Le 17/10/2013 à 11:05 par david_mentre     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó