Publications

• Linear dynamical systems
• Timed automata and Metric Temporal Logic
• Software model checking (and related work)
• Probabilistic systems
• Infinite-state systems
• Timed CSP
• Miscellaneous

Linear dynamical systems

• T. Karimov, F. Luca, J. Nieuwveld, J. Ouaknine, and J. Worrell. On the decidability of Presburger arithmetic expanded with powers.
  Proceedings of SODA 25, 2025.

• R. Aghamov, C. Baier, T. Karimov, J. Nieuwveld, J. Ouaknine, J. Piribauer, and M. Vahanwala. Model checking Markov chains as distribution transformers.
  Principles of Verification: Cycling the Probabilistic Landscape -- Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, LNCS 15261, 2024.

• F. Luca, J. Maynard, A. Noubissie, J. Ouaknine, and J. Worrell. Skolem meets Bateman-Horn.
  Submitted, 2024.

• P. Kebis, F. Luca, J. Ouaknine, A. Scoones, and J. Worrell. On transcendence of numbers related to Sturmian and Arnoux-Rauzy words.
  Proceedings of ICALP 24, LIPIcs 297, 2024.

• Q. Guilmant, E. Lefaucheux, J. Ouaknine, and J. Worrell. The 2-dimensional constraint loop problem is decidable.
  Proceedings of ICALP 24, LIPIcs 297, 2024.

• V. Berthé, T. Karimov, J. Nieuwveld, J. Ouaknine, M. Vahanwala, and J. Worrell. On the decidability of monadic second-order logic with arithmetic predicates.
  Proceedings of LICS 24, 2024. Distinguished Paper Award.

• T. Karimov, E. Kelmendi, J. Ouaknine, and J. Worrell. Multiple reachability in linear dynamical systems.
  Submitted, 2024.

• Y. Bilu, F. Luca, J. Nieuwveld, J. Ouaknine, and J. Worrell. Twisted rational zeros of linear recurrence sequences.
  Submitted, 2023.

• V. Berthé, T. Karimov, J. Nieuwveld, J. Ouaknine, M. Vahanwala, and J. Worrell. The monadic theory of toric words.
  Theoretical Computer Science 1025, 2024.

• R. Aghamov, C. Baier, T. Karimov, J. Ouaknine, and J. Piribauer. Linear dynamical systems with continuous weight functions.
  Proceedings of HSCC 24, 2024. ACM SIGBED Best Paper Award.

• J. D'Costa, J. Ouaknine, and J. Worrell. Nonnegativity problems for matrix semigroups.
  Proceedings of STACS 24, LIPIcs 289, 2024.

• F. Luca, J. Ouaknine, and J. Worrell. On the transcendence of a series related to Sturmian words.
  To appear in Annali della Scuola Normale Superiore di Pisa ????(????), 2024.

• E. Lefaucheux, J. Ouaknine, D. Purser, and J. Worrell. Porous invariants for linear systems.
  Formal Methods in System Design ????(????), 2024.

• E. Hrushovski, J. Ouaknine, A. Pouly, and J. Worrell. On strongest algebraic program invariants.
  Journal of the ACM 70(5), 2023.

• V. Chonev, J. Ouaknine, and J. Worrell. On the zeros of exponential polynomials.
  Journal of the ACM 70(4), 2023.

• Y. Bilu, F. Luca, J. Nieuwveld, J. Ouaknine, and J. Worrell. On the p-adic zeros of the Tribonacci sequence.
  Mathematics of Computation 93(347), 2023.

• G. Kenison, J. Nieuwveld, J. Ouaknine, and J. Worrell. Positivity problems for reversible linear recurrence sequences.
  Proceedings of ICALP 23, LIPIcs 261, 2023.

• T. Karimov, E. Kelmendi, J. Nieuwveld, J. Ouaknine, and J. Worrell. The power of Positivity.
  Proceedings of LICS 23, 2023.

• F. Ghahremani, E. Kelmendi, and J. Ouaknine. Reachability in injective piecewise affine maps.
  Proceedings of LICS 23, 2023.

• G. Kenison, O. Klurman, E. Lefaucheux, F. Luca, P. Moree, J. Ouaknine, M. A. Whiteland, and J. Worrell. On inequality decision problems for low-order holonomic sequences.
  Submitted, 2023.

