Publications of Jérôme Leroux with Jérôme Leroux
Books and proceedings

Alain Finkel,
Jérôme Leroux,
and Igor Potapov, editors.
Reachability Problems  6th International Workshop, RP 2012, Bordeaux, France, September 1719, 2012. Proceedings,
volume 7550 of Lecture Notes in Computer Science,
2012.
Springer.
[url]
[doi]
[bib]
Journal articles and book chapters

Alain Finkel and Jérôme Leroux.
Neue, einfache Algorithmen für Petrinetze.
Informatik Spektrum,
37(3):229236,
2014.
[doi]
[bib]

Jérôme Leroux.
Vector Addition System Reversible Reachability Problem.
Logical Methods in Computer Science,
9(1),
2013.
[doi]
[bib]

Alexander Heussner,
Jérôme Leroux,
Anca Muscholl,
and Grégoire Sutre.
Reachability Analysis of Communicating Pushdown Systems.
Logical Methods in Computer Science,
8(3),
2012.
[url]
[pdf]
[doi]
[bib]

Rémi Bonnet,
Alain Finkel,
Jérôme Leroux,
and Marc Zeitoun.
Model Checking Vector Addition Systems with one zerotest.
Logical Methods in Computer Science,
8(2):11,
June 2012.
[url]
[pdf]
[doi]
[bib]

Jérôme Leroux.
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants.
Logical Methods in Computer Science,
6(3):125,
2010.
[pdf]
[doi]
[bib]

Jérôme Leroux.
Structural Presburger Digit Vector Automata.
Theoretical Computer Science,
409(3):549556,
2008.
[pdf]
[doi]
[bib]

Sébastien Bardin,
Alain Finkel,
Jérôme Leroux,
and Laure Petrucci.
FAST: acceleration from theory to practice.
International Journal on Software Tools for Technology Transfer (STTT),
10(5):401424,
2008.
[ps]
[doi]
[bib]

Alain Finkel and Jérôme Leroux.
The convex hull of a regular set of integer vectors is polyhedral and effectively computable.
Information Processing Letters,
96(1):3035,
2005.
[ps]
[doi]
[bib]
Conference articles

Jérôme Leroux and Ph. Schnoebelen.
On Functions Weakly Computable by Petri Nets and Vector Addition Systems.
In Joël Ouaknine,
Igor Potapov,
and James Worrell, editors,
Reachability Problems  8th International Workshop, RP 2014, Oxford, UK, September 2224, 2014. Proceedings,
volume 8762 of Lecture Notes in Computer Science,
pages 190202,
2014.
Springer.
[url]
[doi]
[bib]

Jérôme Leroux,
M. Praveen,
and Grégoire Sutre.
HyperAckermannian bounds for pushdown vector addition systems.
In Thomas A. Henzinger and Dale Miller, editors,
Joint Meeting of the TwentyThird EACSL Annual Conference on Computer Science Logic (CSL) and the TwentyNinth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSLLICS '14, Vienna, Austria, July 14  18, 2014,
pages 63,
2014.
ACM.
[doi]
[bib]

Jérôme Leroux,
Vincent Penelle,
and Grégoire Sutre.
The ContextFreeness Problem Is coNPComplete for Flat Counter Systems.
In Franck Cassez and JeanFrançois Raskin, editors,
Automated Technology for Verification and Analysis  12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 37, 2014, Proceedings,
volume 8837 of Lecture Notes in Computer Science,
pages 248263,
2014.
Springer.
[doi]
[bib]

Jérôme Leroux.
Acceleration For Presburger Petri Nets.
In Alexei Lisitsa and Andrei P. Nemytykh, editors,
First International Workshop on Verification and Program Transformation, VPT 2013, Saint Petersburg, Russia, July 1213, 2013,
volume 16 of EPiC Series,
pages 1012,
2013.
EasyChair.
[url]
[bib]

