Projects

Coloane

Coloane is a free Eclipse based editor dedicated to systems modeling using different formalisms like Petri Nets. With Coloane you can design your models and connect them to the FrameKit platform. This platform provides you a huge set of tools you can use to verify properties on your models (i.e. "Does my model have a deadlock?")

Gappa

The Gappa tool helps developers to verify arithmetic properties on their numerical programs (either floating-point or fixed-point computations). It can also generate formal proofs of the properties for extra confidence. It has been successfully used with several projects, e.g. for writing some ... [More] robust floating-point filters of CGAL and for certifying the elementary functions of CRlibm. [Less]

Why3

Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification apart 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 ... [More] large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. [Less]

Rudder

Configuration management for the masses

PolyBoRi

PolyBoRi is implemented as a C++ library for Polynomials over Boolean Rings, which provides high-level data types for Boolean polynomials. A python-interface yields extensible algorithms for computing Groebner bases over Boolean Rings.

Sequence Chart Studio

A user-friendly drawing and verification tool for Message Sequence Charts (MSC, HMSC) and UML Sequence Diagrams. Integrated with Microsoft Visio.

Java Modeling Language (JML)

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules (as in design by contract -- DBC). It has many tools to do assertion checking, unit testing, etc.

SysFink

The unix based guard for checking consistency of system files. Sysfink server periodically scan basic information in the client's file systems and reports changes to administrator.

Whiley (Programming Language)

Whiley is a programming language particularly suited to safety-critical systems. It is a hybrid object-oriented and functional programming language which employs extended static checking to eliminate errors at compile time, including divide-by-zero, array out-of-bounds and null dereference errors.

trie-rules

A project to create tools to support the creation of correct rule bases on top of rdf triple stores. The project is still in an early stage, but you can download and try an innovative graphical debugger for rules - it works but is limited to RDF files without anonymous nodes and rules without ... [More] functors or built-ins. Rule cycles will crash it. Over time the project will grow to include a bit of formal verification, visualization and some automatic debugging support. The project is created in Java, is build on top of Eclipse and utilizes the Jena framework. We love to hear from you, in particular if you need debugging/verification tool for rules on top of RDF! Further development of this project will largely depend on whether people need such a thing! Related news and publications will be published on this Blog here. [Less]