48 citations · 362 across the 28 of their papers we have counts for
32 papers
Learning Broadcast Protocols
Dana Fisman, Noa Izsak, Swen Jacobs
The problem of learning a computational model from examples has been receiving growing attention. For the particularly challenging problem of learning models of distributed systems…
Automatic and Incremental Repair for Speculative Information Leaks
Joachim Bard, Swen Jacobs, Yakir Vizel
We present CureSpec, the first model-checking based framework for automatic repair of programs with respect to information leaks in the presence of side-channels and speculative ex…
Parameterized Verification of Disjunctive Timed Networks
Étienne André, Paul Eichler, Swen Jacobs +1
We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards tha…
The Temporal Logic Synthesis Format TLSF v1.2
Swen Jacobs, Guillermo A. Perez, Philipp Schlehuber-Caissier
We present an extension of the Temporal Logic Synthesis Format (TLSF). TLSF builds on standard LTL, but additionally supports high-level constructs, such as sets and functions, as…
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification (Extended Version)
Nouraldin Jaber, Christopher Wagner, Swen Jacobs +2
Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While…
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Perez, Remco Abraham +22
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Th…
Automatic Repair and Deadlock Detection for Parameterized Systems
Swen Jacobs, Mouhammad Sakr, Marcus Völp
We present an algorithm for the repair of parameterized systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property i…
Validation of Abstract Side-Channel Models for Computer Architectures
Hamed Nemati, Pablo Buiras, Andreas Lindner +2
Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to vali…
Parameterized Verification of Systems with Global Synchronization and Guards
Nouraldin Jaber, Swen Jacobs, Christopher Wagner +2
Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is…
QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)
Nouraldin Jaber, Christopher Wagner, Swen Jacobs +2
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far f…
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
Swen Jacobs, Mouhammad Sakr, Martin Zimmermann
We investigate the satisfaction of specifications in Prompt Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify param…
The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Maximilien Colange +11
We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe th…
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
Swen Jacobs, Nicolas Basset, Roderick Bloem +11
We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe th…
Proceedings Sixth Workshop on Synthesis
Dana Fisman, Swen Jacobs
The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in…
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
Swen Jacobs, Mouhammad Sakr
We study cutoff results for parameterized verification and synthesis of guarded protocols, as introduced by Emerson and Kahlon (2000). Guarded protocols describe systems of process…
Distributed Synthesis for Parameterized Temporal Logics
Swen Jacobs, Leander Tentrup, Martin Zimmermann
We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped wi…
The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond
Swen Jacobs, Roderick Bloem
We report on the design of the third reactive synthesis competition (SYNTCOMP 2016), including a major extension of the competition to specifications in full linear temporal logic.…
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Romain Brenguier +13
We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchm…
A High-Level LTL Synthesis Format: TLSF v1.1
Swen Jacobs, Felix Klein, Sebastian Schirmer
We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but…
The Second Reactive Synthesis Competition (SYNTCOMP 2015)
Swen Jacobs, Roderick Bloem, Romain Brenguier +8
We report on the design and results of the second reactive synthesis competition (SYNTCOMP 2015). We describe our extended benchmark library, with 6 completely new sets of benchmar…
A High-Level LTL Synthesis Format: TLSF v1.0
Swen Jacobs, Felix Klein
We present the Temporal Logic Synthesis Format (TLSF), a high-level format to describe synthesis problems via Linear Temporal Logic (LTL). The format builds upon standard LTL, but…
Distributed PROMPT-LTL Synthesis
Swen Jacobs, Leander Tentrup, Martin Zimmermann
We consider the synthesis of distributed implementations for specifications in Prompt Linear Temporal Logic (PROMPT-LTL), which extends LTL by temporal operators equipped with para…
The First Reactive Synthesis Competition (SYNTCOMP 2014)
Swen Jacobs, Roderick Bloem, Romain Brenguier +10
We introduce the reactive synthesis competition (SYNTCOMP), a long-term effort intended to stimulate and guide advances in the design and application of synthesis procedures for re…
Tight Cutoffs for Guarded Protocols with Fairness
Simon Außerlechner, Swen Jacobs, Ayrat Khalimov
Guarded protocols were introduced in a seminal paper by Emerson and Kahlon (2000), and describe systems of processes whose transitions are enabled or disabled depending on the exis…