• E. Lefaucheux, J. Ouaknine, D. Purser, M. Sharifi. Model checking linear dynamical systems under floating-point rounding.
  Proceedings of TACAS 23, LNCS 13993, 2023.

• T. Karimov, E. Kelmendi, J. Ouaknine, and J. Worrell. What's decidable about discrete linear dynamical systems?.
  Principles of System Design -- Thomas A. Henzinger Festschrift, LNCS 13660, 2022.

• F. Luca, J. Ouaknine, and J. Worrell. Algebraic model checking for discrete linear dynamical systems.
  Proceedings of FORMATS 22 (invited paper), LNCS 13465, 2022.

• C. Baier, F. Funke, S. Jantsch, T. Karimov, E. Lefaucheux, J. Ouaknine, D. Purser, M. A. Whiteland, and J. Worrell. Parameter synthesis for parametric probabilistic dynamical systems and prefix-independent specifications.
  Proceedings of CONCUR 22, LIPIcs 243, 2022.

• Y. Bilu, F. Luca, J. Nieuwveld, J. Ouaknine, D. Purser, and J. Worrell. Skolem meets Schanuel.
  Proceedings of MFCS 22, LIPIcs 241, 2022.

• F. Luca, J. Ouaknine, and J. Worrell. A universal Skolem set of positive lower density.
  Proceedings of MFCS 22, LIPIcs 241, 2022.

• J. D'Costa, T. Karimov, R. Majumdar, J. Ouaknine, M. Salamati, and J. Worrell. The pseudo-reachability problem for diagonalisable linear dynamical systems.
  Proceedings of MFCS 22, LIPIcs 241, 2022.

• J. D'Costa, E. Lefaucheux, E. Neumann, J. Ouaknine, and J. Worrell. Bounding the escape time of a linear dynamical system over a compact semialgebraic set.
  Proceedings of MFCS 22, LIPIcs 241, 2022.

• R. J. Lipton, F. Luca, J. Nieuwveld, J. Ouaknine, D. Purser, and J. Worrell. On the Skolem Problem and the Skolem Conjecture.
  Proceedings of LICS 22, 2022.

• T. Karimov, E. Lefaucheux, J. Ouaknine, D. Purser, A. Varonka, M. A. Whiteland, and J. Worrell. What's decidable about linear loops?.
  Proceedings of POPL 22, 2022.

• S. Almagor, D. Chistikov, J. Ouaknine, and J. Worrell. O-minimal invariants for discrete-time dynamical systems.
  ACM TOCL 23(2), 2022.

• C. Baier, F. Funke, S. Jantsch, T. Karimov, E. Lefaucheux, F. Luca, J. Ouaknine, D. Purser, M. A. Whiteland, and J. Worrell. The Orbit Problem for parametric linear dynamical systems.
  Proceedings of CONCUR 21, LIPIcs 203, 2021.

• G. Kenison, O. Klurman, E. Lefaucheux, F. Luca, P. Moree, J. Ouaknine, M. A. Whiteland, and J. Worrell. On positivity and minimality for second-order holonomic sequences.
  Proceedings of MFCS 21, LIPIcs 202, 2021.

• J. D'Costa, T. Karimov, R. Majumdar, J. Ouaknine, M. Salamati, S. Soudjani, and J. Worrell. The Pseudo-Skolem Problem is decidable.
  Proceedings of MFCS 21, LIPIcs 202, 2021.

• J. D'Costa, E. Lefaucheux, E. Neumann, J. Ouaknine, and J. Worrell. On the complexity of the Escape Problem for linear dynamical systems over compact semialgebraic sets.
  Proceedings of MFCS 21, LIPIcs 202, 2021.

• E. Neumann, J. Ouaknine, and J. Worrell. Decision problems for second-order holonomic recurrences.
  Proceedings of ICALP 21, LIPIcs 198, 2021.

• E. Lefaucheux, J. Ouaknine, D. Purser, and J. Worrell. Porous invariants.
  Proceedings of CAV 21, LNCS 12760, 2021.

