List of main publications



  • A. Bouajjani, W. Boutglay, P. Habermehl. Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. CAV 2022. (Arxiv version)

  • Benedikt Bollig, Manuela-Lidia Grindei and Peter Habermehl. Realizability of Concurrent Recursive Programs. Formal Methods Syst. Des. 53(3): 339-362 (2018) (Link)

  • Steven de Oliveira, Virgile Prevosto, Peter Habermehl and Saddek Bensalem. Left-Eigenvectors Are Certificates of the Orbit Problem. RP 2018: 30-44 (Arxiv version)

  • Constantin Enea, Peter Habermehl, Omar Inverso and Gennaro Parlato. On the path-width of integer linear programming. Inf. Comput. 253: 257-271 (2017) (Link)

  • Mohamed Faouzi Atig, Benedikt Bollig and Peter Habermehl. Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete.. Int. J. Found. Comput. Sci. 28(8): 945-976 (2017) (Link)

  • Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier and Daniel Thoma. Model-Checking Counting Temporal Logics on Flat Structures. CONCUR 2017: 29:1-29:17 (Arxiv version)

  • A. Durand-Gasselin, P. Habermehl. Regular transformations of data words through origin information. FOSSACS 2016. (PDF)

  • P. Habermehl, D. Kuske. On Presburger arithmetic extended with modulo counting quantifiers. FOSSACS 2015. (PDF)

  • B. Bollig, P. Habermehl, M. Leucker, B. Monmege. A Robust Class of Data Languages and an Application to Learning. Logical Methods in Computer Science, Volume 10, Issue 4, Dec. 2014. (Link)

  • N. Decker, P. Habermehl, M. Leucker, D. Thoma. Ordered navigation on data words. (Link). CONCUR 2014.

  • C. Enea, P. Habermehl, O. Inverso, G. Parlato. On the Path-Width of Integer Linear Programming. (Link).

  • N. Decker, P. Habermehl, M. Leucker, D. Thoma. Learning Transparent Data Automata. PETRI NETS 2014, Tunis, Tunisia. (PDF)

  • B. Bollig, P. Habermehl, M. Leucker, B. Monmege. A Fresh Approach to Learning Register Automata. DLT 2013, Marne-la-Vallée, France.

  • A. Durand-Gasselin, P. Habermehl. Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree. STACS 2012, Paris. (short version, preliminary long version)

  • A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract regular (tree) model checking. International Journal on Software Tools for Technology Transfer (STTT), Volume 14, Number 2, 167-191, 2012 (Link)

  • P. Habermehl, L. Holik, J. Simacek, A. Rogalewicz, and T. Vojnar. Forest Automata for Verification of Heap Manipulation. Proc. of 23rd International Conference on Computer Aided Verification---CAV'11, Cliff Lodge, Snowbird, Utah, USA. (Link)
    journal version in Formal Methods in System Design, Springer, 2012 (Link)

  • Mohamed Faouzi Atig, Peter Habermehl. On Yen's Path Logic for Petri Nets. International Journal of Foundations of Computer Science, 22(4), pages 783-799, 2011, (Link)

  • A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, T. Vojnar , Programs with Lists are Counter Automata, Formal Methods in System Design, 2011, 38(2), pages 158-192, 2011. (Link)

  • A. Durand-Gasselin, P. Habermehl. On the use of non-deterministic automata for Presburger Arithmetic. In Proc. of the 21st International Conference on Concurrency Theory , LNCS 6269. Springer-Verlag, 2010. (Link)

  • P. Habermehl, R. Meyer, and H. Wimmel. The downward-closure of Petri net languages. In Proc. of the 37th International Colloquium on Automata, Languages and Programming, ICALP 2010, LNCS. Springer-Verlag, 2010. (PDF)

  • P. Habermehl, R. Iosif, and T. Vojnar. Automata-based Verification of Programs with Tree Updates In Acta Informatica, Volume 47, Number 1, pages 1-31, Springer-Verlag, 2010. Link

  • Mohamed Faouzi Atig, Peter Habermehl. On Yen's Path Logic for Petri Nets Proceedings of RP 2009. LNCS 5643, pages 157-172, Springer-Verlag. (PDF)

  • Benedikt Bollig, Peter Habermehl, Carsten Kern and Martin Leucker. Angluin-Style Learning of NFA. Proceedings of IJCAI 2009 (PDF). Full version as Research Report LSV-08-28, Laboratoire Specification et Verification, ENS Cachan, France, October 2008. (PDF)

  • M. Bozga, P. Habermehl, R. Iosif, F. Konecny, and T. Vojnar. Automatic Verification of Integer Array Programs. In 21st International Conference on Computer Aided Verification---CAV'09, LNCS 5643, pages 157-172, Springer-Verlag.

  • Peter Habermehl and Tomas Vojnar (eds.). Proceedings of the 10th International Workshop on Verification of Infinite State Systems (INFINITY'08), Toronto, Canada, August 2008, Electr. Notes Theor. Comput. Sci. 239: 1-3. Elsevier Science Publishers, 2009.

  • Benedikt Bollig, Manuela-Lidia Grindei and Peter Habermehl. Realizability of Concurrent Recursive Programs. In Luca de Alfaro (ed.), FoSSaCS'09, LNCS 5504, pages 410-424. Springer, 2009. (PDF)

  • Mohamed Faouzi Atig, Benedikt Bollig and Peter Habermehl. Emptiness of multi-pushdown automata is 2ETIME-complete. In Masami Ito and Masafumi Toyama (eds.), DLT'08, LNCS 5257, pages 121-133. Springer, 2008.(PDF)

  • P. Habermehl, R. Iosif, and T. Vojnar. A Logic of Singly Indexed Arrays. In Proc. of 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning---LPAR'08, Doha, Qatar, volume 5330 of LNAI, pages 558--573, 2008. Springer-Verlag. An extended version appeared as the technical report TR-2008-9, Verimag, Grenoble, France, 2008.(PDF)

  • Ahmed Bouajjani, Peter Habermehl, Lukas Holik, Tayssir Touili and Tomas Vojnar. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In Oscar H. Ibarra and Bala Ravikumar (eds.), CIAA'08, LNCS 5148, pages 57-67. Springer-Verlag, 2008.(PDF)

  • Ahmed Bouajjani, Peter Habermehl and Tomas Vojnar. Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods in System Design 32(2), pages 129-172, 2008. Link

  • Peter Habermehl, Radu Iosif and Tomas Vojnar. What else is decidable about arrays? In Roberto Amadio (ed.), FoSSaCS'08, LNCS 4962, pages 474-489. Springer, 2008. (PDF)

  • Peter Habermehl, Radu Iosif, Adam Rogalewicz and Tomas Vojnar. Proving Termination of Tree Manipulating Programs. In Kedar Namjoshi and Tomohiro Yoneda (eds.), ATVA'07, LNCS 4762, pages 145-161. Springer, 2007. An extended version appeared as the Verimag Technical Report TR-2007-1

  • Ahmed Bouajjani, Peter Habermehl, Yan Jurski and Mihaela Sighireanu. Rewriting Systems with Data - A Framework for Reasoning About Systems with Unbounded Structures over Infinite Data Domains. In Erzsebet Csuhaj-Varju and Zoltan Esik (eds.), FCT'07, LNCS 4639, pages 1-22. Springer, 2007. Invited paper. (PDF)

  • A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar , Abstract Tree Regular Model Checking of Complex Dynamic Data Structures , In Proc. Intern. Static Analysis Symposium (SAS'06), LNCS 4134, pages 52-70. Springer, 2006, Seoul (Korea). ( gziped PostScript )

  • A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, T. Vojnar , Programs with Lists are Counter Automata , In Thomas Ball and Robert B. Jones (eds.), CAV'06, LNCS 4144, pages 517-531. Springer, Seattle (USA), August 2006. (PDF)

  • P. Habermehl, R. Iosif, and T. Vojnar. Automata-based Verification of Programs with Tree Updates In Proc. 12th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06) LNCS 3920, Vienna (Austria), April 2006. ( gziped PostScript )

  • A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract Regular Tree Model Checking. To appear in Proc. of 7th International Workshop on Verification of Infinite-State Systems Infinity'05 and in ENTCS ( gziped PostScript )

  • A. Bouajjani, P. Habermehl, P. Moro T. Vojnar, Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking , In Proc. 11th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05) LNCS 3440, Edinburgh (UK), April 2005. ( gziped PostScript )

  • P. Habermehl, T. Vojnar, Regular Model Checking using inference of regular languages, In Proc. Infinity Workshop, London (UK), September 2004. (preliminary version: gziped PostScript )

  • Anca Muscholl, Thomas Schwentick, Helmut Seidl, Peter Habermehl, Counting in Trees for free, in Proc. 31st Intern. Coll. on Automata, Languages and Programming , Turku (Finland), July 2004. ( gziped PostScript )

  • A. Bouajjani, P. Habermehl, T. Vojnar, Abstract Regular Model Checking, In Proc. 16th Intern. Conf. on Computer Aided Verification (CAV'04) , LNCS, Boston (Ma, USA), July 2004. ( gziped PostScript )

  • A. Bouajjani, P. Habermehl, T. Vojnar , Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management , in Proc. Intern. Conf. on Concurrency Theory (CONCUR'03) , LNCS 2761, Marseille (France), September 2003. ( gziped PostScript )

  • A. Bouajjani, P. Habermehl, R. Mayr , Automatic Verification of Recursive Procedures with one Integer Parameter , in Proc. 26th Intern. Symp. on Mathematical Foundations of Computer Science (MFCS'01) , LNCS 2136, Marianske Lazne (Czech Republic), August 2001. ( gziped PostScript ). Full version in the journal Theoretical Computer Science , volume 295, 2003. ( gziped PostScript ).

  • Abdulla P.A, Annichini A., Bensalem S., Bouajjani A., Habermehl P., Lakhnech Y. , Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis , in Proc. of 11th Intern. Conf. on Computer Aided Verification (CAV'99) , Lecture Notes in Computer Science, Vol 1633, Trento (Italy), 1999. ( gziped PostScript ).

  • A. Bouajjani, P. Habermehl , Symbolic Reachability Analysis of Fifo-Channel Systems with Nonregular Sets of Configurations , in Proc. 24th Intern. Coll. on Automata, Languages and Programming (ICALP'97) , LNCS 1256, Bologna (Italy), July 1997.
    Full version in the journal of Theoretical Computer Science , volume 221, number 1/2, pages 221-250, 1999. ( gziped PostScript )

  • P. Habermehl , On the complexity of the linear-time mu-calculus for Petri Nets, in Proc. 18th International Conference on Application and Theory of Petri Nets (ICATPN '97) , LNCS 1248, Toulouse, France), 1997. ( gziped PostScript )

  • A. Bouajjani, P. Habermehl , Constrained Properties, Semilinear Systems, and Petri Nets , in Proc. 7th Intern. Conf. on Concurrency Theory (CONCUR'96) , LNCS 1119, Pisa (Italy), August 1996. ( gziped PostScript )

  • A. Bouajjani, R. Echahed, P. Habermehl , On the Verification Problem of Nonregular Properties for Nonregular Processes , in Proc. 10th IEEE Symp. on Logic in Computer Science (LICS'95) , San Diego (Ca, USA), June 1995.

  • A. Bouajjani, R. Echahed, P. Habermehl , Verifying Infinite State Processes with Sequential and Parallel Composition , in Proc. 22nd ACM Symp. on Principles of Programming Languages (POPL'95) , San Francisco (Ca, USA), January 1995.