Conference papers
- Issy: A Comprehensive Tool for Specification and Synthesis of  Infinite-State Reactive Systems
 with Philippe Heim
 CAV 2025 (accepted to appear)
- Synthesis of Communication Policies for Multi-Agent Systems Robust to
  Communication Restrictions
 with Saleh Soudijani
 IJCAI 2025 (accepted to appear)
-  Contract-based Design and Verification of Multi-Agent Systems with
  Quantitative Temporal Requirements
 with Rafael Dewes
 AAAI 2025 (Oral presentation)
- Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
 with Philippe Heim
 POPL 2025
-   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