Environmentally-friendly GR(1) Synthesis Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck. Technical Report MPI-SWS-2018-008 2018.
Reachability analysis of reversal-bounded automata on series-parallel graphs. Rayna Dimitrova, Rupak Majumdar. Acta Inf. 2018.
Concentration of Measure for Chance-Constrained Optimization. Sadegh Soudjani, Rupak Majumdar. ADHS 2018.
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility. Anthony W. Lin, Rupak Majumdar. ATVA 2018.
DebugAR: Mixed Dimensional Displays for Immersive Debugging of Distributed Systems. Patrick Reipschläger, Burcu Kulahcioglu Ozkan, Aman Shankar Mathur, Stefan Gumhold, Rupak Majumdar, Raimund Dachselt. CHI Extended Abstracts 2018.
Effective Divergence Analysis for Linear Recurrence Sequences. Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, James Worrell. CONCUR 2018.
Verification of Immediate Observation Population Protocols. Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy. CONCUR 2018.
Embedded software for robotics: challenges and future directions: special session. Houssam Abbas, Indranil Saha, Yasser Shoukry, Rüdiger Ehlers, Georgios Fainekos, Rajesh Gupta, Rupak Majumdar, Dogan Ulus. EMSOFT 2018.
Model Checking Real-Time Systems. Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine, James Worrell. Handbook of Model Checking 2018.
Symbolic Model Checking in Non-Boolean Domains. Rupak Majumdar, Jean-François Raskin. Handbook of Model Checking 2018.
Multi-Layered Abstraction-Based Controller Synthesis for Continuous-Time Systems. Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck. HSCC 2018.
O-Minimal Invariants for Linear Loops. Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, James Worrell. ICALP 2018.
Parameter optimization in control software using statistical fault localization techniques. Jyotirmoy V. Deshmukh, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu. ICCPS 2018.
Convex Language Semantics for Nondeterministic Probabilistic Automata. Gerco van Heerdt, Justin Hsu, Joël Ouaknine, Alexandra Silva. ICTAC 2018.
Polynomial Invariants for Affine Programs. Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell. LICS 2018.
Sequential Relational Decomposition. Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi. LICS 2018.
Randomized testing of distributed systems with probabilistic guarantees. Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher. OOPSLA 2018.
Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach. Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar. QEST 2018.
Antlab: A Multi-Robot Task Server. Ivan Gavran, Rupak Majumdar, Indranil Saha. ACM Trans. Embedded Comput. Syst. 2017.
Testing Cyber-Physical Systems through Bayesian Optimization. Jyotirmoy V. Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu. ACM Trans. Embedded Comput. Syst. 2017.
Compositional abstractions of interconnected discrete-time stochastic control systems. Abolfazl Lavaei, Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Majid Zamani. CDC 2017.
Compositional construction of finite state abstractions for stochastic control systems. Kaushik Mallik, Sadegh Esmaeil Zadeh Soudjani, Anne-Kathrin Schmuck, Rupak Majumdar. CDC 2017.
On the Polytope Escape Problem for Continuous Linear Dynamical Systems. Joël Ouaknine, João Sousa Pinto, James Worrell. HSCC 2017.
On parametric timed automata and one-counter machines. Daniel Bundala, Joël Ouaknine. Inf. Comput. 2017.
Timed Temporal Logics. Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, James Worrell. Models, Algorithms, Logics and Tools 2017.
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem. Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell. STACS 2017.
Hitting Families of Schedules for Asynchronous Programs. Dmitry Chistikov, Rupak Majumdar, Filip Niksic. CAV 2016.
Algorithms and Tools for Verification and Testing of Asynchronous Programs Zilong Wang. Technical Report MPI-SWS-2016-001 2016.
Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete. Ranko Lazic, Joël Ouaknine, James Worrell. ACM Trans. Comput. Log. 2016.
Symbolic Model Checking for Factored Probabilistic Models. David Deininger, Rayna Dimitrova, Rupak Majumdar. ATVA 2016.
Model Checking Flat Freeze LTL on One-Counter Automata. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell. CONCUR 2016.
Relating Reachability Problems in Timed and Counter Automata. Christoph Haase, Joël Ouaknine, James Worrell. Fundam. Inform. 2016.
On the Skolem Problem for Continuous Linear Dynamical Systems. Ventsislav Chonev, Joël Ouaknine, James Worrell. ICALP 2016.
Proving the Herman-Protocol Conjecture. Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, James Worrell. ICALP 2016.
On the Complexity of the Orbit Problem. Ventsislav Chonev, Joël Ouaknine, James Worrell. J. ACM 2016.
Parameterized Verification of Asynchronous Shared-Memory Systems. Javier Esparza, Pierre Ganty, Rupak Majumdar. J. ACM 2016.
On Recurrent Reachability for Continuous Linear Dynamical Systems. Ventsislav Chonev, Joël Ouaknine, James Worrell. LICS 2016.
Solvability of Matrix-Exponential Equations. Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell. LICS 2016.
Partial Order Reduction for Event-Driven Multi-threaded Programs. Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar. TACAS 2016.
Probabilistic CTL: The Deductive Way. Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar. TACAS 2016.
Safety Verification of Continuous-Space Pure Jump Markov Processes. Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Alessandro Abate. TACAS 2016.
Model Checking Parameterized Asynchronous Shared-Memory Systems. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar. CAV 2015.
Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes. Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar. CONCUR 2015.
Rely/Guarantee Reasoning for Asynchronous Programs. Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis. CONCUR 2015.
Verification of Population Protocols. Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar. CONCUR 2015.
Analysis of Asynchronous Programs with Event-Based Synchronization. Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo. ESOP 2015.
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs. Rayna Dimitrova, Rupak Majumdar. GandALF 2015.
Computing the Skorokhod distance between polygonal traces. Rupak Majumdar, Vinayak S. Prabhu. HSCC 2015.
Dynamic scheduling for networked control systems. Indranil Saha, Sanjoy Baruah, Rupak Majumdar. HSCC 2015.
Reachability problems for Markov chains. S. Akshay, Timos Antonopoulos, Joël Ouaknine, James Worrell. Inf. Process. Lett. 2015.
On the Complexity of Linear Arithmetic with Divisibility. Antonia Lechner, Joël Ouaknine, James Worrell. LICS 2015.
Approximate Counting in SMT and Value Estimation for Probabilistic Programs. Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar. TACAS 2015.
Synthesis of Geometry Proof Problems. Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay. AAAI 2014.
An SMT-Based Approach to Coverability Analysis. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic. CAV 2014.
Regression Test Selection for Distributed Software Histories. Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov. CAV 2014.
Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122). Rupak Majumdar, Richard M. Murray, Pavithra Prabhakar. Dagstuhl Reports 2014.
Deductive control synthesis for alternating-time logics. Rayna Dimitrova, Rupak Majumdar. EMSOFT 2014.
Dynamic Package Interfaces. Shahram Esmaeilsabzali, Rupak Majumdar, Thomas Wies, Damien Zufferey. FASE 2014.
Kuai: A model checker for software-defined networks. Rupak Majumdar, Sai Deep Tetali, Zilong Wang. FMCAD 2014.
Foundations for Decision Problems in Separation Logic with General Inductive Predicates. Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, Joël Ouaknine. FoSSaCS 2014.
Model checking Timed CSP. Philip J. Armstrong, Gavin Lowe, Joël Ouaknine, Bill Roscoe. HOWARD-60 2014.
Edit distance for timed automata. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Rupak Majumdar. HSCC 2014.
On the Positivity Problem for Simple Linear Recurrence Sequences, . Joël Ouaknine, James Worrell. ICALP 2014.
Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences. Joël Ouaknine, James Worrell. ICALP 2014.
Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions. Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros. IEEE Trans. Automat. Contr. 2014.
Towards Robustness for Cyber-Physical Systems. Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, Rupak Majumdar. IEEE Trans. Automat. Contr. 2014.
Positivity Problems for Low-Order Linear Recurrence Sequences. Joël Ouaknine, James Worrell. SODA 2014.
A Uniformization Theorem for Nested Word to Word Transductions Dmitry Chistikov, Rupak Majumdar. Technical Report MPI-SWS-2013-002 2013.
A theory of robust omega-regular software synthesis. Rupak Majumdar, Elaine Render, Paulo Tabuada. ACM Trans. Embedded Comput. Syst. 2013.
Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points. Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell. ATVA 2013.
Incremental, Inductive Coverability. Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac. CAV 2013.
SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. Christoph Haase, Samin Ishtiaq, Joël Ouaknine, Matthew J. Parkinson. CAV 2013.
The first workshop on language support for privacy-enhancing technologies (PETShop'13). Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith. CCS 2013.
Bisimilar finite abstractions of stochastic control systems. Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros. CDC 2013.
Compositional equivalence checking for models and code of control systems. Rupak Majumdar, Indranil Saha, Koichi Ueda, Hakan Yazarel. CDC 2013.
A Uniformization Theorem for Nested Word to Word Transductions. Dmitry Chistikov, Rupak Majumdar. CIAA 2013.
Expand, Enlarge, and Check for Branching Vector Addition Systems. Rupak Majumdar, Zilong Wang. CONCUR 2013.
Synthesis of Fixed-point Programs Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha. EMSOFT 2013.
Verifying multi-threaded software with impact. Björn Wachter, Daniel Kroening, Joël Ouaknine. FMCAD 2013.
Algorithmic probabilistic game semantics - Playing games with automata. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. Formal Methods in System Design 2013.
Code aware resource management. Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, Vishwanath Raman. Formal Methods in System Design 2013.
Specification and Verification of Linear Dynamical Systems: Advances and Challenges. Joël Ouaknine. FroCos 2013.
A Theory of Partitioned Global Address Spaces. Georgel Calin, Egor Derevenetc, Rupak Majumdar, Roland Meyer. FSTTCS 2013.
The Complexity of Coverage. Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar. Int. J. Found. Comput. Sci. 2013.
Expressive Completeness for Metric Temporal Logic. Paul Hunter, Joël Ouaknine, James Worrell. LICS 2013.
A Static Analysis Framework for Livelock Freedom in CSP Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell. Logical Methods in Computer Science 2013.
On the Complexity of Equivalence and Minimisation for Q-weighted Automata Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. Logical Methods in Computer Science 2013.
Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian. Ranko Lazic, Joël Ouaknine, James Worrell. MFCS 2013.
MrCrypt: static analysis for secure cloud computations. Sai Deep Tetali, Mohsen Lesani, Rupak Majumdar, Todd D. Millstein. OOPSLA 2013.
Static Provenance Verification for Message Passing Programs. Rupak Majumdar, Roland Meyer, Zilong Wang. SAS 2013.
Backstepping controller synthesis and characterizations of incremental stability. Majid Zamani, Nathan van de Wouw, Rupak Majumdar. Systems & Control Letters 2013.
Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games. Krishnendu Chatterjee, Martin Chmelik, Rupak Majumdar. ATVA 2012.
APEX: An Analyzer for Open Probabilistic Programs. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. CAV 2012.
Approximately Bisimilar Symbolic Models for Digital Control Systems. Rupak Majumdar, Majid Zamani. CAV 2012.
Recent Developments in FDR. Philip J. Armstrong, Michael Goldsmith, Gavin Lowe, Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell. CAV 2012.
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). Nikolaj Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar. Dagstuhl Reports 2012.
Input-output robustness for discrete systems. Paulo Tabuada, Ayca Balkan, Sina Y. Caliskan, Yasser Shoukry, Rupak Majumdar. EMSOFT 2012.
Synthesis of minimal-error control software. Rupak Majumdar, Indranil Saha, Majid Zamani. EMSOFT 2012.
Language-Theoretic Abstraction Refinement. Zhenyue Long, Georgel Calin, Rupak Majumdar, Roland Meyer. FASE 2012.
On termination and invariance for faulty channel machines. Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell. Formal Asp. Comput. 2012.
Three tokens in Herman's algorithm. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. Formal Asp. Comput. 2012.
Bounded underapproximations. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Formal Methods in System Design 2012.
Branching-Time Model Checking of Parametric One-Counter Automata. Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell. FoSSaCS 2012.
On the Complexity of the Equivalence Problem for Probabilistic Automata. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. FoSSaCS 2012.
Discounting and Averaging in Games across Time scales. Krishnendu Chatterjee, Rupak Majumdar. Int. J. Found. Comput. Sci. 2012.
Countermodels from Sequent Calculi in Multi-Modal Logics Deepak Garg, Valerio Genovese, Sara Negri. LICS 2012.
On the Magnitude of Completeness Thresholds in Bounded Model Checking. Daniel Bundala, Joël Ouaknine, James Worrell. LICS 2012.
CLSE: Closed-Loop Symbolic Execution. Rupak Majumdar, Indranil Saha, K. C. Shashidhar, Zilong Wang. NASA Formal Methods 2012.
Engage: a deployment management system. Jeffrey Fischer, Rupak Majumdar, Shahram Esmaeilsabzali. PLDI 2012.
On the Relationship between Reachability Problems in Timed and Counter Automata. Christoph Haase, Joël Ouaknine, James Worrell. RP 2012.
Efficient May Happen in Parallel Analysis for Async-Finish Parallelism. Jonathan K. Lee, Jens Palsberg, Rupak Majumdar, Hong Hong. SAS 2012.
SAT-solving in CSP trace refinement. Hristina Palikareva, Joël Ouaknine, A. W. Roscoe. Sci. Comput. Program. 2012.
HMC: Verifying Functional Programs Using Abstract Interpreters. Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko. CAV 2011.
Language Equivalence for Probabilistic Automata. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. CAV 2011.
Linear Completeness Thresholds for Bounded Model Checking. Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell. CAV 2011.
Static Livelock Analysis in CSP. Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell. CONCUR 2011.
Tractable Reasoning in a Fragment of Separation Logic. Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, James Worrell. CONCUR 2011.
The Church Synthesis Problem with Metric. Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, James Worrell. CSL 2011.
Performance-aware scheduler synthesis for control systems. Rupak Majumdar, Indranil Saha, Majid Zamani. EMSOFT 2011.
End-to-End Guarantees in Embedded Control Systems - (Abstract). Rupak Majumdar. Ershov Memorial Conference 2011.
Minimum Attention Controller Synthesis for Omega-Regular Objectives. Krishnendu Chatterjee, Rupak Majumdar. FORMATS 2011.
Pessoa 2.0: a controller synthesis tool for cyber-physical systems. Pritam Roy, Paulo Tabuada, Rupak Majumdar. HSCC 2011.
Robust discrete synthesis against unspecified disturbances. Rupak Majumdar, Elaine Render, Paulo Tabuada. HSCC 2011.
On Reachability for Hybrid Automata over Bounded Time. Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell. ICALP 2011.
On Stabilization in Herman's Algorithm. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, Lijun Zhang. ICALP 2011.
VCG with Communities on Random Ad Hoc Networks. Gunes Ercal, Rafit Izhak-Ratzin, Rupak Majumdar, Adam Meyerson. IJDSN 2011.
Cause clue clauses: error localization using maximum satisfiability. Manu Jose, Rupak Majumdar. PLDI 2011.
On Searching for Small Kochen-Specker Vector Systems. Felix Arends, Joël Ouaknine, Charles W. Wampler. WG 2011.
Computing Rational Radical Sums in Uniform TC^0. Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell. FSTTCS 2010.
Model Checking Succinct and Parametric One-Counter Automata. Stefan Göller, Christoph Haase, Joël Ouaknine, James Worrell. ICALP 2010.
Alternating Timed Automata over Bounded Time. Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, James Worrell. LICS 2010.
Systematic testing for control applications. Rupak Majumdar, Indranil Saha, Zilong Wang. MEMOCODE 2010.
On Process-Algebraic Extensions of Metric Temporal Logic. Christoph Haase, Joël Ouaknine, James Worrell. Reflections on the Work of C. A. R. Hoare 2010.
Shape Analysis with Reference Set Relations. Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur. VMCAI 2010.
Reachability in Succinct and Parametric One-Counter Automata. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell. CONCUR 2009.
Faster FDR Counterexample Generation Using SAT-Solving. Hristina Palikareva, Joël Ouaknine, Bill Roscoe. ECEASST 2009.
Fine-Grained Access Control with Object-Sensitive Roles. Jeffrey Fischer, Daniel Marino, Rupak Majumdar, Todd D. Millstein. ECOOP 2009.
IPR: In-Place Reconfiguration for FPGA fault tolerance. Zhe Feng, Yu Hu, Lei He, Rupak Majumdar. ICCAD 2009.
Team Incentives in BitTorrent Systems. Rafit Izhak-Ratzin, Nikitas Liogkas, Rupak Majumdar. ICCCN 2009.
Simultaneous test pattern compaction, ordering and X-filling for testing power reduction. Ju-Yueh Lee, Yu Hu, Rupak Majumdar, Lei He. ISQED 2009.
Verifying liveness for asynchronous programs. Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko. POPL 2009.
An abstraction-based decision procedure for bit-vector arithmetic. Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady. STTT 2009.
Verifying Reference Counting Implementations. Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar. TACAS 2009.
FPGA area reduction by multi-output function based sequential resynthesis. Yu Hu, Victor Shih, Rupak Majumdar, Lei He. DAC 2008.
Nets with Tokens which Carry Data. Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell. Fundam. Inform. 2008.
Universality Analysis for One-Clock Timed Automata. Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, James Worrell. Fundam. Inform. 2008.
On Expressiveness and Complexity in Real-Time Model Checking. Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell. ICALP 2008.
Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs. Yu Hu, Victor Shih, Rupak Majumdar, Lei He. IEEE Trans. on CAD of Integrated Circuits and Systems 2008.
Stochastic limit-average games are in EXPTIME. Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger. Int. J. Game Theory 2008.
Game Refinement Relations and Metrics. Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga. Logical Methods in Computer Science 2008.
On Termination for Faulty Channel Machines. Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell. STACS 2008.
On Automated Verification of Probabilistic Programs. Axel Legay, Andrzej S. Murawski, Joël Ouaknine, James Worrell. TACAS 2008.
Undecidability of Universality for Timed Automata with Minimal Resources. Sara Adams, Joël Ouaknine, James Worrell. FORMATS 2007.
Zone-Based Universality Analysis for Single-Clock Timed Automata. Parosh Aziz Abdulla, Joël Ouaknine, Karin Quaas, James Worrell. FSEN 2007.
Nets with Tokens Which Carry Data. Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell. ICATPN 2007.
On the decidability and complexity of Metric Temporal Logic over finite words. Joël Ouaknine, James Worrell. Logical Methods in Computer Science 2007.
Deciding Bit-Vector Arithmetic with Abstraction. Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady. TACAS 2007.
On Timed Models and Full Abstraction. Gavin Lowe, Joël Ouaknine. Electr. Notes Theor. Comput. Sci. 2006.
Parallel Assignments in Software Model Checking. Murray Stokely, Sagar Chaki, Joël Ouaknine. Electr. Notes Theor. Comput. Sci. 2006.
On Probabilistic Program Equivalence and Refinement. Andrzej S. Murawski, Joël Ouaknine. CONCUR 2005.
Concurrent software verification with states, events, and deadlocks. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha. Formal Asp. Comput. 2005.
Decidability and Complexity Results for Timed Automata via Channel Machines. Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, James Worrell. ICALP 2005.
State/Event Software Verification for Branching-Time Specifications. Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith. IFM 2005.
Verification of Reactive Systems: Formal Methods and Algorithms. By Klaus Schneider. Springer, Texts in Theoretical Computer Science Series, 2004, ISBN: 3-540-00296-0, pp 600. Joël Ouaknine. Softw. Test., Verif. Reliab. 2005.
Computational challenges in bounded model checking. Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman. STTT 2005.
Domain theory, testing and simulation for labelled Markov processes. Franck van Breugel, Michael W. Mislove, Joël Ouaknine, James Worrell. Theor. Comput. Sci. 2005.
Abstraction-Based Satisfiability Solving of Presburger Arithmetic. Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman. CAV 2004.
Axioms for Probability and Nondeterminism. Michael W. Mislove, Joël Ouaknine, James Worrell. Electr. Notes Theor. Comput. Sci. 2004.
Informatic vs. Classical Differentiation on the Real Line. Keye Martin, Joël Ouaknine. Electr. Notes Theor. Comput. Sci. 2004.
Efficient Verification of Sequential and Concurrent C Programs. Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav. Formal Methods in System Design 2004.
Duality for Labelled Markov Processes. Michael W. Mislove, Joël Ouaknine, Dusko Pavlovic, James Worrell. FoSSaCS 2004.
State/Event-Based Software Model Checking. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha. IFM 2004.
On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. Joël Ouaknine, James Worrell. LICS 2004.
Automated, compositional and iterative deadlock detection. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina. MEMOCODE 2004.
Completeness and Complexity of Bounded Model Checking. Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman. VMCAI 2004.
Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke. Electr. Notes Theor. Comput. Sci. 2003.
An Intrinsic Characterization of Approximate Probabilistic Bisimilarity. Franck van Breugel, Michael W. Mislove, Joël Ouaknine, James Worrell. FoSSaCS 2003.
Universality and Language Inclusion for Open and Closed Timed Automata. Joël Ouaknine, James Worrell. HSCC 2003.
Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, Michael Theobald. Int. J. Found. Comput. Sci. 2003.
Revisiting Digitization, Robustness, and Decidability for Timed Automata. Joël Ouaknine, James Worrell. LICS 2003.
Timed CSP = Closed Timed Safety Automata. Joël Ouaknine, James Worrell. Electr. Notes Theor. Comput. Sci. 2002.