Category: Publications

Real-Time Runtime Verification on Chip

We present an algorithmic framework that allows on-line monitoring of past-time MTL specifications in a discrete time setting. The algorithms allow to be synthesized into efficient observer hardware blocks, which take advantage of the highly-parallel nature of hardware designs. For

ArcadePLC: A Verification Platform for Programmable Logic Controllers

This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports static analysis as well as ACTL and past-time LTL model checking using counterexample-guided abstraction refinement for different programming languages used in industry. In the underlying

Access-Based Localization for Octagons

Access-based localization is a two-step process. First, the set of abstract memory locations that are accessed in a procedure are determined. Then, in a subsequent fixed point iteration, the input to the respective procedure is reduced to those variables that

Abstract Interpretation of Microcontroller Code: Intervals Meet Congruences

Bitwise instructions, loops and indirect data access present challenges to the verification of microcontroller programs. In particular, since registers are often memory mapped, it is necessary to show that an indirect store operation does not accidently mutate a register. To

Benchmark Analysis of GTL-Backends using Client-Server Mutex

This white-paper reports on benchmark measurements performed for the alternative model-checking backends of the contract specification language GTL. The GTL has been developed in context of the VerSyKo project. The considered backends are the model-checking tools SPIN and UPPAAL. The

Loop Leaping with Closures

Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops starting from the innermost loop and proceeding in a bottom-up fashion considering one more loop at a time. Loop

Transfer Function Synthesis without Quantifier Elimination

Recently it has been shown how transfer functions for linear template constraints can be derived for bit-vector programs by operating over propositional Boolean formulae. The drawback of this method is that it relies on existential quantifier elimination, which induces a computational bottleneck. The