research
∙
07/13/2023
Retroactive Parametrized Monitoring
In online monitoring, we first synthesize a monitor from a formal specif...
share
research
∙
02/09/2023
Improving Blockchain Scalability with the Setchain Data-type
Blockchain technologies are facing a scalability challenge, which must b...
research
∙
02/01/2023
Decentralized Stream Runtime Verification for Timed Asynchronous Networks
We study the problem of monitoring distributed systems where computers c...
research
∙
01/17/2023
Bounded Model Checking for Asynchronous Hyperproperties
Many types of attacks on confidentiality stem from the nondeterministic ...
research
∙
01/15/2023
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Bounded model checking (BMC) is an effective technique for hunting bugs ...
research
∙
07/14/2022
Multi: a Formal Playground for Multi-Smart Contract Interaction
Blockchains are maintained by a network of participants that run algorit...
research
∙
07/12/2022
Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions
Runtime Verification deals with the question of whether a run of a syste...
research
∙
07/06/2022
Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
Hyperproperties are properties of systems that relate different executio...
research
∙
07/06/2022
Transaction Monitoring of Smart Contracts
Blockchains are modern distributed systems that provide decentralized fi...
research
∙
06/23/2022
Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers
Blockchain technologies are facing a scalability challenge, which must b...
research
∙
06/03/2022
A Tableau Method for the Realizability and Synthesis of Reactive Safety Specifications
We introduce a tableau decision method for deciding realizability of spe...
research
∙
09/21/2021
HyperQube: A QBF-Based Bounded Model Checker for Hyperproperties
This paper presents HyperQube, a push-button QBF-based bounded model che...
research
∙
04/28/2021
A Temporal Logic for Asynchronous Hyperproperties
Hyperproperties are properties of computational systems that require mor...
research
∙
04/26/2021
Asynchronous Extensions of HyperLTL
Hyperproperties are a modern specification paradigm that extends trace p...
research
∙
09/18/2020
Bounded Model Checking for Hyperproperties
This paper introduces the first bounded model checking (BMC) algorithm f...
research
∙
05/15/2020
Verifying Hyperliveness
HyperLTL is an extension of linear-time temporal logic for the specifica...
research
∙
02/28/2020
Declarative Stream Runtime Verification (hLola)
Stream Runtime Verification is a formal dynamic analysis technique that ...
research
∙
07/10/2019
Runtime Verification For Timed Event Streams With Partial Information
Runtime Verification (RV) studies how to analyze execution traces of a s...
research
∙
06/20/2019
Gray-box Monitoring of Hyperproperties (Extended Version)
Many important system properties, particularly in security and privacy, ...
research
∙
02/11/2019
COST Action IC 1402 ArVI: Runtime Verification Beyond Monitoring -- Activity Report of Working Group 1
This report presents the activities of the first working group of the CO...
research
∙
11/16/2018
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
Runtime verification is an area of formal methods that studies the dynam...
research
∙
02/28/2018