-
Article
Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories
Automatic verification of programs and computer systems with input variables represents a significant and well-motivated challenge. The case of Simulink diagrams is especially difficult, because there the inpu...
-
Chapter and Conference Paper
On Clock-Aware LTL Properties of Timed Automata
We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the...
-
Chapter and Conference Paper
LTL Model Checking of LLVM Bitcode with Symbolic Data
The correctness of parallel and reactive programs is often easier specified using formulae of temporal logics. Yet verifying that a system satisfies such specifications is more difficult than verifying safety ...
-
Chapter and Conference Paper
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs
We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement in this new release is an extension of the class of systems that may be verified with the model checker, wh...