6 papers · 1 filter
Pacing Types for Asynchronous Stream Equations
Florian Kohn, Arthur Correnson, Jan Baumeister +1
Stream-based monitoring is a runtime verification approach where a monitor aggregates streams of input data from sensors and other sources to give real-time statistics and assessme…
A Deductive System for Contract Satisfaction Proofs
Arthur Correnson, Haoyi Zeng, Jana Hofmann
Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without…
Pacing Types: Safe Monitoring of Asynchronous Streams
Florian Kohn, Arthur Correnson, Jan Baumeister +1
Stream-based monitoring is a real-time safety assurance mechanism for complex cyber-physical systems such as unmanned aerial vehicles. In this context, a monitor aggregates streams…
Coinductive Proofs for Temporal Hyperliveness
Arthur Correnson, Bernd Finkbeiner
Temporal logics for hyperproperties have recently emerged as an expressive specification technique for relational properties of reactive systems. While the model checking problem f…
Finding Hyperbugs using Symbolic Execution
Arthur Correnson, Tobias Niessen, Bernd Finkbeiner +1
Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of hyperproperties and require, for each execution trace o…
Engineering a Formally Verified Automated Bug Finder
Arthur Correnson, Dominic Steinhoefel
Symbolic execution is a program analysis technique executing programs with symbolic instead of concrete inputs. This principle allows for exploring many program paths at once. Desp…