• F. Luca, J. Ouaknine, and J. Worrell. Universal Skolem sets.
  Proceedings of LICS 21, 2021. Distinguished Paper Award.

• S. Almagor, T. Karimov, E. Kelmendi, J. Ouaknine, and J. Worrell. Deciding ω-regular properties on linear recurrence sequences.
  Proceedings of POPL 21, 2021.

• C. Baier, F. Funke, S. Jantsch, T. Karimov, E. Lefaucheux, J. Ouaknine, A. Pouly, D. Purser, and M. A. Whiteland. Reachability in dynamical systems with rounding.
  Proceedings of FSTTCS 20, LIPIcs 182, 2020.

• R. Majumdar, J. Ouaknine, A. Pouly, and J. Worrell. Algebraic invariants for linear hybrid automata.
  Proceedings of CONCUR 20, LIPIcs 171, 2020.

• E. Neumann, J. Ouaknine, and J. Worrell. On ranking function synthesis and termination for polynomial programs.
  Proceedings of CONCUR 20, LIPIcs 171, 2020.

• T. Karimov, J. Ouaknine, and J. Worrell. On LTL model-checking for low-dimensional discrete linear dynamical systems.
  Proceedings of MFCS 20, LIPIcs 170, 2020.

• G. Kenison, R. J. Lipton, J. Ouaknine, and J. Worrell. On the Skolem Problem and prime powers.
  Proceedings of ISSAC 20, 2020.

• S. Almagor, E. Kelmendi, J. Ouaknine, and J. Worrell. Invariants for continuous linear dynamical systems.
  Proceedings of ICALP 20, LIPIcs 168, 2020.

• J. D'Costa, E. Lefaucheux, J. Ouaknine, and J. Worrell. How fast can you escape a compact polytope?.
  Proceedings of STACS 20, LIPIcs 154, 2020.

• S. Almagor, J. Ouaknine, and J. Worrell. First-order orbit queries.
  Theory of Computing Systems 65(4), 2020.

• N. Fijalkow, E. Lefaucheux, P. Ohlmann, J. Ouaknine, A. Pouly, and J. Worrell. On the Monniaux Problem in abstract interpretation.
  Proceedings of SAS 19, LNCS 11822, 2019.

• M. Hosseini, J. Ouaknine, and J. Worrell. Termination of linear loops over the integers.
  Proceedings of ICALP 19, LIPIcs 132, 2019.

• T. Colcombet, J. Ouaknine, P. Semukhin, and J. Worrell. On reachability problems for low-dimensional matrix semigroups.
  Proceedings of ICALP 19, LIPIcs 132, 2019.

• N. Fijalkow, P. Ohlmann, J. Ouaknine, A. Pouly, and J. Worrell. Complete semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem.
  Theory of Computing Systems 63(5), 2019.

• N. Fijalkow, J. Ouaknine, A. Pouly, J. Sousa Pinto, and J. Worrell. On the decidability of reachability in linear time-invariant systems.
  Proceedings of HSCC 19, 2019.

• S. Almagor, J. Ouaknine, and J. Worrell. The Semialgebraic Orbit Problem.
  Proceedings of STACS 19, LIPIcs 126, 2019.

• J. Ouaknine, A. Pouly, J. Sousa Pinto, and J. Worrell. On the decidability of membership in matrix-exponential semigroups.
  Journal of the ACM 66(2), 2019.

• S. Almagor, B. Chapman, M. Hosseini, J. Ouaknine, and J. Worrell. Effective divergence analysis for linear recurrence sequences.
  Proceedings of CONCUR 18, LIPIcs 118, 2018.

• S. Almagor, D. Chistikov, J. Ouaknine, and J. Worrell. O-minimal invariants for linear loops.
  Proceedings of ICALP 18, LIPIcs 107, 2018.

• E. Hrushovski, J. Ouaknine, A. Pouly, and J. Worrell. Polynomial invariants for affine programs.
  Proceedings of LICS 18, 2018.

• S. Almagor, J. Ouaknine, and J. Worrell. The Polytope-Collision Problem.
  Proceedings of ICALP 17, LIPIcs 80, 2017.

