ChorGram is a tool for choreographic design of message-passing systems. ChorGram is based on g-choreographies and communicating finite-state machines. ChorGram supports top-down and bottom-up development, choreographic testing. It will be soon extended with support for QoS analysis. GSSI & ISTI are also working on integrating Contract Automata in ChorGram.
Available here
Website here
Contact.
The Contract Automata Toolkit is a set of tools for contract automata. It currently features the Contract Automata Library (CATLib), the Contract Automata App (CATApp) and the Contract Automata Runtime Environment (CARE). CATLib is the main repository and implements contract automata and their operations, e.g., composition and synthesis. CATApp is a GUI front-end and CARE is a runtime environment for realising service applications specified using contract automata.
Available here
Website here
Contact.
Lazy-CSeq is a context-bounded verification tool (developed within the CSeq framework) for sequentially consistent C programs using POSIX threads. It handles an extensive fragment of the C language and the main parts of the POSIX thread API, such as dynamic thread creation and deletion, and synchronization via thread join, locks, and condition variables. It supports assertion checking and deadlock detection, and returns counterexamples in case of errors. Lazy-CSeq has won several times the concurrency category of SV-COMP."
Available here
Contact.
VoxLogicA: the Voxel-based Logical Analyser. VoxLogicA is a model checker dedicated to classifying pixels/voxels in 2D/3D images, based on their spatial logical properties, such as proximity, distance, reachability, texture, colour, etc.
Available here
Website here
Contact.