Jérôme Leroux.
Acceleration for Petri Nets.
In Automated Technology for Verification and Analysis  11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 1518, 2013. Proceedings,
volume 8172 of Lecture Notes in Computer Science,
pages 14,
2013.
Springer.
[doi]
[bib]

Jérôme Leroux,
M. Praveen,
and Grégoire Sutre.
A Relational Trace Logic for Vector Addition Systems with Application to ContextFreeness.
In CONCUR 2013  Concurrency Theory  24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 2730, 2013. Proceedings,
volume 8052 of Lecture Notes in Computer Science,
pages 137151,
2013.
Springer.
[doi]
[bib]

Jérôme Leroux.
Presburger Vector Addition Systems.
In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 2528, 2013,
pages 2332,
2013.
IEEE Computer Society.
[doi]
[bib]

Jérôme Leroux,
Vincent Penelle,
and Grégoire Sutre.
On the ContextFreeness Problem for Vector Addition Systems.
In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 2528, 2013,
pages 4352,
2013.
IEEE Computer Society.
[doi]
[bib]

Jerome Leroux.
Vector Addition Systems Reachability Problem (A Simpler Solution).
In Andrei Voronkov, editor,
The Alan Turing Centenary Conference, Turing100, Manchester UK June 2225, 2012, Proceedings,
volume 10 of EPiC Series,
pages 214228,
2012.
EasyChair.
[url]
[bib]

Jérôme Leroux.
The Vector Addition System Reversible Reachability Problem.
In CONCUR 2011  Concurrency Theory, 22th International Conference, Aachen, Germany, 510 September, 2011, Proceedings,
volume 6901 of Lecture Notes in Computer Science,
pages 327341,
2011.
Springer.
[url]
[doi]
[bib]

Sebastien Bardin,
Philippe Herrmann,
Jérôme Leroux,
Aymeric Vincent,
Olivier Ly,
and Renaud Tabary.
The BINCOA Framework for Binary Code Analysis.
In Computer Aided Verification, 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 1420, 2011, Proceedings,
volume 6806 of Lecture Notes in Computer Science,
2011.
Springer.
Note: To appear.
[bib]

Jérôme Leroux.
Vector Addition System Reachability Problem: A Short Selfcontained Proof.
In Adrian Horia Dediu,
Shunsuke Inenaga,
and Carlos MartìnVide, editors,
Language and Automata Theory and Applications  5th International Conference, LATA 2011, Tarragona, Spain, May 2631, 2011. Proceedings,
volume 6638 of Lecture Notes in Computer Science,
pages 4164,
2011.
Springer.
[url]
[doi]
[bib]

Jérôme Leroux.
Vector addition system reachability problem: a short selfcontained proof.
In Proceedings of the 38th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, Texas, January 2628, 2011,
POPL '11,
pages 307316,
2011.
ACM.
[url]
[doi]
[bib]

Rémi Bonnet,
Alain Finkel,
Jérôme Leroux,
and Marc Zeitoun.
PlaceBoundedness for Vector Addition Systems with one zerotest.
In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 1518, 2010, IMSc, Chennai, India,
volume 8 of Leibniz International Proceedings in Informatics (LIPIcs),
pages 192203,
2010.
Schloss Dagstuhl  LeibnizZentrum fuer Informatik.
[url]
[doi]
[bib]

Daniel Kroening,
Jérôme Leroux,
and Philipp Rümmer.
Interpolating QuantifierFree Presburger Arithmetic.
In Christian G. Fermüller and Andrei Voronkov, editors,
Logic for Programming, Artificial Intelligence, and Reasoning  17th International Conference, LPAR17, Yogyakarta, Indonesia, October 1015, 2010. Proceedings,
volume 6397 of Lecture Notes in Computer Science,
pages 489503,
2010.
Springer.
[pdf]
[doi]
[bib]

Alexander Heussner,
Jérôme Leroux,
Anca Muscholl,
and Grégoire Sutre.
Reachability Analysis of Communicating Pushdown Systems.
In C.H. Luke Ong, editor,
Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 2028, 2010. Proceedings,
volume 6014 of Lecture Notes in Computer Science,
pages 267281,
2010.
Springer.
[pdf]
[doi]
[bib]