• J. Ouaknine, J. Sousa Pinto, and J. Worrell. On the Polytope Escape Problem for continuous linear dynamical systems.
  Proceedings of HSCC 17, 2017.

• N. Fijalkow, P. Ohlmann, J. Ouaknine, A. Pouly, and J. Worrell. Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem.
  Proceedings of STACS 17, LIPIcs 66, 2017.

• V. Chonev, J. Ouaknine, and J. Worrell. On the Skolem Problem for continuous linear dynamical systems.
  Proceedings of ICALP 16, LIPIcs 55, 2016.

• V. Chonev, J. Ouaknine, and J. Worrell. On recurrent reachability for continuous linear dynamical systems.
  Proceedings of LICS 16, 2016.

• J. Ouaknine, A. Pouly, J. Sousa Pinto, and J. Worrell. Solvability of matrix-exponential equations.
  Proceedings of LICS 16, 2016.

• V. Chonev, J. Ouaknine, and J. Worrell. On the complexity of the Orbit Problem.
  Journal of the ACM 63(3), 2016. Notable Article, ACM Computing Reviews 21st Annual Best of Computing (2016).

• J. Ouaknine and J. Worrell. On linear recurrence sequences and loop termination (a survey).
  ACM SIGLOG News 2(2), 2015.

• E. Galby, J. Ouaknine, and J. Worrell. On matrix powering in low dimensions.
  Proceedings of STACS 15, LIPIcs 30, 2015.

• J. Ouaknine, J. Sousa Pinto, and J. Worrell. On termination of integer linear loops.
  Proceedings of SODA 15, 2015.

• V. Chonev, J. Ouaknine, and J. Worrell. The Polyhedron-Hitting Problem.
  Proceedings of SODA 15, 2015.

• S. Akshay, T. Antonopoulos, J. Ouaknine, and J. Worrell. Reachability problems for Markov chains.
  Information Processing Letters 115(2), 2015.

• J. Ouaknine and J. Worrell. Ultimate Positivity is decidable for simple linear recurrence sequences.
  Proceedings of ICALP 14, LNCS 8573, 2014. Best Paper Award.

• J. Ouaknine and J. Worrell. On the Positivity Problem for simple linear recurrence sequences.
  Proceedings of ICALP 14, LNCS 8573, 2014.

• J. Ouaknine and J. Worrell. Positivity problems for low-order linear recurrence sequences.
  Proceedings of SODA 14, 2014.

• V. Chonev, J. Ouaknine, and J. Worrell. The Orbit Problem in higher dimensions.
  Proceedings of STOC 13, 2013.

• J. Ouaknine and J. Worrell. Decision problems for linear recurrence sequences.
  Proceedings of RP 12 (invited paper), LNCS 7550, 2012.

Timed automata and Metric Temporal Logic

• Q. Guilmant and J. Ouaknine. Inapproximability in weighted timed games.
  Proceedings of CONCUR 24, LIPIcs 311, 2024.

• H.-M. Ho, J. Ouaknine, and J. Worrell. On the expressiveness and monitoring of Metric Temporal Logic.
  Logical Methods in Computer Science 15(2), 2019.

• N. Drucker, H.-M. Ho, J. Ouaknine, M. Penn, and O. Strichman. Cyclic-routing of Unmanned Aerial Vehicles.
  Journal of Computer and System Sciences 103, 2019.

• P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, J. Ouaknine, and J. Worrell. Model checking real-time systems.
  Handbook of Model Checking, Springer, 2018.

• P. Bouyer, F. Laroussinie, N. Markey, J. Ouaknine, and J. Worrell. Timed temporal logics.
  Proceedings of Models, Algorithms, Logics and Tools, Springer, 2018.

• R. Lazic, J. Ouaknine, and J. Worrell. Zeno, Hercules and the Hydra: Safety Metric Temporal Logic is ACKERMANN-complete.
  ACM TOCL 17(3), 2016.

• H.-M. Ho and J. Ouaknine. The Cyclic-Routing UAV Problem is PSPACE-complete.
  Proceedings of FOSSACS 15, LNCS 9034, 2015.

• H.-M. Ho, J. Ouaknine, and J. Worrell. Online monitoring of Metric Temporal Logic.
  Proceedings of RV 14, LNCS 8734, 2014.

