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, Springer,
dec. 2011.
[
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, D. Kini, B. Srivathsan, I. Walukiewicz.
Using non convex approximations for efficient
analysis of timed automata (Extended version with
proofs). 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 (Extended version with proofs). 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
Submitted/unpublished manuscripts
Students
Postdoc/Thesis/Internship proposals
Current students
Past students
- Aditya Tiwari, IIT Bombay internship, may 2011-jul
2011, with Igor Walukiewicz.
- 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"
with Emmanuel Fleury, then PhD (not defended),
sep. 2008-sep. 2011, with Marc Zeitoun, 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, sep. 2004-jun. 2009, "Unfolding
Concurrent Well-Structured Transition Systems", 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.