Laura Kovács

Laura Ildikó Kovács (* 26. April 1980 in Reșița[1]) ist eine aus dem Banat stammende ungarische Informatikerin und Universitätsprofessorin.

Leben

2002 schloss sie ihr Studium der Mathematik und Informatik an der West-Universität Temeswar ab, 2004 erwarb sie dort einen Master-Abschluss in Informatik. Von 2003 bis 2007 war sie Lehrassistentin an der Fakultät für Mathematik und Informatik der Universität Timisoara und promovierte gleichzeitig an der Universität Linz und am Forschungsinstitut RISC. 2007 schloss sie ihr Doktorat an der Johannes-Kepler-Universität Linz mit ihrer Arbeit „Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema“ ab. Von 2007 bis 2010 war sie Postdoktorandin an der EPFL in Lausanne[2] und anschließend an der ETH Zürich. Seit 2010 arbeitet sie an der Technischen Universität Wien, wo sie sich 2012 habilitierte und seit 2016 als Universitätsprofessorin tätig ist.

2025 gewann zum ersten Mal in der Geschichte der CADE ATP System Competition (CASC) der von Kovács mitentwickelte automatisierte Theorembeweiser VAMPIRE bei der 30. Ausgabe der CASC alle acht Wettbewerbskategorien. Dabei konnte VAMPIRE mehr Probleme lösen als alle anderen teilnehmenden Systeme zusammen.[3]

Forschungsgebiete

Formale Softwareverifikation, symbolische Berechnungen (computergestützte Algebra und algorithmische Kombinatorik), automatischer Theorembeweis.

Veröffentlichungen

  • Buchberger, Bruno; Crăciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, Wolfgang: Theorema: Towards computer-aided mathematical theory exploration. J. Appl. Log. 4, No. 4, 470–504 (2006).
  • Kovács, Laura Ildikó; Jebelean, Tudor: Automated generation of loop invariants by recurrence solving in Theorema. An. Univ. Timis., Ser. Mat.-Inform. Spec. Iss. I, 151–166 (2004).
  • Kovács, Laura; Jebelean, Tudor: Practical aspects of imperative program verification in Theorema. An. Univ. Timis., Ser. Mat.-Inform. 41, Spec. Iss., 135–154 (2003).
  • Kovács, Laura; Moser, Georg; Voronkov, Andrei: On transfinite Knuth-Bendix orders. In: Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wroclaw, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer. Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 384–399 (2011).
  • Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Rybalchenko, Andrey: Aligators for arrays (tool paper). In: Fermüller, Christian G. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings. Berlin: Springer. Lecture Notes in Computer Science 6397, 348–356 (2010).
  • Kovács, Laura; Voronkov, Andrei: Interpolation and symbol elimination. In: Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer. Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 199–213 (2009).
  • Knoop, Jens; Kovács, Laura; Zwirchmayr, Jako: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution. J. Symb. Comput. 80, Part 1, 101-124 (2017)
  • Kovács L.: Efficient approximation for counting of formal concepts generated from formal context. Miskolc Math. Notes 19, No. 2, 983-996 (2018).
  • Moosbrugger, Marcel; Bartocci, Ezio; Katoen, Joost-Pieter; Kovács, Laura: The probabilistic termination tool amber. Form. Methods Syst. Des. 61, No. 1, 90-109 (2022).
  • Humenberger, Andreas; Amrollahi, Daneshvar; Bjørner, Nikolaj; Kovács, Laura: Algebra-based reasoning for loop synthesis. Formal Asp. Comput. 34, No. 1, Article No. 4, 31 p. (2022).
  • Jaroschek, Maximilian; Kauers, Manuel; Kovács, Laura: Lonely points in simplices. Discrete Comput. Geom. 69, No. 1, 4-25 (2023).

Einzelnachweise

  1. TU Wien: Univ.Prof. Dipl.-Ing. Dr.techn. Laura Kovacs. tuwien.at, 1. April 2020, abgerufen am 10. September 2025 (englisch).
  2. EPFL = École Polytechnique Fédérale de Lausanne
  3. Riesenerfolg für VAMPIRE bei tuwien.at, am 8. August 2025.