• D. Bundala and J. Ouaknine. On the complexity of temporal-logic path checking.
  Proceedings of ICALP 14, LNCS 8573, 2014.

• R. Lazic, J. Ouaknine, and J. Worrell. Zeno, Hercules and the Hydra: Downward rational termination is Ackermannian.
  Proceedings of MFCS 13, LNCS 8087, 2013.

• P. Hunter, J. Ouaknine, and J. Worrell. Expressive completeness for Metric Temporal Logic.
  Proceedings of LICS 13, 2013.

• M. Jenkins, J. Ouaknine, A. Rabinovich, and J. Worrell. The Church Synthesis Problem with metric.
  Proceedings of CSL 11, LIPIcs 12, 2011.

• M. Jenkins, J. Ouaknine, A. Rabinovich, and J. Worrell. Alternating timed automata over bounded time.
  Proceedings of LICS 10, 2010.

• J. Ouaknine and J. Worrell. Towards a theory of time-bounded verification.
  Proceedings of ICALP 10 (invited paper), LNCS 6199, 2010.

• C. Haase, J. Ouaknine, and J. Worrell. On process-algebraic extensions of Metric Temporal Logic.
  Reflections on the Work of C.A.R. Hoare, 2010.

• J. Ouaknine, A. Rabinovich, and J. Worrell. Time-bounded verification.
  Proceedings of CONCUR 09, LNCS 5710, 2009.

• J. Ouaknine and J. Worrell. Some recent results in Metric Temporal Logic.
  Proceedings of FORMATS 08 (invited paper), LNCS 5215, 2008.

• P. Bouyer, N. Markey, J. Ouaknine, and J. Worrell. On expressiveness and complexity in real-time model checking.
  Proceedings of ICALP 08, LNCS 5126, 2008.

• P. A. Abdulla, J. Deneux, J. Ouaknine, K. Quaas, and J. Worrell. Universality analysis for one-clock timed automata.
  Fundamenta Informaticae 89(4), 2008.

• S. Adams, J. Ouaknine, and J. Worrell. Undecidability of universality for timed automata with minimal resources.
  Proceedings of FORMATS 07, LNCS 4763, 2007.

• P. Bouyer, N. Markey, J. Ouaknine, and J. Worrell. The cost of punctuality.
  Proceedings of LICS 07, 2007.

• P. A. Abdulla, J. Ouaknine, K. Quaas, and J. Worrell. Zone-based universality analysis for single-clock timed automata.
  Proceedings of FSEN 07, LNCS 4767, 2007.

• J. Ouaknine and J. Worrell. On the decidability and complexity of Metric Temporal Logic over finite words.
  Logical Methods in Computer Science 3(1), 2007.

• J. Ouaknine and J. Worrell. On Metric Temporal Logic and faulty Turing machines.
  Proceedings of FOSSACS 06, LNCS 3921, 2006.

• J. Ouaknine and J. Worrell. Safety Metric Temporal Logic is fully decidable.
  Proceedings of TACAS 06, LNCS 3920, 2006.

• P. A. Abdulla, J. Deneux, J. Ouaknine, and J. Worrell. Decidability and complexity results for timed automata via channel machines.
  Proceedings of ICALP 05, LNCS 3580, 2005.

• J. Ouaknine and J. Worrell. On the decidability of Metric Temporal Logic.
  Proceedings of LICS 05, 2005.

• J. Ouaknine and J. Worrell. On the language inclusion problem for timed automata: Closing a decidability gap.
  Proceedings of LICS 04, 2004.

• J. Ouaknine and J. Worrell. Revisiting digitization, robustness, and decidability for timed automata.
  Proceedings of LICS 03, 2003.

• J. Ouaknine and J. Worrell. Universality and language inclusion for open and closed timed automata.
  Proceedings of HSCC 03, LNCS 2623, 2003.

Software model checking (and related work)

• D. Fried, A. Legay, J. Ouaknine, and M. Y. Vardi. Sequential relational decomposition.
  Logical Methods in Computer Science 18(1), 2022.

• D. Fried, A. Legay, J. Ouaknine, and M. Y. Vardi. Sequential relational decomposition.
  Proceedings of LICS 18, 2018.

