Logo EPFL
I&C
Ecole Polytechnique Fédérale de Lausanne
Laura Kovács
english only

LKovacs

Laura Kovács



Starting February 1, 2010, I am affiliated with
Vienna University of Technology.




Research Interests

My research is on program verification. More specifically, combining:
  • automated assertion generation;
  • symbolic summation;
  • computer algebra;
  • automated theorem proving.

Program Committees


Publications

    New!

  • 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])
    Recent

  • 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.

Software

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

Teaching