Joël Ouaknine

According to our database1, Joël Ouaknine authored at least 129 papers between 1999 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
On the Expressiveness and Monitoring of Metric Temporal Logic.
Logical Methods in Computer Science, 2019

Cyclic-routing of Unmanned Aerial Vehicles.
J. Comput. Syst. Sci., 2019

On the Decidability of Membership in Matrix-exponential Semigroups.
J. ACM, 2019

The Semialgebraic Orbit Problem.
Proceedings of the 36th International Symposium on Theoretical Aspects of Computer Science, 2019

Termination of Linear Loops over the Integers.
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

On Reachability Problems for Low-Dimensional Matrix Semigroups.
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

On the decidability of reachability in linear time-invariant systems.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

2018
Model Checking Real-Time Systems.
Proceedings of the Handbook of Model Checking., 2018

Reachability Problems 2014: Special issue.
Theor. Comput. Sci., 2018

Polynomial Invariants for Affine Programs.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Sequential Relational Decomposition.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Convex Language Semantics for Nondeterministic Probabilistic Automata.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

O-Minimal Invariants for Linear Loops.
Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, 2018

Effective Divergence Analysis for Linear Recurrence Sequences.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017
On parametric timed automata and one-counter machines.
Inf. Comput., 2017

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem.
Proceedings of the 34th Symposium on Theoretical Aspects of Computer Science, 2017

LICS 2017 foreword.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

The Polytope-Collision Problem.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

On the Polytope Escape Problem for Continuous Linear Dynamical Systems.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

Timed Temporal Logics.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

2016
Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete.
ACM Trans. Comput. Log., 2016

On the Complexity of the Orbit Problem.
J. ACM, 2016

Relating Reachability Problems in Timed and Counter Automata.
Fundam. Inform., 2016

Solvability of Matrix-Exponential Equations.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

On Recurrent Reachability for Continuous Linear Dynamical Systems.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

On the Skolem Problem for Continuous Linear Dynamical Systems.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Proving the Herman-Protocol Conjecture.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Model Checking Flat Freeze LTL on One-Counter Automata.
Proceedings of the 27th International Conference on Concurrency Theory, 2016

2015
On linear recurrence sequences and loop termination.
SIGLOG News, 2015

Reachability problems for Markov chains.
Inf. Process. Lett., 2015

On Matrix Powering in Low Dimensions.
Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science, 2015

On Termination of Integer Linear Loops.
Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, 2015

The Polyhedron-Hitting Problem.
Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, 2015

On the Complexity of Linear Arithmetic with Divisibility.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

The Cyclic-Routing UAV Problem is PSPACE-Complete.
Proceedings of the Foundations of Software Science and Computation Structures, 2015

2014
Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141).
Dagstuhl Reports, 2014

Positivity Problems for Low-Order Linear Recurrence Sequences.
Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, 2014

Online Monitoring of Metric Temporal Logic.
Proceedings of the Runtime Verification - 5th International Conference, 2014

Advances in Parametric Real-Time Reasoning.
Proceedings of the Mathematical Foundations of Computer Science 2014, 2014

Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences.
Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

On the Positivity Problem for Simple Linear Recurrence Sequences, .
Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

On the Complexity of Temporal-Logic Path Checking.
Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

Foundations for Decision Problems in Separation Logic with General Inductive Predicates.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Model checking Timed CSP.
Proceedings of the HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, 2014

2013
Algorithmic probabilistic game semantics - Playing games with automata.
Formal Methods in System Design, 2013

A Static Analysis Framework for Livelock Freedom in CSP
Logical Methods in Computer Science, 2013

On the Complexity of Equivalence and Minimisation for Q-weighted Automata
Logical Methods in Computer Science, 2013

Decision Problems for Linear Recurrence Sequences.
Proceedings of the 5th International Symposium on Symbolic Computation in Software Science, 2013

The orbit problem in higher dimensions.
Proceedings of the Symposium on Theory of Computing Conference, 2013

Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian.
Proceedings of the Mathematical Foundations of Computer Science 2013, 2013

Expressive Completeness for Metric Temporal Logic.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Discrete Linear Dynamical Systems.
Proceedings of the Language and Automata Theory and Applications, 2013

Specification and Verification of Linear Dynamical Systems: Advances and Challenges.
Proceedings of the Frontiers of Combining Systems, 2013

Verifying multi-threaded software with impact.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Decision Problems for Linear Recurrence Sequences.
Proceedings of the Fundamentals of Computation Theory - 19th International Symposium, 2013

SeLoger: A Tool for Graph-Based Reasoning in Separation Logic.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
SAT-solving in CSP trace refinement.
Sci. Comput. Program., 2012

Three tokens in Herman's algorithm.
Formal Asp. Comput., 2012

On termination and invariance for faulty channel machines.
Formal Asp. Comput., 2012

Decision Problems for Linear Recurrence Sequences.
Proceedings of the Reachability Problems - 6th International Workshop, 2012

On the Relationship between Reachability Problems in Timed and Counter Automata.
Proceedings of the Reachability Problems - 6th International Workshop, 2012

On the Magnitude of Completeness Thresholds in Bounded Model Checking.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

