Piter's Home Page

Z3 is a new high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is still under development, but it has already been integrated with Spec#/Boogie, and HAVOC. We are currently integrating Z3 with Pex, SAGE, Yogi, Vigilante, and SLAM. It can read problems in SMT-LIB and Simplify formats.

Safety properties state that “something bad never happens” (a program never enters an unacceptable state).

Liveness properties state that “something good will eventually happen” (a program eventually enters a desirable state).

Guarantees specify that an event will eventually happen but does not promise repetitions.

Obligations are disjunctions of safety and guarantee formula

Responses specify that an event will happen infinitely many times.

Persistence specifies the eventual stabilization of a system condition after an arbitrary delay.

Reactivity is the maximal class formed from the disjunction of response and persistence properties.

Unconditional Fairness states that a property p holds infinitely often.

Weak Fairness states that if a property p is continuously true then the property A must be true infinitely often.

Strong Fairness states that if a property A is true infinitely often then the property B must be true infinitely often

Classification of Formal Methods (approaches and tools) according to the types of systems they apply:

* Concurrent systems

o CCS - Calculus of Communicating Systems
o CIRCAL - CIRcuit CALculus
o Concurrency Factory
o CSP - Communicating Sequential Processes
o LOTOS - Language of Temporal Ordering Specifications
o Meije - verification of concurrent programs
o Murphi - description language and verifier tool
o Petri Nets
o Pobl - development method for concurrent object-based programs
o RAISE Method
o TLA - Temporal Logic of Actions
o VeriSoft - model checking tool

* Distributed systems

o Rapide - toolset for large-scale distributed multi-language systems
o SPIN - is an automated verification tool
o UPPAAL
o UNITY - programming notation for parallel and distributed program

* Embedded systems

o HyTech - The HYbrid TECHnology Tool

* Parallel systems

o UNITY - programming notation for parallel and distributed programs

* Reactive systems

o DisCo - specification method for reactive systems
o Esterel - Language and Tools
o LUSTRE - language for programming reactive systems
o TLA - Temporal Logic of Actions
o TTM/RTTL - framework for real-time reactive systems
o VeriSoft - model checking tool

* Real-time systems

o ACSR - Algebra of Communicating Shared Resources
o DC - Duration Calculus
o Kronos - verification tool
o PARAGON - visual specification and verification of real-time systems
o RAISE Method
o TRIO - tools for real-time systems
o TTM/RTTL - framework for real-time reactive systems
o UPPAAL - verification and validation tools for real-time systems
o VeriSoft - model checking tool

* Safety-Critical systems

o NP-Tools - framework for mathematically proving safety properties

* Sequential systems

o ACL2 - A Computational Logic for Applicative Common Lisp
o B-Method
o Boyer-Moore - Theorem Prover
o LARCH
o LOTOS - Language of Temporal Ordering Specifications
o Nqthm - Boyer-Moore theorem prover
o PVS - Prototype Verification System
o RAISE Method
o VDM - Vienna Development Method
o Z notation

* Synchronous systems

o Esterel - Language and Tools
o Signal language

“Lock” resource statement modeled and verified with UPPAAL:

lock.zip

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Spec# is pronounced “Spec sharp” and can be written (and searched for) as the “specsharp” or “Spec# programming system”. The Spec# system consists of:

• The Spec# programming language. Spec# is an extension of the object-oriented language C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.
• The Spec# compiler. Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.
• The Spec# static program verifier. This component (codenamed Boogie) generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.

A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.

Spec# Home