Verified Systems International GmbH
Quality Assurance for Embedded Systems
Quality Assurance for Embedded Systems
We present an algorithmic framework that allows on-line monitoring of past-time MTL specifications in a discrete time…
This paper introduces Arcade.PLC, a verification platform for programmable logic controllers (PLCs). The tool supports…
Access-based localization is a two-step process. First, the set of abstract memory locations that are accessed in a…
Bitwise instructions, loops and indirect data access present challenges to the verification of microcontroller programs.…
This white-paper reports on benchmark measurements performed for the alternative model-checking backends of the contract…
Loop leaping is the colloquial name given to a form of program analysis in which summaries are derived for nested loops…
Recently it has been shown how transfer functions for linear template constraints can be derived for bit-vector programs…