CNRS-LABRI-MVTSI : Jerome LEROUX

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
CNRS-LABRI-MVTSI : Jerome LEROUX

Jerome LEROUX
Full-time researcher at CNRS,

Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Equipe Modelisation, Verification et Test de Systemes Informatises (MVTSI)
Domaine Universitaire
351, cour de la liberation
33405 Talence Cedex
FRANCE

Phone :	+33 54000 3509
Fax :	+33 54000 6669
E-Mail :	jerome DOT leroux AT labri DOT fr
Office :	264

Research Interests

Scale-up formal verification techniques to industrial problems.
Infinite state Model-Checking, Accelerations, Abstract Interpretation : ACI Persée, Tool FAST.
Efficient Symbolic representations, Presburger arithmetics and Number Decision Diagrams.
Validation of floating point programs : ACI V3F.

Seminar

MVTSI Seminar

Stages

Master 2ème année 2006-2007: sujet.
1er année ENS Lyon 2005-2006: sujet.
Master 2ème année 2005-2006: sujet 1, sujet 2.
X 1ème année 2005-2006: sujet 1, sujet 2.
Master 2ème année 2004-2005: sujet 1, sujet 2.

Tools

Tool FAST : Fast Accecleration of Symbolic Transition systems

Publications

NEW !!! The LICS05 paper rewritten from scratch

J. Leroux. Least Significant Digit First Presburger Automata (the arxive version without the indexes arxive, the complete local version), dec. 6, 2006.

Technical Reports (Submitted papers)

J. Leroux. SDA: Serialized Digit Automata. Labri Technical Report 1397-06, Mar. 31, 2006.
J. Leroux. Complete Linear Acceleration for Convex Binary Relations . Labri Technical Report 1387-06, Feb. 20, 2006.
J. Leroux. Regular Acceleration for Number Decision Diagrams. Labri Technical Report 1385-06, Jan. 30, 2006.

Journals

A. Finkel and J. Leroux. The Convex Hull of a Number Decision Diagram is a Computable Polyhedron. Information Processing Letters 96(1), pages 30-35, 2005.

Conferences

S. Bardin, J. Leroux, G. Point. Tool Presentation: FAST Extended Release. In Proc. 18th Conf. Computer Aided Verification (CAV'2006), Seattle, Washington, USA, August 2006 , volume 4144 of Lecture Notes in Computer Science, pages 63-66. Springer, 2006.
S. Bardin, A. Finkel, J. Leroux, P. Schnoebelen. Flat acceleration in symbolic model checking. In Proc. 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, Oct. 2005 , volume 3707 of Lecture Notes in Computer Science, pages 474-488. Springer, 2005.
J. Leroux, G. Sutre. Flat counter automata almost everywhere!. In Proc. 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, Oct. 2005 , volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005.
J. Leroux. A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams. In Proc. 20th IEEE Symp. Logic in Computer Science (LICS'2005), Chicago, USA, Jun. 2005, pages 147-156. IEEE Comp. Soc. Press. 2005.
S. Bardin, A. Finkel, and J. Leroux. FASTer acceleration of counter automata in practice. In Proc. 10th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), Barcelona, Spain, Apr. 2004, volume 2988 of Lecture Notes in Computer Science, pages 576-590. Springer, 2004.
A. Finkel and J. Leroux. Image computation in infinite state model checking. In Proc. 16th Int. Conf. Computer Aided Verification (CAV 2004), Boston, MA, USA, July 2004, volume 3114 of Lecture Notes in Computer Science, pages 361-371. Springer, 2004.
A. Finkel and J. Leroux. Polynomial time image computation with interval-definable counters systems. In Model Checking Software, Proc. 11th Int. SPIN Workshop (SPIN 2004), Barcelona, Spain, Apr. 2004, volume 2989 of Lecture Notes in Computer Science, pages 182-197. Springer, 2004.
J. Leroux. Disjunctive invariants for numerical systems. In Proc. 2nd Int. Symp. Automated Technology for Verification and Analysis (ATVA 2004), Taipei, Taiwan, Nov. 2004, volume 3299 of Lecture Notes in Computer Science, pages 99-107. Springer, 2004.
J. Leroux. The affine hull of a binary automaton is computable in polynomial time. In Proc. 5th Int. Workshop on Verification of Infinite State Systems (INFINITY 2003), Marseille, France, Sep. 2003, volume 98 of Electronic Notes in Theor. Comp. Sci., pages 89-104. Elsevier Science, 2004.
J. Leroux and G. Sutre. On flatness for 2-dimensional vector addition systems with states. In Proc. 15th Int. Conf. Concurrency Theory (CONCUR 2004), London, UK, Aug.-Sep. 2004, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004.
S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Proc. 15th Int. Conf. Computer Aided Verification (CAV 2003), Boulder, CO, USA, July 2003, volume 2725 of Lecture Notes in Computer Science, pages 118-121. Springer, 2003.
A. Finkel and J. Leroux. How to compose Presburger-accelerations: Applications to broadcast protocols. In Proc. 22nd Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS 2002), Kanpur, India, Dec. 2002, volume 2556 of Lecture Notes in Computer Science, pages 145-156. Springer, 2002.
A. Finkel and J. Leroux. A finite covering tree for analysing entropic broadcast protocols. In M. Leuschel, A. Podelski, C. R. Ramakrishnan, and U. Ultes-Nitsche, editors, Proc. Int. Workshop on Verification and Computational Logic (VCL 2000), London, July 2000, 2000. Proceedings published as Report DSSE-TR-2000-6, Univ. Southampton, GB.

Other Publications - Talks

J. Leroux. De l'automate binaire à la formule de Presburger. Invited talk. Groupe de travail Journées des Systèmes Infinis (JSI 2005), Cachan, France, Mar. 2005.
J. Leroux. A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams. Technical report 1251 of Université de Montréal, Montréal, QC Canada, Sep. 2004.
J. Leroux. Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST. Thèse ENS de Cachan, Dec. 2003.
S. Bardin, A. Finkel, J. Leroux, L. Petrucci and L. Worobel. FAST, Users' Manual, Aug. 2003.
A. Finkel and J. Leroux. Acceleration of loops for verification. Invited talk. Workshop on Mathematical Models and Techniques for Analysing Systems, Sep.-Oct. 2002, Univ. Montréal, Canada, October 2002.
J. Leroux. Vérification des systèmes paramétrés. Mémoire de DEA, DEA Algorithmique, Paris, September 1999. 51 pages.