Software

ClabureDB

It can serve as a tool for tuning and valuation of miscellaneous program analysis tools. The software contains bug-reports produced by various tools applied to various source codes. The bug-reports are classified as either real errors or false positives. The software currently contains more than 800 bug-reports detected in the Linux kernel 2.6.28, almost 300 reports from Software Competition 2012 and over 2000 reports from Software Competition 2013. Support of other software projects written in various programming languages is planned.

Detailed information can be found on the project homepage.

Contact: Jiri Slaby and Marek Trtík

COBRA - the COde-BReaking game Analyzer

COBRA is a tool for modeling and solving deductive (or codebreaking) games. Deductive games are played by two players, the codemaker and the codebreaker, where the codemaker selects a secret code and the codebreaker strives to discover this code using a minimal number of allowed experiments that reveal some partial information about the code. Using COBRA, one can compute optimal strategies and ranking strategies for selected ranking functions, and simulate plays based on the computed strategies.

Detailed information can be found on the project homepage.

Contact: Miroslav Klimoš and Antonín Kučera

SCStudio - Sequence Chart Studio

SCStudio (Sequence Chart Studio) is a user-friendly drawing and verification tool for Message Sequence Charts. It provides several verification algorithms and offers an open interface for additional modules. The graphical front-end is implemented as a Microsoft Visio add-on, but integration with other applications is possible.

Detailed information can be found on the project homepage.

Contact: Vojtěch Řehák

Stanse

The aim of this project is to research, evaluate and implement modern approaches to automatic bug finding for programs written in procedural languages related to C (C/C++/C#/Java). The goal is to create a software tool which is able to automatically discover some types of bugs in real-life sized projects (e.g. the Linux kernel).

Detailed information can be found on the project homepage.

Contact: Jiri Slaby and Marek Trtík

Symbiotic

Symbiotic is a tool implementing a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs.

Detailed information can be found on the project homepage.

Contact: Jiri Slaby and Marek Trtík

software.txt · Last modified: 2014/10/23 13:32 by Antonin Kucera