Automated Program Reasoning

Description

The Automated Program Reasoning - APRe group focuses on the design and development of new theories, technologies, and tools for automating program analysis, with a particular focus on generating and proving program properties that can prevent programmers introducing errors while making changes in their code. The APRe research therefore focuses, among others, on algebra-based program analysis, loop invariant synthesis, proving loop termination, probablistic programming, SMT solving, first-order theorem proving, inductive reasoning, and security analysis.

Group members
PhD student
PhD student
PhD student
PhD student
PhD student
PostDoc researcher
Professor
PhD student
PostDoc researcher
PhD student
PhD student
PostDoc researcher
PhD student
PhD student
Visiting Professor
Publications

2021

The probabilistic termination tool amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of FM 2021: The 24th international symposium of formal methods, 2021.
Automated termination analysis of polynomial probabilistic programs
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovacs.
Proc. Of ESOP 2021: The 30th european symposium on programming, pages 491-518, 2021.
[pdf] [doi]

2020

Induction with generalization in superposition reasoning
Marton Hajdu, Petra Hozzova, Laura Kovacs, Johannes Schoisswohl, Andrei Voronkov.
Proceedings of the 13th international conference on intelligent computer mathematics, pages 123-137, 2020.
[pdf] [doi]
Automating termination analysis of probabilistic programs
Marcel Moosbrugger.
2020.
[pdf]
Mora - automatic generation of moment-based invariants
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of TACAS 2020: The 26th international conference on tools and algorithms for the construction and analysis of systems, pages 492-498, 2020.
[doi]
Algebra-based loop synthesis
Andreas Humenberger, Nikolaj Bjorner, Laura Kovacs.
Proceedings of the 16th international conference on integrated formal methods, pages 440-459, 2020.
[doi]
Subsumption demodulation in first-order theorem proving
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 297-315, 2020.
[pdf] [doi]
ProbInG: Distribution recovery for invariant generation of probabilistic programs
Ezio Bartocci, Laura Kovacs, Efstathia Bura.
2020.
First-order reasoning with aggregates
Sophie Rain.
2020.
[pdf]
Analysis of bayesian networks via prob-solvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ICTAC 2020: The 17th international colloquium on theoretical aspects of computing, pages 221-241, 2020.
[doi]
Formalizing graph trail properties in isabelle/HOL
Laura Kovacs, Hanna Elif Lachnitt, Stefan Szeider.
CICM 2020: Intelligent computer mathematics, pages 190-205, 2020.
[pdf] [doi]
Trace logic for inductive loop reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs.
Proceedings of the 20th conference on formal methods in computer-aided design - FMCAD 2020, pages 255-263, 2020.
[pdf] [doi]

2019

