Abstraction and counterexample-guided refinement in model checking of hybrid systems E Clarke, A Fehnker, Z Han, B Krogh, J Ouaknine, O Stursberg, ... International journal of foundations of computer science 14 (04), 583-604, 2003 | 249 | 2003 |

State/event-based software model checking S Chaki, EM Clarke, J Ouaknine, N Sharygina, N Sinha Integrated Formal Methods: 4th International Conference, IFM 2004 …, 2004 | 224 | 2004 |

On the decidability of metric temporal logic J Ouaknine, J Worrell 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05), 188-197, 2005 | 218 | 2005 |

Sudoku as a SAT Problem. I Lynce, J Ouaknine AI&M, 2006 | 210 | 2006 |

Some recent results in metric temporal logic J Ouaknine, J Worrell Formal Modeling and Analysis of Timed Systems: 6th International Conference …, 2008 | 186 | 2008 |

Deciding bit-vector arithmetic with abstraction RE Bryant, D Kroening, J Ouaknine, SA Seshia, O Strichman, B Brady Tools and Algorithms for the Construction and Analysis of Systems: 13th …, 2007 | 183 | 2007 |

Completeness and complexity of bounded model checking E Clarke, D Kroening, J Ouaknine, O Strichman Verification, Model Checking, and Abstract Interpretation: 5th International …, 2004 | 177 | 2004 |

On the decidability and complexity of metric temporal logic over finite words J Ouaknine, J Worrell arXiv preprint cs/0702120, 2007 | 151 | 2007 |

Nets with tokens which carry data R Lazić, T Newcomb, J Ouaknine, AW Roscoe, J Worrell Fundamenta Informaticae 88 (3), 251-274, 2008 | 140* | 2008 |

On the language inclusion problem for timed automata: Closing a decidability gap J Ouaknine, J Worrell Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science …, 2004 | 138 | 2004 |

Positivity problems for low-order linear recurrence sequences J Ouaknine, J Worrell Proceedings of the twenty-fifth annual ACM-SIAM Symposium on Discrete …, 2014 | 125 | 2014 |

Tractable Reasoning in a Fragment of Separation Logic. B Cook, C Haase, J Ouaknine, MJ Parkinson, J Worrell CONCUR 11, 235-249, 2011 | 114 | 2011 |

Reachability in succinct and parametric one-counter automata C Haase, S Kreutzer, J Ouaknine, J Worrell CONCUR 2009-Concurrency Theory: 20th International Conference, CONCUR 2009 …, 2009 | 98 | 2009 |

Efficient verification of sequential and concurrent C programs S Chaki, EM Clarke, A Groce, J Ouaknine, O Strichmann, K Yorav Carnegie Mellon University, 2004 | 98 | 2004 |

On metric temporal logic and faulty Turing machines J Ouaknine, J Worrell FoSSaCS 3921, 217-230, 2006 | 97 | 2006 |

Concurrent software verification with states, events, and deadlocks S Chaki, E Clarke, J Ouaknine, N Sharygina, N Sinha Formal Aspects of Computing 17 (4), 461-483, 2005 | 87 | 2005 |

Revisiting digitization, robustness, and decidability for timed automata J Ouaknine, J Worrell 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings …, 2003 | 83 | 2003 |

Foundations for Decision Problems in Separation Logic with General Inductive Predicates. T Antonopoulos, N Gorogiannis, C Haase, MI Kanovich, J Ouaknine FoSSaCS 14, 411-425, 2014 | 81 | 2014 |

Axioms for probability and nondeterminism M Mislove, J Ouaknine, J Worrell Electronic Notes in Theoretical Computer Science 96, 7-28, 2004 | 80 | 2004 |

Ultimate positivity is decidable for simple linear recurrence sequences J Ouaknine, J Worrell Automata, Languages, and Programming: 41st International Colloquium, ICALP …, 2014 | 73 | 2014 |