[Chalmers University of

Laura Kovács
Associate Professor
Department of Computer Science and Engineering
Chalmers University of Technology

Email: laura dot kovacs at chalmers dot se
Phone: +46 31 772 1696
Fax: +46 31 772 3663
Office: EDIT 5481
Postal address: EDIT Bldg., Rännvägen 6B, 41296 Gothenburg, Sweden



Research Grants

Student projects



Since April 2016, I am a full professor of computer science at the Faculty of Informatics of the Vienna University of Technology (TU Wien).

I also hold a part-time position as an associate professor at the Chalmers University of Technology.

Research interest:
My research is on formal software analysis and verification. More specifically, I am interested in designing new methods for computer-aided verification by combining:

  • automated theorem proving;
  • automated assertion generation;
  • symbolic computation.

Research Grants:

Research topics for students:
If you are interested in doing a semester project, master thesis or a PhD in formal methods, please contact me! A list of possible project topics can be found here.

Program Committees:



  • W. Ahrendt, L. Kovács and S. Robillard (2015). "Reasoning About Loops Using Vampire in KeY". Proc. of LPAR 2015. To appear.
  • E. Kotelnikov, L. Kovács and Andrei Voronkov (2015). "A First Class Boolean Sort in First-Order Theorem Proving and TPTP". Proc. of CICM 2015., pp. 71-86. (preprint)
  • P. Cerny, T. A. Henzinger, L. Kovács, A. Radhakrishna and Jakob Zwirchmayr (2015). "Segment Abstraction for Worst-Case Execution Time Analysis". Proc. of ESOP 2015, pp. 105-131.
    Recent (selected):
  • A. Gupta, L. Kovács, B. Kragl and A Voronkov. "Extensional Crisis and Proving Identity". Proc. of ATVA 2014, pp. 185-200.(preprint [pdf])
  • M. Reza Shoaei, L. Kovács and B. Lennartson. "Supervisory Control of Discrete-Event Systems via IC3". Proc. of HVC 2014, pp. 252-266. (preprint [pdf])
  • L. Kovács and A. Voronkov (2013). "First-Order Theorem Proving and Vampire". Proc. of CAV 2013, pp. 1-35. (preprint [pdf])
  • R. Blanc, A. Gupta, L. Kovács and B. Kragl. "Tree Interpolation in Vampire." Proc. of LPAR 2013, pp. 173-181. (preprint [pdf])
  • J. Knoop, L. Kovács and J. Zwirchmayr (2013). "WCET Squeezing: On-demand Feasibility Refinement for Proven Precise WCET-bounds". Proc. of RTNS 2013, pp. 161-170. (preprint [pdf])
  • A. Biere, J. Knoop, L. Kovács and J. Zwirchmayr (2013). "SmacC: A Retargetable Symbolic Execution Engine". Proc. of ATVA 2013, pp. 482-486. (preprint [pdf])
  • A. Biere, J. Knoop, L. Kovács and J. Zwirchmayr (2013). "The Auspicious Couple: Symbolic Execution and WCET Analysis". Proc. of WCET 2013, pp. 53-63. (preprint [pdf])
  • K. Hoder, L. Kovács, and A. Voronkov (2012). "Playing in the Grey Area of Proofs". Proc. of POPL 2012. pp. 259-272. (preprint [pdf])
  • A. Holzer, K. Hoder, L. Kovács, and A. Voronkov (2012). "Vinter: A Vampire-Based Tool for Interpolation". Proc. of APLAS 2012, pp. 148-156. (preprint [pdf])
  • L. Kovács, B. Paláncz and L. Kovács (2012). "Solving Robust Glucose-Insulin Control by Dixon Resultant Computations". Proc. of SYNASC 2012, pp. 53-61. (preprint [pdf])
  • J. Knoop, L. Kovács and J. Zwirchmayr (2012). "r-TuBound: Loop Bounds for WCET Analysis". Proc. of LPAR 2012, pp. 435-444. (preprint [pdf])
  • K. Hoder, L. Kovács and A. Voronkov (2011). "Invariant Generation in Vampire". Proc. of TACAS 2011, pp. 60-64. (preprint [pdf])
  • L. Kovács and A. and A. Voronkov (2009)."Interpolation and Symbol Elimination". Proc. of CADE 2009, pp. 199-213. (preprint [pdf])
  • L. Kovács and A. and A. Voronkov (2009). "Finding Loop Invariants for Programs over Arrays Using a Theorem Prover". Proc. of FASE 2009. LNCS 5503, pp. 470-485. (preprint [pdf])
  • L. Kovács (2008). "Invariant Generation for P-solvable Loops with Assignments". Proc. of CSR 2008, LNCS 5010, pp. 349-359. (preprint [pdf])
    Best paper award.