Conference papers
- Contract-based Design and Verification of Multi-Agent Systems with
Quantitative Temporal Requirements
with Rafael Dewes
AAAI 2025 accepted to appear
- Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
with Philippe Heim
POPL 2025 accepted to appear
- Localized Attractor Computations for Infinite-State Games
with Philippe Heim, Satya Prakash Nayak, and Anne-Kathrin Schmuck
CAV 2024
- Solving Infinite-State Games via Acceleration
with Philippe Heim
POPL 2024
- Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
with Philippe Heim
TACAS 2023
- Compositional High-Quality Synthesis
with Rafael Dewes
ATVA 2023
- Probabilistic Hyperproperties of Markov Decision Processes
with Bernd Finkbeiner and Hazem Torfah
ATVA 2020
- Conformance-Based Doping Detection for Cyber-Physical Systems
with Maciej Gazda, Mohammad Reza Mousavi, Sebastian Biewer and Holger Hermanns
FORTE 2020
- Near-Optimal Reactive Synthesis Incorporating Runtime Information
with Suda Bharadwaj, Abraham P. Vinod and Ufuk Topcu
ICRA 2020
- Approximate Automata for Omega-regular Languages
with Bernd Finkbeiner and Hazem Torfah
ATVA 2019
- Synthesizing Approximate Implementations for Unrealizable Specifications
with Bernd Finkbeiner and Hazem Torfah
CAV 2019
- Synthesis of Minimum-Cost Shields for Multi-Agent Systems
with Suda Bharadwaj, Roderik Bloem, Bettina Könighofer and Ufuk Topcu
ACC 2019
- Maximum Realizability for Linear Temporal Logic Specifications
with Mahsa Ghasemi and Ufuk Topcu
ATVA 2018
- Synthesis of Surveillance Strategies via Belief Abstraction
with Suda Bharadwaj and Ufuk Topcu
CDC 2018
- Distributed Synthesis of Surveillance Strategies for Mobile Sensors
with Suda Bharadwaj and Ufuk Topcu
CDC 2018
- The Robot Routing Problem for Collecting Aggregate Stochastic Rewards
with Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu and Sadegh Esmaeil Zadeh Soudjani
CONCUR 2017
- Robust Optimal Policies for Markov Decision Processes with
Safety-Threshold Constraints
with
Jie Fu and
Ufuk Topcu
CDC 2016
- Symbolic Model Checking for Factored Probabilistic Models
with
David Deininger and
Rupak Majumdar
ATVA 2016
- Probabilistic CTL*: The Deductive Way
with
Luis María Ferrer Fioriti,
Holger Hermanns and
Rupak Majumdar
TACAS 2016
- Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
with Rupak Majumdar
GandALF 2015
- Approximate Counting in SMT and Value Estimation for Probabilistic Programs
with Dmitry Chistikov and Rupak Majumdar
TACAS 2015 (nominated for ETAPS Best Paper Award)
- Deductive Control Synthesis for Alternating-Time Logics
with Rupak Majumdar
EMSOFT 2014 (Nominated for Best Paper Award)
- Abstractions and Sensor Design in Partial-Information, Reactive Controller Synthesis
with Jie Fu and Ufuk Topcu
ACC 2014
- Lossy Channel Games under Incomplete Information
with Bernd Finkbeiner
SR 2013
- Counterexample-guided Synthesis of Observation Predicates
with Bernd Finkbeiner
FORMATS 2012
- Monitoring Temporal Information Flow
with Bernd Finkbeiner and Markus N. Rabe
ISoLA 2012 (invited paper)
- Model Checking Information Flow in Reactive Systems
with Bernd Finkbeiner, Máté Kovács, Markus N. Rabe and Helmut Seidl
VMCAI 2012 (won the RS3 Best Paper Award, best among 27 papers of the RS3 project)
- Synthesis of Fault-Tolerant Distributed Systems
with Bernd Finkbeier
ATVA 2009
- Abstraction Refinement for Games with Incomplete Information
with Bernd Finkbeiner
FSTTCS 2008
- Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?
with Andreas Podelski
VMCAI 2008
Journal articles
PhD thesis
Synthesis and Control of Infinite-State Systems with Partial Observability