A Lyapunov Approach for Time-Bounded Reachability of CTMCs and CTMDPs. Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar. ACM Trans. Model. Perform. Evaluation Comput. Syst. 2020.
Algebraic Invariants for Linear Hybrid Automata. Rupak Majumdar, Joël Ouaknine, Amaury Pouly, James Worrell. CONCUR 2020.
On Ranking Function Synthesis and Termination for Polynomial Programs. Eike Neumann, Joël Ouaknine, James Worrell. CONCUR 2020.
On the relation between reactive synthesis and supervisory control of non-terminating processes. Anne-Kathrin Schmuck, Thomas Moor, Rupak Majumdar. Discret. Event Dyn. Syst. 2020.
On the relation between reactive synthesis and supervisory control of non-terminating processes. Anne-Kathrin Schmuck, Thomas Moor, Rupak Majumdar. Discrete Event Dynamic Systems 2020.
Reachability in Dynamical Systems with Rounding. Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, Markus A. Whiteland. FSTTCS 2020.
On abstraction-based controller design with output feedback. Rupak Majumdar, Necmiye Ozay, Anne-Kathrin Schmuck. HSCC 2020.
Symbolic controller synthesis for Büchi specifications on stochastic systems. Rupak Majumdar, Kaushik Mallik, Sadegh Soudjani. HSCC 2020.
Invariants for Continuous Linear Dynamical Systems. Shaull Almagor, Edon Kelmendi, Joël Ouaknine, James Worrell. ICALP 2020.
On Decidability of Time-Bounded Reachability in CTMDPs. Rupak Majumdar, Mahmoud Salamati, Sadegh Soudjani. ICALP 2020.
Rational Subsets of Baumslag-Solitar Groups. Michaël Cadilhac, Dmitry Chistikov, Georg Zetzsche. ICALP 2020.
The Complexity of Bounded Context Switching with Dynamic Thread Creation. Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche. ICALP 2020.
The Complexity of Knapsack Problems in Wreath Products. Michael Figelius, Moses Ganardi, Markus Lohrey, Georg Zetzsche. ICALP 2020.
DeepEquaL: Deep Learning Based Mathematical Equation to Latex Generation. Ghaith Bilbeisi, Sheraz Ahmed, Rupak Majumdar. ICONIP 2020.
Assume-Guarantee Distributed Synthesis. Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Damien Zufferey. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020.
On the skolem problem and prime powers. George Kenison, Richard Lipton, Joël Ouaknine, James Worrell. ISSAC 2020.
An Approach to Regular Separability in Vector Addition Systems. Wojciech Czerwinski, Georg Zetzsche. LICS 2020.
Extensions of ω-Regular Languages. Mikolaj Bojanczyk, Edon Kelmendi, Rafal Stefanski, Georg Zetzsche. LICS 2020.
Knapsack and the Power Word Problem in Solvable Baumslag-Solitar Groups. Markus Lohrey, Georg Zetzsche. MFCS 2020.
On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems. Toghrul Karimov, Joël Ouaknine, James Worrell. MFCS 2020.
Multiparty motion coordination: from choreographies to robotics programs. Rupak Majumdar, Nobuko Yoshida, Damien Zufferey. OOPSLA 2020.
Testing consensus implementations using communication closure. Cezara Dragoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic. OOPSLA 2020.
How Fast Can You Escape a Compact Polytope? Julian D'Costa, Engel Lefaucheux, Joël Ouaknine, James Worrell. STACS 2020.
Lazy Abstraction-Based Controller Synthesis. Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck. ATVA 2019.
Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer. CAV 2019.
Incremental Abstraction Computation for Symbolic Controller Synthesis in a Changing Environment. Yunjun Bai, Kaushik Mallik, Anne-Kathrin Schmuck, Damien Zufferey, Rupak Majumdar. CDC 2019.
Motion Session Types for Robotic Interactions (Brave New Idea Paper). Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, Damien Zufferey. ECOOP 2019.
The Geometry of Rank Decompositions of Matrix Multiplication I: 2 × 2 Matrices. Luca Chiantini, Christian Ikenmeyer, J. M. Landsberg, Giorgio Ottaviani. Experimental Mathematics 2019.
Regular Separability and Intersection Emptiness Are Independent Problems. Ramanathan S. Thinniyam, Georg Zetzsche. FSTTCS 2019.
On the decidability of reachability in linear time-invariant systems. Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell. HSCC 2019.
On Geometric Complexity Theory: Multiplicity Obstructions Are Stronger Than Occurrence Obstructions. Julian Dörfler, Christian Ikenmeyer, Greta Panova. ICALP 2019.
On Reachability Problems for Low-Dimensional Matrix Semigroups. Thomas Colcombet, Joël Ouaknine, Pavel Semukhin, James Worrell. ICALP 2019.
Termination of Linear Loops over the Integers. Mehran Hosseini, Joël Ouaknine, James Worrell. ICALP 2019.
PGCD: robot programming and verification with geometry, concurrency, and dynamics. Gregor B. Banusic, Rupak Majumdar, Marcus Pirron, Anne-Kathrin Schmuck, Damien Zufferey. ICCPS 2019.
Compositional Synthesis of Finite-State Abstractions. Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani, Rupak Majumdar. IEEE Trans. Autom. Control. 2019.
Shrinking Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances. Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Soudjani. IEEE Trans. Autom. Control. 2019.
Shrinking Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances. Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Soudjani. IEEE Trans. Automat. Contr. 2019.
On the Decidability of Membership in Matrix-exponential Semigroups. Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell. J. ACM 2019.
Cyclic-routing of Unmanned Aerial Vehicles. Nir Drucker, Hsi-Ming Ho, Joël Ouaknine, Michal Penn, Ofer Strichman. J. Comput. Syst. Sci. 2019.
Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. Christoph Haase, Georg Zetzsche. LICS 2019.
On the Expressiveness and Monitoring of Metric Temporal Logic. Hsi-Ming Ho, Joël Ouaknine, James Worrell. Log. Methods Comput. Sci. 2019.
On the Expressiveness and Monitoring of Metric Temporal Logic. Hsi-Ming Ho, Joël Ouaknine, James Worrell. Logical Methods in Computer Science 2019.
Trace aware random testing for distributed systems. Burcu Kulahcioglu Ozkan, Rupak Majumdar, Simin Oraee. OOPSLA 2019.
Checking linearizability using hitting families. Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic. PPoPP 2019.
Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets. Sylvain Schmitz, Georg Zetzsche. RP 2019.
On the Monniaux Problem in Abstract Interpretation. Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell. SAS 2019.
Environmentally-Friendly GR(1) Synthesis. Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck. TACAS 2019.
Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem. Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell. Theory Comput. Syst. 2019.
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.
Reachability analysis of reversal-bounded automata on series-parallel graphs. Rayna Dimitrova, Rupak Majumdar. Acta Informatica 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.
Lazy Abstraction-Based Control for Safety Specifications. Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck. CDC 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.
Bounded Context Switching for Valence Systems. Roland Meyer, Sebastian Muskalla, Georg Zetzsche. CONCUR 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.
Causality Analysis for Concurrent Reactive Systems (Extended Abstract). Rayna Dimitrova, Rupak Majumdar, Vinayak S. Prabhu. CREST@ETAPS 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.
iDeA: an immersive debugger for actors. Aman Shankar Mathur, Burcu Kulahcioglu Ozkan, Rupak Majumdar. Erlang Workshop 2018.
Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper). Rupak Majumdar. FSTTCS 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.
Unboundedness Problems for Languages of Vector Addition Systems. Wojciech Czerwinski, Piotr Hofman, Georg Zetzsche. 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.
Separability by piecewise testable languages and downward closures beyond subwords. Georg Zetzsche. LICS 2018.
Sequential Relational Decomposition. Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi. LICS 2018.
Model Checking Flat Freeze LTL on One-Counter Automata. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell. Log. Methods Comput. Sci. 2018.
Model Checking Flat Freeze LTL on One-Counter Automata. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell. Logical Methods in Computer Science 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.
Knapsack Problems for Wreath Products. Moses Ganardi, Daniel König, Markus Lohrey, Georg Zetzsche. STACS 2018.
On the complexity of hazard-free circuits. Christian Ikenmeyer, Balagopal Komarath, Christoph Lenzen, Vladimir Lysikov, Andrey Mokhov, Karteek Sreenivasaiah. STOC 2018.
Antlab: A Multi-Robot Task Server. Ivan Gavran, Rupak Majumdar, Indranil Saha. ACM Trans. Embed. Comput. Syst. 2017.
Testing Cyber-Physical Systems through Bayesian Optimization. Jyotirmoy V. Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu. ACM Trans. Embed. Comput. Syst. 2017.
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.
Approximate counting in SMT and value estimation for probabilistic programs. Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar. Acta Informatica 2017.
Dynamic Bayesian networks for formal verification of structured stochastic processes. Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar. Acta Informatica 2017.
Verification of population protocols. Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar. Acta Informatica 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.
Dynamic hierarchical reactive controller synthesis. Anne-Kathrin Schmuck, Rupak Majumdar, Adrian Leva. Discret. Event Dyn. Syst. 2017.
A Characterization for Decidable Separability by Piecewise Testable Languages. Wojciech Czerwinski, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, Georg Zetzsche. Discret. Math. Theor. Comput. Sci. 2017.
Model checking parameterized asynchronous shared-memory systems. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar. Formal Methods Syst. Des. 2017.
Quantifying conformance using the Skorokhod metric. Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu. Formal Methods Syst. Des. 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.
Decidability, complexity, and expressiveness of first-order logic over the subword ordering. Simon Halfon, Philippe Schnoebelen, Georg Zetzsche. LICS 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.
On Boolean Closed Full Trios and Rational Kripke Frames. Georg Zetzsche, Dietrich Kuske, Markus Lohrey. Theory Comput. Syst. 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.
Knapsack and subset sum problems in nilpotent, polycyclic, and co-context-free groups. Daniel König, Markus Lohrey, Georg Zetzsche. AMS-EMS-SPM Joint Meeting 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.
Supervisory control synthesis for deterministic context free specification languages - Enforcing controllability least restrictively. Anne-Kathrin Schmuck, Sven Schneider, Jörg Raisch, Uwe Nestmann. Discret. Event Dyn. Syst. 2016.
Permutations of context-free, ET0L and indexed languages. Tara Brough, Laura Ciobanu, Murray Elder, Georg Zetzsche. Discret. Math. Theor. Comput. Sci. 2016.
Permutations of context-free, ET0L and indexed languages. Tara Brough, Laura Ciobanu, Murray Elder, Georg Zetzsche. Discrete Mathematics & Theoretical Computer Science 2016.
Relating Reachability Problems in Timed and Counter Automata. Christoph Haase, Joël Ouaknine, James Worrell. Fundam. Inform. 2016.
Relating Reachability Problems in Timed and Counter Automata. Christoph Haase, Joël Ouaknine, James Worrell. Fundam. Informaticae 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.
First-order logic with reachability for infinite-state systems. Emanuele D'Osualdo, Roland Meyer, Georg Zetzsche. LICS 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.
The complexity of regular abstractions of one-counter languages. Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche. LICS 2016.
Knapsack in Graph Groups, HNN-Extensions and Amalgamated Products. Markus Lohrey, Georg Zetzsche. STACS 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.
Supervisory controller synthesis for decomposable deterministic context free specification languages. Kaushik Mallik, Anne-Kathrin Schmuck. WODES 2016.
On linear recurrence sequences and loop termination. Joël Ouaknine, James Worrell. ACM SIGLOG News 2015.
Model Checking Parameterized Asynchronous Shared-Memory Systems. Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar. CAV 2015.
Comparing asynchronous l-complete approximations and quotient based abstractions. Anne-Kathrin Schmuck, Paulo Tabuada, Jörg Raisch. CDC 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.
Rational subsets and submonoids of wreath products. Markus Lohrey, Benjamin Steinberg, Georg Zetzsche. Inf. Comput. 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.
Building bridges in abstraction-based controller synthesis: advancing, combining, and comparing methods from computer and control. Anne-Kathrin Schmuck. PhD Thesis 2015.
The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets. Georg Zetzsche. RP 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.
Constructing (Bi)similar finite state abstractions using asynchronous l-complete approximations. Anne-Kathrin Schmuck, Jörg Raisch. CDC 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. Autom. Control. 2014.
Towards Robustness for Cyber-Physical Systems. Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, Rupak Majumdar. IEEE Trans. Autom. Control. 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.
Simulation and bisimulation over multiple time scales in a behavioral setting. Anne-Kathrin Schmuck, Jörg Raisch. MED 2014.
Positivity Problems for Low-Order Linear Recurrence Sequences. Joël Ouaknine, James Worrell. SODA 2014.
Asynchronous I-complete approximations. Anne-Kathrin Schmuck, Jörg Raisch. Syst. Control. Lett. 2014.
Extending Supervisory Controller Synthesis to Deterministic Pushdown Automata - Enforcing Controllability Least Restrictively. Anne-Kathrin Schmuck, Sven Schneider, Jörg Raisch, Uwe Nestmann. WODES 2014.
Reducing an Operational Supervisory Control Problem by Decomposition for Deterministic Pushdown Automata. Sven Schneider, Anne-Kathrin Schmuck, Uwe Nestmann, Jörg Raisch. WODES 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. Embed. Comput. Syst. 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.
Algorithmic probabilistic game semantics - Playing games with automata. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. Formal Methods Syst. Des. 2013.
Code aware resource management. Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, Vishwanath Raman. Formal Methods Syst. Des. 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.
Rational Subsets and Submonoids of Wreath Products. Markus Lohrey, Benjamin Steinberg, Georg Zetzsche. ICALP 2013.
The Complexity of Coverage. Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar. Int. J. Found. Comput. Sci. 2013.
From tests to proofs. Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko. Int. J. Softw. Tools Technol. Transf. 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. Log. Methods Comput. Sci. 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. Log. Methods Comput. Sci. 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.
Semilinearity and Context-Freeness of Languages Accepted by Valence Automata. P. Buckheister, Georg Zetzsche. MFCS 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. Syst. Control. Lett. 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 Aspects Comput. 2012.
Three tokens in Herman's algorithm. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. Formal Aspects Comput. 2012.
Bounded underapproximations. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Formal Methods in System Design 2012.
Bounded underapproximations. Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Formal Methods Syst. Des. 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.
A Sufficient Condition for Erasing Productions to Be Avoidable. Georg Zetzsche. Developments in Language Theory 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.
On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids. Georg Zetzsche. ICALP 2011.
VCG with Communities on Random Ad Hoc Networks. Gunes Ercal, Rafit Izhak-Ratzin, Rupak Majumdar, Adam Meyerson. Int. J. Distributed Sens. Networks 2011.
Toward Understanding the Generative Capacity of Erasing Rules in Matrix Grammars. Georg Zetzsche. Int. J. Found. Comput. Sci. 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.
Algorithms for Game Metrics (Full Version) Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, Vishwanath Raman. Log. Methods Comput. Sci. 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.
Erasing in Petri Net Languages and Matrix Grammars. Georg Zetzsche. Developments in Language Theory 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.
Faster FDR Counterexample Generation Using SAT-Solving. Hristina Palikareva, Joël Ouaknine, Bill Roscoe. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 2009.
Properties of Multiset Language Classes Defined by Multiset Pushdown Automata. Manfred Kudlek, Patrick Totzke, Georg Zetzsche. Fundam. Inform. 2009.
Multiset Pushdown Automata. Manfred Kudlek, Patrick Totzke, Georg Zetzsche. Fundam. Informaticae 2009.
Properties of Multiset Language Classes Defined by Multiset Pushdown Automata. Manfred Kudlek, Patrick Totzke, Georg Zetzsche. Fundam. Informaticae 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.
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. Int. J. Softw. Tools Technol. Transf. 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.
Language Classes Defined by Concurrent Finite Automata. Matthias Jantzen, Manfred Kudlek, Georg Zetzsche. Fundam. Inform. 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.
Language Classes Defined by Concurrent Finite Automata. Matthias Jantzen, Manfred Kudlek, Georg Zetzsche. Fundam. Informaticae 2008.
Nets with Tokens which Carry Data. Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell. Fundam. Informaticae 2008.
Petri Net Controlled Finite Automata. Berndt Farwer, Matthias Jantzen, Manfred Kudlek, Heiko Rölke, Georg Zetzsche. Fundam. Informaticae 2008.
Universality Analysis for One-Clock Timed Automata. Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, James Worrell. Fundam. Informaticae 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. Comput. Aided Des. Integr. Circuits Syst. 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. Log. Methods Comput. Sci. 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.
The software model checker Blast. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar. Int. J. Softw. Tools Technol. Transf. 2007.
On the decidability and complexity of Metric Temporal Logic over finite words. Joël Ouaknine, James Worrell. Log. Methods Comput. Sci. 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.
Parallel Assignments in Software Model Checking. Murray Stokely, Sagar Chaki, Joël Ouaknine. Electron. Notes Theor. Comput. Sci. 2006.
Timed CSP: A Retrospective. Joël Ouaknine, Steve Schneider. Electron. 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.
Concurrent software verification with states, events, and deadlocks. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha. Formal Aspects 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.
Computational challenges in bounded model checking. Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman. Int. J. Softw. Tools Technol. Transf. 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. Verification 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.
Informatic vs. Classical Differentiation on the Real Line. Keye Martin, Joël Ouaknine. Electron. 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.
Efficient Verification of Sequential and Concurrent C Programs. Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav. Formal Methods Syst. Des. 2004.
Duality for Labelled Markov Processes. Michael W. Mislove, Joël Ouaknine, Dusko Pavlovic, James Worrell. FoSSaCS 2004.
Fair watermarking using combinatorial isolation lemmas. Jennifer L. Wong, Rupak Majumdar, Miodrag Potkonjak. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 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.
Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke. Electron. Notes Theor. Comput. Sci. 2003.
Axioms for Probability and Nondeterminism. Michael W. Mislove, Joël Ouaknine, James Worrell. EXPRESS 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.