On the Complexity of the Equivalence Problem for Probabilistic Automata.
Proceedings of the Foundations of Software Science and Computational Structures, 2012

Branching-Time Model Checking of Parametric One-Counter Automata.
Proceedings of the Foundations of Software Science and Computational Structures, 2012

APEX: An Analyzer for Open Probabilistic Programs.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Recent Developments in FDR.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Preface.
Electr. Notes Theor. Comput. Sci., 2011

On Searching for Small Kochen-Specker Vector Systems.
Proceedings of the Graph-Theoretic Concepts in Computer Science, 2011

On Stabilization in Herman's Algorithm.
Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

On Reachability for Hybrid Automata over Bounded Time.
Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

The Church Synthesis Problem with Metric.
Proceedings of the Computer Science Logic, 2011

Static Livelock Analysis in CSP.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Tractable Reasoning in a Fragment of Separation Logic.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Linear Completeness Thresholds for Bounded Model Checking.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Language Equivalence for Probabilistic Automata.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Alternating Timed Automata over Bounded Time.
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

Towards a Theory of Time-Bounded Verification.
Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Model Checking Succinct and Parametric One-Counter Automata.
Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010

Computing Rational Radical Sums in Uniform TC^0.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010

On Process-Algebraic Extensions of Metric Temporal Logic.
Proceedings of the Reflections on the Work of C. A. R. Hoare., 2010

2009
An abstraction-based decision procedure for bit-vector arithmetic.
STTT, 2009

Faster FDR Counterexample Generation Using SAT-Solving.
ECEASST, 2009

Time-Bounded Verification.
Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

Reachability in Succinct and Parametric One-Counter Automata.
Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

2008
Universality Analysis for One-Clock Timed Automata.
Fundam. Inform., 2008

On Automated Verification of Probabilistic Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

On Termination for Faulty Channel Machines.
Proceedings of the STACS 2008, 2008

On Expressiveness and Complexity in Real-Time Model Checking.
Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

Some Recent Results in Metric Temporal Logic.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2008

2007
On the decidability and complexity of Metric Temporal Logic over finite words.
Logical Methods in Computer Science, 2007

Deciding Bit-Vector Arithmetic with Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

The Cost of Punctuality.
Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

Zone-Based Universality Analysis for Single-Clock Timed Automata.
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

Undecidability of Universality for Timed Automata with Minimal Resources.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2007

Nets with Tokens Which Carry Data.
Proceedings of the Petri Nets and Other Models of Concurrency, 2007

2006
Parallel Assignments in Software Model Checking.
Electr. Notes Theor. Comput. Sci., 2006

Timed CSP: A Retrospective.
Electr. Notes Theor. Comput. Sci., 2006

On Timed Models and Full Abstraction.
Electr. Notes Theor. Comput. Sci., 2006

Safety Metric Temporal Logic Is Fully Decidable.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Sudoku as a SAT Problem.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2006

On Metric Temporal Logic and Faulty Turing Machines.
Proceedings of the Foundations of Software Science and Computation Structures, 2006

2005
Domain theory, testing and simulation for labelled Markov processes.
Theor. Comput. Sci., 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.
Softw. Test., Verif. Reliab., 2005

Computational challenges in bounded model checking.
STTT, 2005

Concurrent software verification with states, events, and deadlocks.
Formal Asp. Comput., 2005

On the Decidability of Metric Temporal Logic.
Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

State/Event Software Verification for Branching-Time Specifications.
Proceedings of the Integrated Formal Methods, 5th International Conference, 2005

Decidability and Complexity Results for Timed Automata via Channel Machines.
Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

On Probabilistic Program Equivalence and Refinement.
Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

2004
Efficient Verification of Sequential and Concurrent C Programs.
Formal Methods in System Design, 2004

Axioms for Probability and Nondeterminism.
Electr. Notes Theor. Comput. Sci., 2004

Informatic vs. Classical Differentiation on the Real Line.
Electr. Notes Theor. Comput. Sci., 2004

Completeness and Complexity of Bounded Model Checking.
Proceedings of the Verification, 2004

Automated, compositional and iterative deadlock detection.
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

State/Event-Based Software Model Checking.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

Duality for Labelled Markov Processes.
Proceedings of the Foundations of Software Science and Computation Structures, 2004

Abstraction-Based Satisfiability Solving of Presburger Arithmetic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Timed CSP = Closed Timed epsilon-automata.
Nord. J. Comput., 2003

Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems.
Int. J. Found. Comput. Sci., 2003

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.
Electr. Notes Theor. Comput. Sci., 2003

Revisiting Digitization, Robustness, and Decidability for Timed Automata.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Universality and Language Inclusion for Open and Closed Timed Automata.
Proceedings of the Hybrid Systems: Computation and Control, 2003

An Intrinsic Characterization of Approximate Probabilistic Bisimilarity.
Proceedings of the Foundations of Software Science and Computational Structures, 2003

2002
Timed CSP = Closed Timed Safety Automata.
Electr. Notes Theor. Comput. Sci., 2002

Digitisation and Full Abstraction for Dense-Time Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

2000
Discrete analysis of continuous behaviour in real-time concurrent systems.
PhD thesis, 2000

1999
Model-Checking Temporal Behaviour in CSP.
Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999


  Loading...