Thomas Gawlitza,
Jérôme Leroux,
Jan Reineke,
Helmut Seidl,
Grégoire Sutre,
and Reinhard Wilhelm.
Polynomial Precise Interval Analysis Revisited.
In Susanne Albers,
Helmut Alt,
and Stefan Näher, editors,
Efficient Algorithms, Essays Dedicated to Kurt Mehlhorn on the Occasion of His 60th Birthday, Saarbrücken, Germany, August 27  28, 2009 Proceedings,
volume 5760 of Lecture Notes in Computer Science,
pages 422437,
2009.
Springer.
[pdf]
[doi]
[bib]

Bernard Boigelot,
Julien Brusten,
and Jérôme Leroux.
A Generalization of Semenov's Theorem to Automata over Real Numbers.
In Renate A. Schmidt, editor,
Automated Deduction, 22nd International Conference, CADE 2009, McGill University, Montreal,August 2  7, 2009 Proceedings,
volume 5663 of Lecture Notes in Computer Science,
pages 469484,
2009.
Springer.
[pdf]
[doi]
[bib]

Jérôme Leroux.
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants.
In 24th IEEE Symposium on Logic in Computer Science (LICS 2009), 1114 August 2009, Los Angeles, California, USA, Proceedings,
pages 413,
2009.
IEEE Computer Society.
[pdf]
[bib]

Jérôme Leroux and Gérald Point.
TaPAS : The Talence Presburger Arithmetic Suite.
In Stefan Kowalewski and Anna Philippou, editors,
Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 2229, 2009. Proceedings,
volume 5505 of Lecture Notes in Computer Science,
pages 182185,
2009.
Springer.
[pdf]
[doi]
[bib]

Jérôme Leroux.
Convex Hull of Arithmetic Automata.
In Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, Jully 1618, 2008, Proceedings,
volume 5079 of Lecture Notes in Computer Science,
pages 4761,
2008.
Springer.
[ps]
[doi]
[bib]

Florent Bouchy,
Jérôme Leroux,
and Alain Finkel.
Decomposition of Decidable FirstOrder Logics over Integers and Reals.
In Temporal Representation and Reasoning, 15th International Symposium, TIME 2008, Montréal, Canada, June 16  18, 2008, Proceedings,
pages 147155,
2008.
IEEE Computer Society Press.
[ps]
[doi]
[bib]

Nicolas Caniart,
Emmanuel Fleury,
Jérôme Leroux,
and Marc Zeitoun.
Accelerating Interpolationbased ModelChecking.
In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29  April 6, 2008, Proceedings,
volume 4963 of Lecture Notes in Computer Science,
pages 428442,
2008.
Springer.
[pdf]
[doi]
[bib]

Jérôme Leroux and Grégoire Sutre.
Acceleration in Convex DataFlow Analysis.
In Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, FSTTCS 2007, New Delhi, India, December 1214, 2007, Proceedings,
volume 4855 of Lecture Notes in Computer Science,
pages 520531,
2007.
Springer.
[pdf]
[doi]
[bib]

Jérôme Leroux and Grégoire Sutre.
Accelerated DataFlow Analysis.
In Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 2224, 2007, Proceedings,
volume 4634 of Lecture Notes in Computer Science,
pages 184199,
2007.
Springer.
[pdf]
[doi]
[bib]

Sébastien Bardin,
Jérôme Leroux,
and Gérald Point.
FAST Extended Release.
In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 1720, 2006, Proceedings,
volume 4144 of Lecture Notes in Computer Science,
pages 6366,
2006.
Springer.
[pdf]
[doi]
[bib]

Sébastien Bardin,
Alain Finkel,
Jérôme Leroux,
and Ph. Schnoebelen.
Flat Acceleration in Symbolic Model Checking.
In Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 47, 2005, Proceedings,
volume 3707 of Lecture Notes in Computer Science,
pages 474488,
2005.
Springer.
[pdf]
[doi]
[bib]