• T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for decision problems in Separation Logic with general inductive predicates.
  Proceedings of FOSSACS 14, LNCS 8412, 2014.

• B. Wachter, D. Kroening, and J. Ouaknine. Verifying multithreaded software with Impact.
  Proceedings of FMCAD 13, 2013.

• C. Haase, S. Ishtiaq, J. Ouaknine, and M. J. Parkinson. SeLoger: A tool for graph-based reasoning in Separation Logic.
  Proceedings of CAV 13, LNCS 8044, 2013.

• J. Ouaknine, H. Palikareva, A. W. Roscoe, and J. Worrell. A static analysis framework for livelock freedom in CSP.
  Logical Methods in Computer Science 9(3), 2013.

• P. Armstrong, M. Goldsmith, G. Lowe, J. Ouaknine, H. Palikareva, A. W. Roscoe, and J. Worrell. Recent developments in FDR.
  Proceedings of CAV 12, LNCS 7358, 2012.

• D. Bundala, J Ouaknine, and J Worrell. On the magnitude of completeness thresholds in bounded model checking.
  Proceedings of LICS 12, 2012.

• B. Cook, C. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. Tractable reasoning in a fragment of Separation Logic.
  Proceedings of CONCUR 11, LNCS 6901, 2011.

• J. Ouaknine, H. Palikareva, A. W. Roscoe, and J. Worrell. Static livelock analysis in CSP.
  Proceedings of CONCUR 11, LNCS 6901, 2011. Best Paper Award.

• D. Kroening, J. Ouaknine, O. Strichman, Thomas Wahl, and J. Worrell. Linear completeness thresholds for bounded model checking.
  Proceedings of CAV 11, LNCS 6806, 2011.

• R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady. An abstraction-based decision procedure for bit-vector arithmetic.
  International Journal on Software Tools for Technology Transfer 11(2), 2009.

• R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady. Deciding bit-vector arithmetic with abstraction.
  Proceedings of TACAS 07, LNCS 4424, 2007.

• M. Stokely, S. Chaki, and J. Ouaknine. Parallel assignments in software model checking.
  Proceedings of SVV 05, ENTCS 157(1), 2006.

• S. Chaki, E. M. Clarke, O. Grumberg, J. Ouaknine, N. Sharygina, T. Touili, and H. Veith. State/event software verification for branching-time specifications.
  Proceedings of IFM 05, LNCS 3771, 2005.

• S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha. Concurrent software verification with states, events, and deadlocks.
  Formal Aspects of Computing 17(4), 2005.

• E. M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Computational challenges in bounded model checking.
  International Journal on Software Tools for Technology Transfer 7(2), 2005.

• D. Kroening, J. Ouaknine, S. Seshia, and O. Strichman. Abstraction-based satisfiability solving of Presburger arithmetic.
  Proceedings of CAV 04, LNCS 3114, 2004.

• S. Chaki, E. M. Clarke, J. Ouaknine, and N. Sharygina. Automated, compositional and iterative deadlock detection.
  Proceedings of MEMOCODE 04, 2004.

• S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha. State/event-based software model checking.
  Proceedings of IFM 04, LNCS 2999, 2004.

• S. Chaki, E. M. Clarke, A. Groce, J. Ouaknine, O. Strichman, and K. Yorav. Efficient verification of sequential and concurrent C programs.
  Formal Methods in System Design 25(2-3), 2004.

• E. M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Completeness and complexity of bounded model checking.
  Proceedings of VMCAI 04, LNCS 2937, 2004.

• S. Chaki, J. Ouaknine, K. Yorav, and E. M. Clarke. Automated compositional abstraction refinement for concurrent C programs: A two-level approach.
  Proceedings of SoftMC 03, ENTCS 89(3), 2003.

• E. M. Clarke, A. Fehnker, Z. Han, B. Krogh, J. Ouaknine, O. Stursberg, and M. Theobald. Abstraction and counterexample-guided refinement in model checking of hybrid systems.
  International Journal of Foundations of Computer Science 14(4), 2003.

Probabilistic systems

• G. van Heerdt, J. Hsu, J. Ouaknine, and A. Silva. Convex language semantics for nondeterministic probabilistic automata.
  Proceedings of ICTAC 18, LNCS 11187, 2018.

• M. Bruna, R. Grigore, S. Kiefer, J. Ouaknine, and J. Worrell. Proving the Herman-Protocol Conjecture.
  Proceedings of ICALP 16, LIPIcs 55, 2016.

• S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. Algorithmic probabilistic game semantics: Playing games with automata.
  Formal Methods in System Design 43(2), 2013.

• S. Kiefer, A. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. On the complexity of equivalence and minimisation for Q-weighted automata.
  Logical Methods in Computer Science 9(1), 2013.

• S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. APEX: An analyzer for open probabilistic programs.
  Proceedings of CAV 12, LNCS 7358, 2012.

• S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. On the complexity of the equivalence problem for probabilistic automata.
  Proceedings of FOSSACS 12, LNCS 7213, 2012.

• S. Kiefer, A. S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. Three tokens in Herman's algorithm.
  Formal Aspects of Computing 24(4-6), 2012.

• S. Kiefer, A. Murawski, J. Ouaknine, B. Wachter, and J. Worrell. Language equivalence for probabilistic automata.
  Proceedings of CAV 11, LNCS 6806, 2011.

• S. Kiefer, J. Ouaknine, J. Worrell, and L. Zhang. On stabilization in Herman's algorithm.
  Proceedings of ICALP 11, LNCS 6756, 2011.

• A. Legay, A. S. Murawski, J. Ouaknine, and J. Worrell. On automated verification of probabilistic programs.
  Proceedings of TACAS 08, LNCS 4963, 2008.

• A. S. Murawski and J. Ouaknine. On probabilistic program equivalence and refinement.
  Proceedings of CONCUR 05, LNCS 3653, 2005.

• F. van Breugel, M. W. Mislove, J. Ouaknine, and J. Worrell. Domain theory, testing and simulation for labelled Markov processes.
  Theoretical Computer Science 333(1-2), 2005.

• M. W. Mislove, J. Ouaknine, D. Pavlovic, and J. Worrell. Duality for labelled Markov processes.
  Proceedings of FOSSACS 04, LNCS 2987, 2004.

• M. W. Mislove, J. Ouaknine, and J. Worrell. Axioms for probability and nondeterminism.
  Proceedings of EXPRESS 03, ENTCS 96, 2004.

• F. van Breugel, M. W. Mislove, J. Ouaknine, and J. Worrell. An intrinsic characterization of approximate probabilistic bisimilarity.
  Proceedings of FOSSACS 03, LNCS 2620, 2003.

Infinite-state systems

• A. Lechner, R. Mayr, J. Ouaknine, A. Pouly, and J. Worrell. Model checking flat Freeze LTL on one-counter automata.
  Logical Methods in Computer Science 9(3), 2018.

• D. Bundala and J. Ouaknine. On parametric timed automata and one-counter machines.
  Information and Computation 253, 2017.

• A. Lechner, R. Mayr, J. Ouaknine, A. Pouly, and J. Worrell. Model checking flat Freeze LTL on one-counter automata.
  Proceedings of CONCUR 16, LIPIcs 59, 2016.

• C. Haase, J. Ouaknine, and J. Worrell. Relating reachability problems in timed and counter automata.
  Fundamenta Informaticae 143, 2016.

• A. Lechner, J. Ouaknine, and J. Worrell. On the complexity of linear arithmetic with divisibility.
  Proceedings of LICS 15, 2015.

• D. Bundala and J. Ouaknine. Advances in parametric real-time reasoning.
  Proceedings of MFCS 14, LNCS 8634, 2014.

• T. Brihaye, L. Doyen, G. Geeraerts, J. Ouaknine, J.-F. Raskin, and J. Worrell. Time-bounded reachability for monotonic hybrid automata: Complexity and fixed points.
  Proceedings of ATVA 13, LNCS 8172, 2013.

• C. Haase, J. Ouaknine, and J. Worrell. On the relationship between reachability problems in timed and counter automata.
  Proceedings of RP 12, LNCS 7550, 2012.

• S. Göller, C. Haase, J. Ouaknine, and J. Worrell. Branching-time model checking of parametric one-counter automata.
  Proceedings of FOSSACS 12, LNCS 7213, 2012.

• P. Bouyer, N. Markey, J. Ouaknine, P. Schnoebelen, and J. Worrell. On termination and invariance for faulty channel machines.
  Formal Aspects of Computing 24(4-6), 2012.

• T. Brihaye, L. Doyen, G. Geeraerts, J. Ouaknine, J.-F. Raskin, and J. Worrell. On reachability for hybrid automata over bounded time.
  Proceedings of ICALP 11, LNCS 6756, 2011.

• S. Göller, C. Haase, J. Ouaknine, and J. Worrell. Model checking succinct and parametric one-counter automata.
  Proceedings of ICALP 10, LNCS 6199, 2010.

• C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. Reachability in succinct and parametric one-counter automata.
  Proceedings of CONCUR 09, LNCS 5710, 2009.

• R. Lazic, T. Newcomb, J. Ouaknine, A. W. Roscoe, and J. Worrell. Nets with tokens which carry data (full version).
  Fundamenta Informaticae 88(3), 2008.

• P. Bouyer, N. Markey, J. Ouaknine, Ph. Schnoebelen, and J. Worrell. On termination for faulty channel machines.
  Proceedings of STACS 08, LIPIcs 1, 2008.

• R. Lazic, T. Newcomb, J. Ouaknine, A. W. Roscoe, and J. Worrell. Nets with tokens which carry data.
  Proceedings of ICATPN 07, LNCS 4546, 2007.

Timed CSP

• P. Armstrong, G. Lowe, J. Ouaknine, and A. W. Roscoe. Model checking Timed CSP.
  Proceedings of HOWARD-60, 2012.

• J. Ouaknine and S. Schneider. Timed CSP: A retrospective.
  Proceedings of the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond, ENTCS 162, 2006.

• G. Lowe and J. Ouaknine. On timed models and full abstraction.
  Proceedings of MFPS 05, ENTCS 155, 2006.

• J. Ouaknine and J. Worrell. Timed CSP = closed timed epsilon-automata.
  Nordic Journal of Computing 10, 2003.

• J. Ouaknine. Digitisation and full abstraction for dense-time model checking.
  Proceedings of TACAS 02, LNCS 2280, 2002.

• J. Ouaknine and J. Worrell. Timed CSP = closed timed automata.
  Proceedings of EXPRESS 02, ENTCS 68(2), 2002.

• J. Ouaknine. Discrete analysis of continuous behaviour in real-time concurrent systems.
  Ph.D. Thesis, Oxford University, 2001.

• J. Ouaknine and G. M. Reed. Model checking temporal behaviour in CSP.
  Proceedings of PDPTA 99, 1999.

• J. Ouaknine. A framework for model checking Timed CSP.
  Proceedings of the Colloquium on Applicable Modelling, Verification and Analysis Techniques for Real-Time Systems, The Institution of Electrical Engineers, London, 1999.

Miscellaneous

• H. Palikareva, J. Ouaknine, and A. W. Roscoe. SAT-solving in CSP trace refinement.
  Science of Computer Programming 77, 2012.

• F. Arends, J. Ouaknine, and C. W. Wampler. On searching for small Kochen-Specker vector systems (extended version).
  Proceedings of WG 11, LNCS 6986, 2011.

• P. Hunter, P. Bouyer, N. Markey, J. Ouaknine, and J. Worrell. Computing rational radical sums in uniform TC⁰.
  Proceedings of FSTTCS 10, 2010.

• H. Palikareva, J.Ouaknine, and A. W. Roscoe. Faster FDR counterexample generation using SAT-solving.
  Proceedings of AVOCS 09, 2009.

• I. Lynce and J. Ouaknine. Sudoku as a SAT problem.
  Proceedings of AIMATH 06, 2006.

• K. Martin and J. Ouaknine. Informatic vs. classical differentiation on the real line.
  Proceedings of Domains VI, ENTCS 73, 2004.

• E. M. Clarke, M. Kohlhase, J. Ouaknine, and K. Sutner. System description: Analytica 2.
  Proceedings of CALCULEMUS 03, 2003.