Jérôme Leroux

Vincent Penelle

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Vector Addition System Reversible Reachability Problem

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

On the Context-Freeness Problem for Vector Addition Systems.

[BibT_eX]

[DOI]

Vincent Penelle

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Presburger Vector Addition Systems.

[BibT_eX]

[DOI]

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness.

[BibT_eX]

[DOI]

M. Praveen

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

Acceleration For Presburger Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Verification and Program Transformation, 2013

Acceleration for Petri Nets.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Reachability Analysis of Communicating Pushdown Systems

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Model Checking Vector Addition Systems with one zero-test

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Vector Addition Systems Reachability Problem (A Simpler Solution).

[BibT_eX]

[DOI]

Proceedings of the Turing-100, 2012

2011

Vector Addition System Reachability Problem: A Short Self-contained Proof.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2011

The BINCOA Framework for Binary Code Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2010

Interpolating Quantifier-Free Presburger Arithmetic.

[BibT_eX]

[DOI]

Daniel Kroening

Philipp Rümmer

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Place-Boundedness for Vector Addition Systems with one zero-test.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010

2009

TaPAS: The Talence Presburger Arithmetic Suite.

[BibT_eX]

[DOI]

Gérald Point

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

A Generalization of Semenov's Theorem to Automata over Real Numbers.

[BibT_eX]

[DOI]

Bernard Boigelot

Julien Brusten

Proceedings of the Automated Deduction, 2009

Polynomial Precise Interval Analysis Revisited.

[BibT_eX]

[DOI]

Proceedings of the Efficient Algorithms, 2009

2008

Structural Presburger digit vector automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

FAST: acceleration from theory to practice.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2008

Decomposition of Decidable First-Order Logics over Integers and Reals.

[BibT_eX]

[DOI]

Florent Bouchy

Proceedings of the 15th International Symposium on Temporal Representation and Reasoning, 2008

Accelerating Interpolation-Based Model-Checking.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Convex Hull of Arithmetic Automata.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 15th International Symposium, 2008

2007

Accelerated Data-Flow Analysis.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 14th International Symposium, 2007

Acceleration in Convex Data-Flow Analysis.

[BibT_eX]

[DOI]

Proceedings of the FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 2007

2006

Least Significant Digit First Presburger Automata

[BibT_eX]

[DOI]

CoRR, 2006

FAST Extended Release.

[BibT_eX]

[DOI]

Sébastien Bardin

Gérald Point

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

The convex hull of a regular set of integer vectors is polyhedral and effectively computable.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2005

A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Flat Counter Automata Almost Everywhere!

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2005

Flat Acceleration in Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2005

2004

FASTer Acceleration of Counter Automata in Practice.

[BibT_eX]

[DOI]

Sébastien Bardin

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Polynomial Time Image Computation with Interval-Definable Counters Systems.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2004

On Flatness for 2-Dimensional Vector Addition Systems with States.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

Image Computation in Infinite State Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Disjunctive Invariants for Numerical Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2003

The Affine Hull of a Binary Automaton is Computable in Polynomial Time.

[BibT_eX]

[DOI]

Proceedings of INFINITY 2003, 2003

FAST: Fast Acceleration of Symbolikc Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

How to Compose Presburger-Accelerations: Applications to Broadcast Protocols.

[BibT_eX]

[DOI]