Jérôme Leroux and Grégoire Sutre.
Flat Counter Automata Almost Everywhere!.
In Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 47, 2005, Proceedings,
volume 3707 of Lecture Notes in Computer Science,
pages 489503,
2005.
Springer.
[ps]
[doi]
[bib]

Jérôme Leroux.
A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams.
In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2629 June 2005, Chicago, IL, USA, Proceedings,
pages 147156,
2005.
IEEE Computer Society.
[ps]
[doi]
[bib]

Jérôme Leroux.
Disjunctive Invariants for Numerical Systems.
In Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31November 3, 2004. Proceedings,
volume 3299 of Lecture Notes in Computer Science,
pages 93107,
2004.
Springer.
[ps]
[doi]
[bib]

Alain Finkel and Jérôme Leroux.
Image Computation in Infinite State Model Checking.
In Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 1317, 2004, Proceedings,
volume 3114 of Lecture Notes in Computer Science,
pages 361371,
2004.
Springer.
[ps]
[doi]
[bib]

Jérôme Leroux and Grégoire Sutre.
On Flatness for 2Dimensional Vector Addition Systems with States.
In CONCUR 2004  Concurrency Theory, 15th International Conference, London, UK, August 31  September 3, 2004, Proceedings,
volume 3170 of Lecture Notes in Computer Science,
pages 402416,
2004.
Springer.
[ps]
[doi]
[bib]

Alain Finkel and Jérôme Leroux.
Polynomial Time Image Computation with IntervalDefinable Counters Systems.
In Model Checking Software, 11th International SPIN Workshop, Barcelona, Spain, April 13, 2004, Proceedings,
volume 2989 of Lecture Notes in Computer Science,
pages 182197,
2004.
Springer.
[ps]
[doi]
[bib]

Sébastien Bardin,
Alain Finkel,
and Jérôme Leroux.
FASTer Acceleration of Counter Automata in Practice.
In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29  April 2, 2004, Proceedings,
volume 2988 of Lecture Notes in Computer Science,
pages 576590,
2004.
Springer.
[ps]
[doi]
[bib]

Jérôme Leroux.
The Affine Hull of a Binary Automaton is Computable in Polynomial Time.
In Verification of InfiniteState Systems, 5th International Workshop, INFINITY 2003, Held as Part of the Conference on Concurrency Theory, CONCUR 2003, Marseille, France, September 35, 2003, Proceedings,
volume 98 of Electronic Notes Theoritical Computer Science,
pages 89104,
2004.
Elsevier.
[ps]
[doi]
[bib]

Sébastien Bardin,
Alain Finkel,
Jérôme Leroux,
and Laure Petrucci.
FAST: Fast Acceleration of Symbolikc Transition Systems.
In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 812, 2003, Proceedings,
volume 2725 of Lecture Notes in Computer Science,
pages 118121,
2003.
Springer.
[ps]
[doi]
[bib]

Alain Finkel and Jérôme Leroux.
How to Compose PresburgerAccelerations: Applications to Broadcast Protocols.
In Foundations of Software Technology and Theoretical Computer Science, 22th International Conference, FSTTCS 2002, Kanpur, India, December 1214, 2002, Proceedings,
volume 2556 of Lecture Notes in Computer Science,
pages 145156,
2002.
Springer.
[ps]
[doi]
[bib]

Alain Finkel and Jérôme Leroux.
A finite covering tree for analysing entropic broadcast protocols.
In C. R. Ramakrishnan M. Leuschel, A. Podelski and U. UltesNitsche, editors,
International Workshop on Verification and Computational Logic, VCL 2000, London, July 2000, 2000, Proceedings published as Report DSSETR20006, Univ. Southampton, GB,
2000.
[ps]
[bib]
This document was translated from BibT_{E}X by
bibtex2html