Subproject

S1

Categories

Model checker for hard & soft real-time systems

Overview

Fully symbolic backward model checker for FSMTs (finite state machine with time) based on LinAIGs. A FSMT is a symbolic representation of real time systems.

Publications

G. Morbe, F. Pigorsch, and C. Scholl. Fully Symbolic Model Checking for Timed Automata. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science (LNCS), pages 616-632, 2011.

G. Morbe and C. Scholl. Fully Symbolic Model Checking for Timed Automata. In Frank Oppenheimer, editor, 14th Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", pages 9-18, 2011.

Benchmarks

See www.informatik.uni-freiburg.de/~morbe/fsmt/

Download

Click here for the binary.

Manual

Just type ./fsmtMC on the command line to see how it can be used.

Status

Prototype