Publications

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

Timed automata and Metric Temporal Logic

• J. Ouaknine, A. Rabinovich, and J. Worrell. Time-bounded verification.
  Accepted to CONCUR 09, 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)

• 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

• 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

• C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. Reachability in succinct and parametric one-counter automata.
  Accepted to CONCUR 09, 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, 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

• 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.
  Technical Report PRG-RR-01-06, Oxford University Computing Laboratory.

• 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

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

• J. Ouaknine. Book review of "Verification of reactive systems: Formal methods and algorithms" by Klaus Schneider.
  Software Testing, Verification and Reliability 15, 2005.

• 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.