
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:
 PC Chair of
SYNASC 2015,
Vampire 2015 and 2014,
iPrA 2015, 2014 and 2013,
SYNASC 2014  Logic and Programming track,
SYNASC 2013  Logic and Programming track,
SCCS 2013,
SYNASC 2012  Logic and Programming track,
WWV 2011 and WWV 2010,
WING
2010, WING 2009
 PC member of the following events:
 2016: POPL 2016,
CAV 2016,
FM 2016
CSL 2016,
CICM 2016
CPP 2016,
TAP 2016,
TASE 2016,
PAAR 2016,
WWV 2016,
ICDCIT 2016;
 2015:
LICS 2015,
CADE 2015,
FM 2015,
LPAR 2015,
HVC 2015,
PSI 2015,
TAPAS 2015,
WWV 2015,
Quantify 2015;

2014:
CSLLICS 2014,
CAV 2014,
SAS 2014,
iFM 2014,
CICM 2014  Calculemus track,
SCSS 2014,
HVC 2014
WING 2014,
VMCAI 2014,
QUANTIFY 2014,
PSI 2014 and 2011,
WWV 2014,
QUANTIFY 2014;

2013:
LPAR 2013,
MACIS 2013,
FTfJP 2013,

2012: CSL 2012,
LPAR 2012,

2011:
ICFEM 2011 ,
PSI 2011, CAI 2011,

2010:
LPAR 2010, Synasc 2010,
ISSAC 2010,

2009:
LPAR 2009,

2007:
Calculemus
2007,
CSR 2007
Community:
Publications:

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 FirstOrder Theorem Proving and TPTP". Proc. of CICM 2015., pp. 7186. (preprint)

P. Cerny, T. A. Henzinger, L. Kovács, A. Radhakrishna and Jakob Zwirchmayr (2015). "Segment Abstraction for WorstCase Execution Time Analysis".
Proc. of ESOP 2015, pp. 105131.

A. Gupta, L. Kovács, B. Kragl and A Voronkov.
"Extensional Crisis and Proving Identity". Proc. of ATVA 2014, pp. 185200.(preprint [pdf])

M. Reza Shoaei, L. Kovács and B. Lennartson.
"Supervisory Control of DiscreteEvent Systems via IC3". Proc. of HVC 2014, pp. 252266. (preprint [pdf])
 L. Kovács and A. Voronkov (2013). "FirstOrder Theorem Proving and Vampire".
Proc. of CAV 2013, pp. 135. (preprint [pdf])
 R. Blanc, A. Gupta, L. Kovács and B. Kragl. "Tree Interpolation in Vampire."
Proc. of LPAR 2013, pp. 173181. (preprint [pdf])
 J. Knoop, L. Kovács and J. Zwirchmayr (2013). "WCET Squeezing: Ondemand Feasibility Refinement for Proven Precise WCETbounds".
Proc. of RTNS 2013, pp. 161170. (preprint [pdf])

A. Biere, J. Knoop, L. Kovács and J. Zwirchmayr (2013). "SmacC: A Retargetable Symbolic Execution Engine".
Proc. of ATVA 2013, pp. 482486. (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. 5363. (preprint [pdf])
 K. Hoder, L. Kovács, and A. Voronkov (2012). "Playing in the Grey Area of Proofs". Proc. of
POPL 2012. pp. 259272. (preprint [pdf])

A. Holzer, K. Hoder, L. Kovács, and A. Voronkov (2012). "Vinter: A VampireBased Tool for Interpolation". Proc. of
APLAS 2012, pp. 148156. (preprint [pdf])

L. Kovács, B. Paláncz and L. Kovács (2012). "Solving Robust GlucoseInsulin Control by Dixon Resultant Computations".
Proc. of SYNASC 2012, pp. 5361. (preprint [pdf])
 J. Knoop, L. Kovács and J. Zwirchmayr (2012). "rTuBound: Loop Bounds for WCET Analysis". Proc. of LPAR 2012, pp. 435444. (preprint [pdf])
 L. Kovács and A. and A. Voronkov (2009)."Interpolation and Symbol
Elimination".
Proc. of CADE 2009,
pp. 199213.
(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. 470485.
(preprint
[pdf])
 L. Kovács (2008). "Invariant Generation for Psolvable Loops with Assignments".
Proc. of CSR 2008, LNCS 5010, pp.
349359.
(preprint
[pdf])
Best paper award.
