Automated Analysis and Verification Research Group - VeriFIT

2019

Trau: SMT solver for string constraints, software
Authors: Abdulla Parosh A., Atig Mohamed F., Bui Phi Diep, Holík Lukáš, Chen Yu-Fang, Rezine Ahmed, Rummer Philipp

VeriFIT Static Analysis Plugins, software
Authors: Marcin Vladimír, Harmim Dominik, Pavela Ondřej, Vojnar Tomáš, Fiedor Tomáš, Rogalewicz Adam

2018

MINA: A Tool for Verification of Programs with an Unbounded Number of Threads, software
Authors: Holík Lukáš, Turoňová Lenka, Vojnar Tomáš

Ranger: A Tool for Bounds Analysis of Heap-Manipulating Programs, software
Authors: Fiedor Tomáš, Holík Lukáš, Rogalewicz Adam, Sinn Moritz, Vojnar Tomáš, Zuleger Florian

Sloth: An SMT Solver for String Constraints, software
Authors: Holík Lukáš, Janků Petr, Lin Anthony W., Rummer Philipp, Vojnar Tomáš

2017

Gaston - Symbolic WS1S Solver, software
Authors: Fiedor Tomáš, Holík Lukáš, Janků Petr, Lengál Ondřej, Vojnar Tomáš

2015

dWiNA - An Implementation of Decision Procedure for WS1S, software
Authors: Fiedor Tomáš, Lengál Ondřej, Holík Lukáš, Vojnar Tomáš

INCLUDER (tracer): Trace Inclusion for Data Word Automata, software
Authors: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš

Norn: An SMT Solver for String Constraints, software
Authors: Abdulla Parosh A., Atig Mohamed F., Holík Lukáš, Chen Yu-Fang, Rezine Ahmed, Stenman Jari

2014

HADES (Hazard Detection System), software
Authors: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš

SLIDE: Separation Logic with Inductive Definitions, software
Authors: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš

SPEN - A Solver for Separation Logic Entailments, software
Authors: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš

2013

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs, software
Authors: Müller Petr, Vojnar Tomáš

2012

ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, software
Authors: Fiedor Jan, Vojnar Tomáš

HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, software
Authors: Zachariášová Marcela, Lengál Ondřej, Kajan Michal

VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, software
Authors: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš

2011

A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, software
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Vojnar Tomáš

2010

An Easy to Use Infrastructure for Building Static Analysis Tools, software
Authors: Dudka Kamil, Peringer Petr, Vojnar Tomáš

Forester: A Tool for Verification of Programs with Pointers, software
Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš

Framework for Formal Verification of Clock Domain Crossing, software
Authors: Smrčka Aleš, Vojnar Tomáš

libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software
Authors: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš

Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, software
Authors: Dudka Kamil, Peringer Petr, Vojnar Tomáš

Replay Tracer & BMC, software
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš

Search-based Testing Environment (SearchBestie), software
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav

Tool for verification of systems described using the Modechart formalism, software
Authors: Gach Marek, Fiedor Jan, Češka Milan

Tool for verification of systems specified in RT-Logic language, software
Authors: Fiedor Jan, Gach Marek, Češka Milan

2009

Clock Domain Crossing Analyzer, software
Authors: Smrčka Aleš

FAST to ARMC Translator, software
Authors: Smrčka Aleš

FLATA, software
Authors: Konečný Filip, Vojnar Tomáš, Bozga Marius, Iosif Radu

Tool for Computing Simulations, software
Authors: Holík Lukáš, Šimáček Jiří, Vojnar Tomáš

2008

Java Atomicity Violation Detector & Healer, software
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav

Model checking Using Symbolic Execution, software
Authors: Křena Bohuslav, Braione Pietro, Denaro Giovanni, Pezze Mauro

2007

ARTMC - Abstract Regular Tree Model Checking, software
Authors: Rogalewicz Adam, Vojnar Tomáš

Java Race Detector & Healer, software
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav

Translator of VHDL Design to Counter Automaton, software
Authors: Smrčka Aleš, Vojnar Tomáš