Symbol elimination and vampire
Laura Kovacs.
2019.
Verifying relational properties using trace logic
Laura Kovacs.
2019.
Subsumption demodulation in first-order theorem proving
Jakob Rath.
2019.
Foreword
James Davenport, Laura Kovacs, Daniela Zaharie.
Mathematics in Computer Science, volume 13, pages 459-460, 2019.
[pdf] [doi]
Interactive visualization of saturation attempts in vampire
Bernhard Gleiss, Laura Kovacs, Lena Schnedlitz.
Proceedings of the 15th international conference on integrated formal methods (iFM) 2019, pages 504-513, 2019.
[pdf] [doi]
Automatic generation of moment-based invariants for prob-solvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic.
Proc. Of ATVA 2019: The 17th international symposium on automated technology for verification and analysis, pages 255-276, 2019.
[pdf] [doi]
Formal methods in the digital world (in hungarian)
Laura Kovacs.
2019.
Superposition reasoning about quantified bitvector formulas
David Damestani, Laura Kovacs, Martin Suda.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 95-99, 2019.
[doi]
Portfolio SAT and SMT solving of cardinality constraints in sensor network optimization
Gergely Kovasznai, Krisztian Gajdar, Laura Kovacs.
Proceedings of the 21st international symposium on symbolic and numeric algorithms for scientific computing (SYNASC), 2019, pages 85-91, 2019.
[doi]
First-order interpolation
Laura Kovacs.
2019.
Trace reasoning in formal verification - guiding vampire in induction
Pamina Georgiou.
2019.
Foreword - formalization of geometry, automated and interactive geometric reasoning
Pascal Schreck, Tetsuo Ida, Laura Kovacs.
Annals of Mathematics and Artificial Intelligence, volume 85, pages 71-72, 2019.
[pdf] [doi]
Trace reasoning for formal verification using the first-order superposition calculus
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
2019.
Forward subsumption demodulation - fast conditional rewriting in vampire
Bernhard Gleiss, Laura Kovacs, Jakob Rath.
2019.
First order interpolation
Laura Kovacs.
2019.
Verifying relational properties using trace logic
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei.
Proceedings of formal methods in computer aided design (FMCAD), pages 170-178, 2019.
[pdf] [doi]
60 shades of grey in vampire
Laura Kovacs.
2019.
Subsumption demodulation in first-order theorem proving
Jakob Rath.
2019.
Symbolic computation and automated reasoning for program analysis
Laura Kovacs.
2019.
Interpolation in the grey area of proofs
Laura Kovacs.
2019.
APRe, vampire, welcome in vienna!
Laura Kovacs.
2019.

2018

Symbol elimination in program analysis
Laura Kovacs.
2018.
Symbol elimination for program analysis
Laura Kovacs.
2018.
First-order interpolation
Laura Kovacs.
2018.
Automated reasoning for rigorous systems engineering
Laura Kovacs.
2018.
First-order theorem proving in rigorous systems engineering
Laura Kovacs, Andrei Voronkov.
2018.
Automated reasoning for systems engineering
Laura Kovacs.
2018.
Invariant generation for multi-path loops with polynomial assignments
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Verification, model checking, and abstract interpretation - 19th international conference, pages 226-246, 2018.
[pdf] [doi]
Unification with abstraction and theory instantiation in saturation-based reasoning
Giles Reger, Martin Suda, Andrei Voronkov.
Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pages 3-22, 2018.
[pdf]
Automated reasoning for systems engineering
Laura Kovacs.
Foundations of information and knowledge systems (FOIKS) 2018, pages 1, 2018.
A FOOLish encoding of the next state relations of imperative programs.
Evgenii Kotelnikov, Laura Kovacs, Andrei Voronkov.
Proceedings of the 9th international joint conference on automated reasoning (IJCAR) 2018, pages 405-421, 2018.
[doi]
Loop analysis by quantification over iterations
Bernhard Gleiss, Laura Kovacs, Simon Robillard.
Proceedings of the 22nd international conference on logic for programming, artificial intelligence and reasoning (LPAR), pages 381-399, 2018.
[pdf] [doi]
Vampire 2017. Proceedings of the 4th vampire workshop
Laura Kovacs, Andrei Voronkov.
2018.
[pdf]
Aligator.jl - a julia package for loop invariant generation
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
Proceedings of the 11th international conference on intelligent computer mathematics (CICM), pages 111-117, 2018.
[pdf] [doi]
First-order interpolation in the grey area of proofs
Laura Kovacs.
2018.

2017

