27 citations · 106 across the 15 of their papers we have counts for
17 papers
Reproducible Execution of POSIX Programs with DiOS
Petr Ročkai, Zuzana Baranová, Jan Mrázek +2
In this paper, we describe DiOS, a lightweight model operating system which can be used to execute programs that make use of POSIX APIs. Such executions are fully reproducible: run…
Symbolic Computation via Program Transformation
Henrich Lauko, Petr Ročkai, Jiří Barnat
Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic…
From Model Checking to Runtime Verification and Back
Katarína Kejstová, Petr Ročkai, Jiří Barnat
We describe a novel approach for adapting an existing software model checker to perform precise runtime verification. The software under test is allowed to communicate with the wid…
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking
Jan Mrázek, Martin Jonáš, Jiří Barnat
In semi-symbolic (control-explicit data-symbolic) model checking the state-space explosion problem is fought by representing sets of states by first-order formulas over the bit-vec…
DiVM: Model Checking with LLVM and Graph Memory
Petr Ročkai, Vladimír Štill, Ivana černá +1
In this paper, we introduce the concept of a virtual machine with graph-organised memory as a versatile backend for both explicit-state and abstraction-driven verification of softw…
A Simulator for LLVM Bitcode
Petr Ročkai, Jiří Barnat
In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, au…