Frédéric Herbreteau
Maître de Conférences (Associate Professor)
Contact information
Domaine Universitaire
351, cours de la Libération
33405 Talence cedex
FRANCE
room: 263
phone: (+33) 5.40.00.33.36
fax: (+33) 5.40.00.66.69
1, av du Dr. Albert Schweitzer
Domaine Universitaire - BP99
33402 Talence cedex
FRANCE
room: 213
phone: (+33) 5.56.84.23.57
fax: (+33) 5.56.84.23.35
Research interests
My research activity concerns the formal modeling and verification
of computerized systems, mainly model-checking of infinite-state
systems. My goal is to develop new techniques, particularly for
real-time systems, and to scale existing ones to industrial-size
applications. Current topics are:
- Acceleration techniques for the state-space computation of
timed automata and linear hybrid systems
- Efficient algorithms for model-checking timed automata, in
particular, coarse and dynamic abstractions
- Verification of communicating timed automata and
distributed real-time systems
This work is or has been supported by the following projects:
People I work(ed) with:
Publications
International journal papers
-
F. Herbreteau, B. Srivathsan and I. Walukiewicz
Efficient Emptiness Check for Timed Büchi
Automata. Formal Methods in System Design, 40(2),
pp. 122-146, Springer, 2012.
[
authors' version |
publisher's version] (Special issue on
Computer-Aided Verification - CAV'10)
- F. Herbreteau, F. Cassez and O. Roux.
Application of Partial-Order Methods to Reactive Programs
with Event Memorization. Real-time Systems, Kluwer
Academic Publisher, 20(3), pages 287-316, may
2001.
[
authors' version |
publisher's version]
International conference papers
- F. Herbreteau, B. Srivathsan and I. Walukiewicz.
Better abstractions for timed automata. Proc. 27th
ACM/IEEE Symp. on Logic in Computer Science (LICS), 2012.
[authors'
version]
-
F. Herbreteau, D. Kini, B. Srivathsan, I. Walukiewicz.
Using non convex approximations for efficient
analysis of timed automata. Proc. 31st IARCS Annual
Conference on Foundations of Software Technology and
Theoretical Computer Science (FSTTCS), Leibniz
International Proceedings in Informatics (LIPIcs), 2011.
[authors'
version |
publisher's version]
- F. Herbreteau, B. Srivathsan.
Coarse abstractions make Zeno behaviors difficult to
detect. Proc. 22nd
Int. Conf. on Concurrency Theory (CONCUR), 2011.
[authors'
version |
publisher's version]
- F. Herbreteau, B. Srivathsan.
Efficient On-The-Fly Emptiness Check for Timed Büchi
Automata. Proc. of the 8th Int. Symp. on Automated
Technology for Verification and Analysis (ATVA),
2010.
[
authors' version |
publisher's version]
- F. Herbreteau, B. Srivathsan and I. Walukiewicz.
Efficient Emptiness Check for Timed Büchi
Automata. Proc. of the 22nd Int. Conf. on Computer
Aided Verification (CAV),
2010.
[
authors' version |
publisher's version]
- F. Herbreteau, G. Sutre an T.Q. Tran.
Unfolding Concurrent Well-Structured Transition
Systems. Proc. of the 13th Int. Conf. on Tools and
Algorithms for the Construction and Analysis of Systems
(TACAS), LNCS, Springer, Volume 4424, pages 706-720,
Braga, Portugal, mar-apr
2007.
[
authors' version |
publisher's version]
- B. Boigelot and F. Herbreteau.
The Power of Hybrid Acceleration. Proc. of the 18th
Int. Conf. on Computer Aided Verification (CAV), LNCS,
Springer, Volume 4144, pages 438-451, Seattle USA, aug
2006.
[
authors' version |
publisher's version]
- B. Boigelot, F. Herbreteau and S. Jodogne.
Hybrid Acceleration using Real Vector
Automata. Proc. of the 15th Int. Conf. on Computer
Aided Verification (CAV), LNCS, Springer, Volume 2725,
pages 193-205, Boulder USA, jul
2003.
[
authors' version |
publisher's version]
- F. Herbreteau, F. Cassez, A. Finkel, O. Roux and G. Sutre.
Verification of Embedded Reactive Fiffo
Systems. Proc. of the 5th Latin American Conf. in
Theoretical INformatics (LATIN), LNCS, Springer, Volume
2286, pages 400-414, apr
2002.
[
authors' version |
publisher's
version ]
Doctorate thesis (French PhD)
- F. Herbreteau. Automates à file réactifs embarqués -
Application à la vérification de systèmes
temps-réel. Doctorat de l'Université de Nantes et de l'École
Centrale de Nantes. 14 décembre 2001, Nantes, France (in
French). pdf
National workshops and conferences
- F. Herbreteau. Some Properties of Reactive FIFFO
Automata. Modelling and VErification of Parallel Processes
(MOVEP summer school), june 2000, Nantes,
France. pdf
Students
Postdoc/Thesis/Internship proposals
Current students
- B. Srivathsan,
PhD candidate, sep. 2009-now, with Igor Walukiewicz.
Past students
- Aditya Tiwari, undergraduate IIT Bombay internship,
may 2011-jul 2011, "Lazy abstraction of Timed Automata".
- D. Kini, undergraduate internship IIT Bombay,
may-jul. 2010, "Abstraction of Timed Automata", now a graduate
student at University of Illinois at Urbana-Champaign.
- N. Aucouturier, Master Thesis, feb.-jun. 2008,
"Language interpolation for abstraction-based model-checking",
now an engineer at Ausy.
- B. Srivathsan, undergraduate internship IIT Bombay,
may-jul. 2007, "On-The-Fly Emptiness Check for Timed Büchi
Automata", now a PhD student at LaBRI.
- T.Q. Tran, PhD "Unfolding Concurrent Well-Structured
Transition Systems" (19th June 2009), now an engineer at Vietnam
National University.
- S. Gaudan, Master Thesis, feb.-jun. 2004, "Automatic
Abstraction-Refinement for the Verification of Infinite-State
Systems", now an engineer at THALES.