First-order interpolation and grey areas of proofs
Laura Kovacs.
Proceedings of the 26th EACSL annual conference on computer science logic (CSL), volume 82, pages 3:1, 2017.
[doi]
Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution
Jens Knoop, Laura Kovacs, Jakob Zwirchmayr.
Journal of Symbolic Computation, volume 80, pages 101-124, 2017.
[doi]
First-order interpolation and interpolating proof systems
Laura Kovacs, Andrei Voronkov.
LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 49-64, 2017.
Algebraic reasoning for program analysis
Laura Kovacs.
2017.
Instantiation and pretending to be an SMT solver with vampire
Giles Reger, Martin Suda, Andrei Voronkov.
2017.
Polynomial invariant generation for multi-path loops
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
2017.
Symbol elimination for program analysis
Laura Kovacs.
2017.
A supervisory control algorithm based on property-directed reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovacs, Bengt Lennartson.
13th international haifa verification conference (HVC), pages 115-130, 2017.
[doi]
Theory-specific reasoning about loops with arrays using vampire
Yuting Chen, Laura Kovacs, Simon Robillard.
Proceedings of the third vampire workshop, 2017.
Coming to terms with quantified reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov.
Proceedings of the 44th ACM SIGPLAN symposium on principles of programming languages (POPL), pages 260-270, 2017.
[pdf] [doi]
Recent improvements of theory reasoning in vampire
Giles Reger, Martin Suda, Andrei Voronkov.
2017.
Testing a saturation-based theorem prover: Experiences and challenges
Giles Reger, Martin Suda, Andrei Voronkov.
Tests and proofs - 11th international conference, TAP 2017, held as part of STAF 2017, marburg, germany, july 19-20, 2017, proceedings, pages 152-161, 2017.
[pdf] [doi]
Automated generation of non-linear loop invariants utilizing hypergeometric sequences
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs.
ISSAC '17 proceedings of the 2017 ACM on international symposium on symbolic and algebraic computation, pages 221-228, 2017.
[pdf] [doi]
Splitting proofs for interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda.
Automated deduction - CADE 26 - 26th international conference on automated deduction, gothenburg, sweden, august 6-11, 2017, proceedings, pages 291-309, 2017.
[pdf] [doi]

2016

A clausal normal form translation for FOOL
Evgenii Kotelnikov, Laura Kovacs, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 53-71, 2016.
[pdf]
AVATAR modulo theories
Giles Reger, Nikolaj Bjorner, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 39-52, 2016.
[pdf]
New techniques in clausal form generation
Giles Reger, Martin Suda, Andrei Voronkov.
GCAI 2016. 2nd global conference on artificial intelligence, pages 11-23, 2016.
[pdf]
Finding finite models in multi-sorted first-order logic
Giles Reger, Martin Suda, Andrei Voronkov.
Theory and applications of satisfiability testing - SAT 2016 - 19th international conference, bordeaux, france, july 5-8, 2016, proceedings, pages 323-341, 2016.
[pdf] [doi]
Symbolic computation and automated reasoning for program analysis
Laura Kovacs.
Proceedings of the 12th international conference on integrated formal methods (iFM), volume 9681, pages 20-27, 2016.
[pdf] [doi]
The vampire and the FOOL
Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov.
Proceedings of the 5th ACM SIGPLAN conference on certified programs and proofs (CPP), pages 37-48, 2016.
[pdf] [doi]
With a timisoara background in the scientific world of computer science and
Laura Kovacs.
2016.
New techniques in clausal form generation
Giles Reger, Martin Suda, Andrei Voronkov.
2016.
Automated reasoning for systems engineering
Laura Kovacs.
2016.
Enjoying research at the intersection of math and computer science
Laura Kovacs.
2016.
First-order theorem proving and vampire
Laura Kovacs.
2016.
Proceedings of the 1st and 2nd vampire workshops
Laura Kovacs, Andrei Voronkov.
2016.
Selecting the selection
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov.
Automated reasoning - 8th international joint conference, IJCAR 2016, coimbra, portugal, june 27 - july 2, 2016, proceedings, pages 313-329, 2016.
[pdf] [doi]

2012

Vinter: A vampire-based tool for interpolation
Krystof Hoder, Andreas Holzer, Laura Kovacs, Andrei Voronkov.
APLAS, pages 148-156, 2012.
[doi]

2011

Decision procedures in soft, hard and bio-ware - follow up (dagstuhl seminar 11272)
Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov.
Dagstuhl Reports, volume 1, pages 23-35, 2011.
[pdf] [doi]