27 citations · 71 across the 6 of their papers we have counts for
6 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…
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…
Using Off-the-Shelf Exception Support Components in C++ Verification
Vladimír Štill, Petr Ročkai, Jiří Barnat
An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex…