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

P. Bacik, T. Karimov, F. Luca, J. Nieuwveld, J. Ouaknine, D. Purser, and J. Worrell. A survey of the Skolem and Positivity Problems for linear recurrence sequences.
Submitted, 2026.

G. Kenison, O. Klurman, E. Lefaucheux, F. Luca, P. Moree, J. Ouaknine, E. C. Sertöz, M. A. Whiteland, and J. Worrell. On the Positivity Problem for second-order holonomic sequences.
Submitted, 2026.
Q. Guilmant, F. Luca, R. Mayr, J. Ouaknine, and J. Worrell. On periodic and aperiodic optimal strategies in solvency games.
Submitted, 2026.
P. Kebis, F. Luca, J. Ouaknine, A. Scoones, and J. Worrell. Transcendence for Pisot morphic words over an algebraic base.
Ergodic Theory and Dynamical Systems, 2026.
P. Bacik, J. Nieuwveld, J. Ouaknine, M. Vahanwala, M. Venkatesh, and E. R. Wieser. On variable-bounded non-linear expansions of Presburger arithmetic.
Proceedings of LICS 26, LIPIcs 380, 2026.
T. Karimov, J. Nieuwveld, and J. Ouaknine. Rich sequences and decidability of logical theories.
Submitted, 2026.
F. Luca, J. Ouaknine, and J. Worrell. Conjectural decidability of the Skolem Problem.
Submitted, 2026.
A. M. Ben-Amram, S. Genaim, J. Ouaknine, and J. Worrell. Termination analysis of linear-constraint programs.
Foundations and Trends in Programming Languages 10(1-2), 2026.
E. C. Sertöz, J. Ouaknine, and J. Worrell. Computing transcendence and linear relations of 1-periods.
Submitted, 2025.
R. Aghamov, C. Baier, T. Karimov, J. Ouaknine, and J. Piribauer. Linear dynamical systems with weight functions.
Nonlinear Analysis: Hybrid Systems 60, 2026.
P. Bacik, J. Ouaknine, D. Purser, and J. Worrell. On the p-adic Skolem Problem.
Proceedings of STACS 26, LIPIcs 364, 2026.
P. Bacik, J. Ouaknine, and J. Worrell. On the complexity of the Skolem Problem at low orders.
Proceedings of SODA 26, 2026.
T. Karimov, J. Nieuwveld, J. Ouaknine, M. Vahanwala, and J. Worrell. Algorithmic applications of Schanuel's Conjecture.
Proceedings of the Colloquium on Principles of Formal Quantitative Analysis, 2025.
F. Luca, J. Ouaknine, and J. Worrell. On large zeros of linear recurrence sequences.
Proceedings of MFCS 25, LIPIcs 345, 2025.
J. Nieuwveld and J. Ouaknine. On expansions of monadic second-order logic with dynamical predicates.
Proceedings of MFCS 25, LIPIcs 345, 2025.
T. Karimov, E. Kelmendi, J. Ouaknine, and J. Worrell. Multiple reachability in linear dynamical systems.
Proceedings of LICS 25, 2025.
F. Luca, J. Ouaknine, and J. Worrell. Transcendence of Hecke-Mahler series.
Bulletin of the London Mathematical Society 57(5), 2025.
N. Fijalkow, E. Lefaucheux, P. Ohlmann, J. Ouaknine, A. Pouly, and J. Worrell. On the Monniaux Problem in abstract interpretation.
Journal of the ACM 72(2), 2025.
Y. Bilu, F. Luca, J. Nieuwveld, J. Ouaknine, and J. Worrell. Twisted rational zeros of linear recurrence sequences.
Journal of the London Mathematical Society 111(3), 2025.
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.
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.
E. Lefaucheux, J. Ouaknine, D. Purser, and J. Worrell. Porous invariants for linear systems.
Formal Methods in System Design 63(1), 2024.
F. Luca, J. Ouaknine, and J. Worrell. On the transcendence of a series related to Sturmian words.
Annali della Scuola Normale Superiore di Pisa, 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.
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, J. Ouaknine, and I. Vialard. The Value Problem for weighted timed games with two clocks is undecidable.
Proceedings of FOSSACS 26, LNCS XXXX, 2026. Best ETAPS Paper Award.
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. 2025 LICS Test-of-Time Award.
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)

R. Aghamov, C. Baier, T. Karimov, R. Majumdar, J. Ouaknine, J. Piribauer, and T. Spork. Model checking Linear Temporal Logic with standpoint modalities.
Proceedings of KR 25, 2025.
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

R. Aghamov, C. Baier, J. Ouaknine, J. Piribauer, M. Vahanwala, and I. Vialard. Temporal properties of conditional independence in Dynamic Bayesian Networks.
Proceedings of AAAI 26, 2026.
G. van Heerdt, J. Hsu, J. Ouaknine, and A. Silva. Convex language semantics for nondeterministic probabilistic automata.
Theoretical Computer Science 1040, 2025.
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.

Back to Joël Ouaknine's home page

Imprint / Data Protection