I am an associate professor at Bordeaux INP (ENSEIRB-MATMECA), an engineering school located in Bordeaux (FRANCE) where I teach computer science. I do research at LaBRI as a member, and current head, of the team "Modelling and Technologies for the Verification (MTV)".

ResearchGate GPG public key

International journal papers

• Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, Igor Walukiewicz: Why Liveness for Timed Automata Is Hard, and What We Can Do About It. ACM Trans. Comput. Log. 21(3): 17:1-17:28 (2020) [author's version|publisher's version](Extends FSTTCS'16 paper)
• Shweta Bhandari, Frédéric Herbreteau, Vijay Laxmi, Akka Zemmari, Manoj Singh Gaur, Partha S. Roop: SneakLeak+: Large-scale klepto apps analysis. Future Gener. Comput. Syst. 109: 593-603 (2020) [publisher's version]
• F. Herbreteau, B. Srivathsan and I. Walukiewicz. Better Abstractions for Timed Automata. Information and Computation, 2016. [authors' version | publisher's version] (Long version of LICS'12 paper)
• F. Herbreteau and B. Srivathsan. Coarse Abstrations Make Zeno Behaviors Difficult to Detect. Logical Methods in Computer Science 9(1), 2013. [authors'/publisher's version] (Special issue - CONCUR'11)
• 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 - 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

• Patricia Bouyer, Paul Gastin, Frédéric Herbreteau, Ocan Sankur, B. Srivathsan: Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next? FORMATS 2022: 16-42 [authors' version]
• Frédéric Herbreteau, B. Srivathsan and Igor Walukiewicz: Checking Timed Büchi Automata Emptiness using the Local-Time Semantics. CONCUR 2022. [publisher's version]
• R. Govind, Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz: Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods. LICS 2022: 24:1-24:14 [authors' version]
• Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol: Certifying Emptiness of Timed Büchi Automata. FORMATS 2020: 58-75 [authors' version | publisher's version] Oded Maler best paper award
• R. Govind, F. Herbreteau, B. Srivathsan and I. Walukiewicz: Revisiting local time semantics for networks of timed automata CONCUR 2019: 16:1--16:15. [authors' version | publisher's version]
• Shweta Bhandari, F. Herbreteau, Vijay Laxmi, Akka Zemmari, Partha S. Roop, Manoj Singh Gaur: POSTER: Detecting Inter-App Information Leakage Paths. AsiaCCS 2017: 908-910. [ authors' version | publisher's version]
• Shweta Bhandari, F. Herbreteau, Vijay Laxmi, Akka Zemmari, Partha S. Roop, Manoj Singh Gaur: SneakLeak: Detecting Multipartite Leakage Paths in Android Apps. TrustCom/BigDataSE/ICESS 2017: 285-292 [ publisher's version]
• F. Herbreteau, B. Srivathsan, T.-T. Tran, I. Walukiewicz: Why Liveness for Timed Automata Is Hard, and What We Can Do About It. FSTTCS 2016: 48:1-48:14, 2016. [ publisher's version]
• F. Herbreteau and T.T. Tran. Improving search order for reachability testing in timed automata Proc. 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2015. [authors' version | publisher's version]
• B. Boigelot, F. Herbreteau and I. Mainz. Acceleration of Affine Hybrid Transformations Proc. 12th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), 2014. [authors' version| publisher's version]
• L. Clemente, F. Herbreteau and G. Sutre. Decidable Topologies for Communicating Automata with FIFO and Bag Channels Proc. 25th Conf. on Concurrency Theory (CONCUR), 2014. [authors' version| publisher's version]
• F. Herbreteau, B. Srivathsan and I. Walukiewicz. Lazy abstractions for timed automata Proc. 25th Int. Conf. on Computer Aided Verification (CAV), 2013. [authors' version| publisher's version]
• L. Clemente, F. Herbreteau, A. Stainer and G. Sutre. Reachability of Communicating Timed Processes. Proc. 16th Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS), 2013. [authors' version| publisher's version]
• 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 | publisher's version] An error in the statement of theorem 34 has been fixed in the 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

Submitted/unpublished manuscripts

• A. Deshpande, F. Herbreteau, B. Srivathsan, T.-T. Tran and I. Walukiewicz. Fast detection of cycles in timed automata. arXiv:1410.4509 (The iterability check has already been published in "R. Jaubert and P.-A. Reynier. Quantitative Robustness Analysis of Flat Timed Automata. FoSSaCS, 2011").