Institute for Computer Languages
Compilers and Languages Group

Laura Kovács

Mailing Address: Compilers and Languages Group Institute for Computer Languages Vienna University of Technology Argentinierstrasse 8/ 4/ E185.1 A-1040 Vienna Austria Phone: +43-1-58801-18516 Fax: +43-1-58801-18598 E-Mail: lkovacs at complang dot tuwien dot ac dot at

---

I am an FWF Hertha Firnberg Research Fellow (Austrian Research Fund) at the Vienna University of Technology (TU Wien).

Curriculum Vitae

Research Interests:
My research is on formal software analysis and verification. More specifically, combining:

• automated assertion generation;
• symbolic summation;
• computer algebra;
• automated theorem proving.

Looking for Master and PhD students:

If you are interested in doing a semester project, master thesis or a PhD with me, please contact me!

A list of possible project topics can be found here.

Program Committees

• PC member of Turing-100, CSL 2012, LPAR 2012, ICFEM 2011 , PSI 2011, CAI 2011, LPAR 2010, Synasc 2010, ISSAC 2010, LPAR 2009, Calculemus 2007, CSR 2007

• Tutorial Chair of SYNASC 2011, SYNASC 2009

• PC Chair of WWV 2011 and WWV 2010, WING 2010, WING 2009

• Workshop Chair of LPAR 2012, LPAR 2010, LPAR 2008

Community

• Austrian Rigorous Systems Engineering (ARiSE)

Publications

• My publication list.

New!

• A. Bonenfant, H. Cass, J. Knoop, L. Ková, M. de Michiel and J. Zwirchmayr (2012). "FFX: A Portable WCET Annotation Language". Proc. of RNTS 2012. To appear.

• K. Hoder, A. Holzer, L. Kovács, and A. Voronkov (2012). "Vinter: A Vampire-Based Tool for Interpolation". Proc. of APLAS 2012. To appear. (preprint [pdf])

• L. Kovács, B. Paláncz, and L. Kovács (2012). "Solving Robust Glucose-Insulin Control by Dixon Resultant Computations". Prof. of SYNASC 2012. To appear. (preprint [pdf])

Recent

• J. Knoop, L. Kovács and J. Zwirchmayr (2011). "r-TuBound: Loop Bounds for WCET Analysis". Proc. of LPAR 2012, pp. 435-444. (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])

• K. Hoder, L. Kovács, and A. Voronkov (2011). "Case Studies on Invariant Generation Using a Saturation Theorem Prover". Proc. of MICAI 2011, pp. 1-15. (preprint [pdf])

• L. Kovács, G. Moser, and A. Voronkov (2011). "On Transfinite Knuth-Bendix Orders". Proc. of CADE 2011, pp. 384-399. (preprint [pdf])

• J. Knoop, L. Kovács and J. Zwirchmayr (2011). "An Evaluation of WCET Analysis using Symbolic Loop Bounds". Proc. of WCET 2011. To appear.

• J. Knoop, L. Kovács and J. Zwirchmayr (2011). "Symbolic Loop Bound Computation for WCET Analysis". Proc. of PSI 2011. To appear. (preprint [pdf])

• K. Hoder, L. Kovács and A. Voronkov (2011). "Invariant Generation in Vampire". Proc. of TACAS 2011, pp. 60-64. (preprint [pdf])

• T. Henzinger, T. Hottelier, L. Kovács and A. Rybalchenko (2010). "Aligators for Arrays". Proc. of LPAR 2010, pp. 348-356. (preprint [pdf])

• R. Blanc, T. Henzinger, T. Hottelier and L. Kovacs (2010). "ABC: Algebraic Loop Bound Computation". Proc. of LPAR 2009. Postproceedings appeared as LNAI 6355, pp. 103-118 (preprint [pdf])

• K. Hoder, L. Kovacs and A. Voronkov (2010). "Symbol Elimination and Interpolation in Vampire". Proc. of IJCAR 2010, pp. 188-195. (preprint [pdf])

• T. Henzinger, T. Hottelier, L. Kovács and A. Voronkov (2010). "Invariant and Type Inference for Matrices". Proc. of VMCAI 2010, pp. 163-179. (preprint [pdf])

• L. Kovács and A. Voronkov (2009). "Interpolation and Symbol Elimination". Proc. of CADE 2009, pp. 199-213. (preprint [pdf])

• L. Kovács (2009). "A Complete Invariant Generation Approach for P-solvable Loops". Proc. of PSI 2009, pp. 184-194. (preprint [pdf])

• L. Kovács 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])
• T. A. Henzinger, T. Hottelier and L. Kovács (2008). "Valigator: A Verification Tool with Bound and Invariant Generation". Proc. of LPAR 2008. LNCS 5330, pp. 333-342. (preprint [pdf])

• L. Kovács (2008). "Aligator: A Mathematica Package for Invariant Generation". Proc. of IJCAR 2008, LNCS 5195, pp. 275-282. (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.
  

• L. Kovács (2008). "Reasoning Algebraically About P-solvable Loops". Proc. of TACAS 2008, LNCS 4963, pp. 249-264. (preprint [pdf])

• List of publications from the RISC homepage.

Software

• ALIGATOR : a Mathematica package for loop invariant generation.
  NEW version of Aligator is now released!

Teaching

• Advanced Theoretical Computer Science - ATCS (Fall 2011, Fall 2010) at TU Wien.

• Software Engineering Seminar (Fall 2009) at ETH Zurich.

• Foundations of Computer Science 1 (Fall 2009) at University of Zurich.

• Advanced Theoretical Computer Science (Spring 2009) at EPFL.

• Basic and Advanced Theoretical Computer Science (Spring 2008) at EPFL.