research
∙
06/15/2023
Counterfactuals Modulo Temporal Logics
Lewis' theory of counterfactuals is the foundation of many contemporary ...
share
research
∙
05/29/2023
Second-Order Hyperproperties
We introduce Hyper^2LTL, a temporal logic for the specification of hyper...
research
∙
03/26/2023
Automata-Based Software Model Checking of Hyperproperties
We develop model checking algorithms for Temporal Stream Logic (TSL) and...
research
∙
03/02/2023
Iterative Circuit Repair Against Formal Specifications
We present a deep learning approach for repairing sequential circuits ag...
research
∙
01/26/2023
AutoHyper: Explicit-State Model Checking for HyperLTL
HyperLTL is a temporal logic that can express hyperproperties, i.e., pro...
research
∙
01/17/2023
Bounded Model Checking for Asynchronous Hyperproperties
Many types of attacks on confidentiality stem from the nondeterministic ...
research
∙
10/04/2022
Synthesizing Dominant Strategies for Liveness (Full Version)
Reactive synthesis automatically derives a strategy that satisfies a giv...
research
∙
08/15/2022
Smart Contract Synthesis Modulo Hyperproperties
Smart contracts are small but highly security-critical programs that imp...
research
∙
06/07/2022
Software Verification of Hyperproperties Beyond k-Safety
Temporal hyperproperties are system properties that relate multiple exec...
research
∙
06/04/2022
Explaining Hyperproperty Violations
Hyperproperties relate multiple computation traces to each other. Model ...
research
∙
06/04/2022
Formal Specifications from Natural Language
We study the generalization abilities of language models when translatin...
research
∙
06/03/2022
Prophecy Variables for Hyperproperty Verification
Temporal logics for hyperproperties like HyperLTL use trace quantifiers ...
research
∙
06/01/2022
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
We report on the last four editions of the reactive synthesis competitio...
research
∙
05/30/2022
Attention Flows for General Transformers
In this paper, we study the computation of how much an input token in a ...
research
∙
05/30/2022
Deciding Hyperproperties Combined with Functional Specifications
We study satisfiability for HyperLTL with a ∀^*∃^* quantifier prefix, kn...
research
∙
05/24/2022
Information Flow Guided Synthesis (Full Version)
Compositional synthesis relies on the discovery of assumptions, i.e., re...
research
∙
05/12/2022
Reactive Synthesis of Smart Contract Control Flows
Smart contracts are small but highly error-prone programs that implement...
research
∙
03/14/2022
A Logic for Hyperproperties in Multi-Agent Systems
Hyperproperties are commonly used in computer security to define informa...
research
∙
03/08/2022
Runtime Enforcement of Hyperproperties
An enforcement mechanism monitors a reactive system for undesired behavi...
research
∙
11/09/2021
RTLola on Board: Testing Real Driving Emissions on your Phone
This paper is about shipping runtime verification to the masses. It pres...
research
∙
08/08/2021
Visual Analysis of Hyperproperties for Understanding Model Checking Results
Model checkers provide algorithms for proving that a mathematical model ...
research
∙
07/25/2021
Neural Circuit Synthesis from Specification Patterns
We train hierarchical Transformers on the task of synthesizing hardware ...
research
∙
07/25/2021
Model Checking Algorithms for Hyperproperties
Hyperproperties generalize trace properties by expressing relations betw...
research
∙
07/20/2021
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory
In the synthesis of distributed systems, we automate the development of ...
research
∙
07/06/2021
A Temporal Logic for Strategic Hyperproperties
Hyperproperties are commonly used in computer security to define informa...
research
∙
07/02/2021
Live Synthesis
Synthesis automatically constructs an implementation that satisfies a gi...
research
∙
06/28/2021
Compositional Synthesis of Modular Systems (Full Version)
Given the advances in reactive synthesis, it is a natural next step to c...
research
∙
05/29/2021
Causality-Based Game Solving
We present a causality-based algorithm for solving two-player reachabili...
research
∙
04/30/2021
Temporal Stream Logic modulo Theories
Temporal Stream Logic (TSL) is a temporal logic that extends LTL with up...
research
∙
04/28/2021
A Temporal Logic for Asynchronous Hyperproperties
Hyperproperties are properties of computational systems that require mor...
research
∙
03/15/2021
Specification Decomposition for Reactive Synthesis (Full Version)
Reactive synthesis is the task of automatically deriving an implementati...
research
∙
01/19/2021
Controller Synthesis for Hyperproperties
We investigate the problem of controller synthesis for hyperproperties s...
research
∙
01/19/2021
Program Repair for Hyperproperties
We study the repair problem for hyperproperties specified in the tempora...
research
∙
01/19/2021
The Complexity of Monitoring Hyperproperties
We study the runtime verification of hyperproperties, expressed in the t...
research
∙
01/18/2021
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
We present Syntroids, a case study for the automatic synthesis of hardwa...
research
∙
01/18/2021
Realizing Omega-regular Hyperproperties
We studied the hyperlogic HyperQPTL, which combines the concepts of trac...
research
∙
01/18/2021
Efficient Monitoring of Hyperproperties using Prefix Trees
Hyperproperties, such as non-interference and observational determinism,...
research
∙
12/29/2020
Synthesizing Approximate Implementations for Unrealizable Specifications
The unrealizability of a specification is often due to the assumption th...
research
∙
12/29/2020
Approximate Automata for Omega-Regular Languages
Automata over infinite words, also known as omega-automata, play a key r...
research
∙
12/29/2020
Canonical Representations of k-Safety Hyperproperties
Hyperproperties elevate the traditional view of trace properties form se...
research
∙
12/29/2020
Explainable Reactive Synthesis
Reactive synthesis transforms a specification of a reactive system, give...
research
∙
12/15/2020
Verified Rust Monitors for Lola Specifications
The safety of cyber-physical systems rests on the correctness of their m...
research
∙
10/07/2020
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
We study the expressivity and the model checking problem of linear tempo...
research
∙
07/14/2020
Model Checking Branching Properties on Petri Nets with Transits (Full Version)
To model check concurrent systems, it is convenient to distinguish betwe...
research
∙
07/14/2020
Dependency-based Compositional Synthesis (Full Version)
Despite many recent advances, reactive synthesis is still not really a p...
research
∙
05/15/2020
Verifying Hyperliveness
HyperLTL is an extension of linear-time temporal logic for the specifica...
research
∙
05/14/2020
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)
The correctness of networks is often described in terms of the individua...
research
∙
05/12/2020
The Hierarchy of Hyperlogics
Hyperproperties, which generalize trace properties by relating multiple ...
research
∙
05/07/2020
Probabilistic Hyperproperties of Markov Decision Processes
We study the specification and verification of hyperproperties for proba...
research
∙
03/27/2020
