-
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...
-
Article
Analysing sanity of requirements for avionics systems
In the last decade it became a common practice to formalise software requirements to improve the clarity of users’ expectations. In this work we build on the fact that functional requirements can be expressed ...
-
Chapter and Conference Paper
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration
We present SymDIVINE: a tool for bit-precise model checking of parallel C and C++ programs. It builds upon LLVM compiler infrastructure, hence, it uses LLVM IR as an input formalism. Internally, SymDIVINE extends...
-
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
Checking Sanity of Software Requirements
In the last decade it became a common practice to formalise software requirements to improve the clarity of users’ expectations. In this work we build on the fact that functional requirements can be expressed ...
