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 algebrabased program analysis, loop invariant synthesis, proving loop termination, probablistic programming, SMT solving, firstorder theorem proving, inductive reasoning, and security analysis. 
Group members 

Publications 
2021
The probabilistic termination tool amber
Marcel Moosbrugger, Ezio Bartocci, JoostPieter 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, JoostPieter Katoen, Laura Kovacs. Proc. Of ESOP 2021: The 30th european symposium on programming, pages 491518, 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 123137, 2020. [pdf] [doi]
ProbInG: Distribution recovery for invariant generation of probabilistic programs
Ezio Bartocci, Laura Kovacs, Efstathia Bura. 2020.
Mora  automatic generation of momentbased 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 492498, 2020. [doi]
Algebrabased loop synthesis
Andreas Humenberger, Nikolaj Bjorner, Laura Kovacs. Proceedings of the 16th international conference on integrated formal methods, pages 440459, 2020. [doi]
Subsumption demodulation in firstorder theorem proving
Bernhard Gleiss, Laura Kovacs, Jakob Rath. Proceedings of the 10th international joint conference on automated reasoning (IJCAR), pages 297315, 2020. [pdf] [doi]
Analysis of bayesian networks via probsolvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic. Proc. Of ICTAC 2020: The 17th international colloquium on theoretical aspects of computing, pages 221241, 2020. [doi]
Formalizing graph trail properties in isabelle/HOL
Laura Kovacs, Hanna Elif Lachnitt, Stefan Szeider. CICM 2020: Intelligent computer mathematics, pages 190205, 2020. [pdf] [doi]
Trace logic for inductive loop reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs. Proceedings of the 20th conference on formal methods in computeraided design  FMCAD 2020, pages 255263, 2020. [pdf] [doi] 2019
Foreword
James Davenport, Laura Kovacs, Daniela Zaharie. Mathematics in Computer Science, volume 13, pages 459460, 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 504513, 2019. [pdf] [doi]
Automatic generation of momentbased invariants for probsolvable loops
Ezio Bartocci, Laura Kovacs, Miroslav Stankovic. Proc. Of ATVA 2019: The 17th international symposium on automated technology for verification and analysis, pages 255276, 2019. [pdf] [doi]
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 9599, 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 8591, 2019. [doi]
Foreword  formalization of geometry, automated and interactive geometric reasoning
Pascal Schreck, Tetsuo Ida, Laura Kovacs. Annals of Mathematics and Artificial Intelligence, volume 85, pages 7172, 2019. [pdf] [doi]
Trace reasoning for formal verification using the firstorder 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.
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 170178, 2019. [pdf] [doi] 2018
Invariant generation for multipath loops with polynomial assignments
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs. Verification, model checking, and abstract interpretation  19th international conference, pages 226246, 2018. [pdf] [doi]
Unification with abstraction and theory instantiation in saturationbased 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 322, 2018. [pdf]
Automated reasoning for systems engineering
Laura Kovacs. Foundations of information and knowledge systems (FOIKS) 2018, pages 1, 2018.
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 111117, 2018. [pdf] [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 381399, 2018. [pdf] [doi]
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 405421, 2018. [doi] 2017
Splitting proofs for interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda. Automated deduction  CADE 26  26th international conference on automated deduction, gothenburg, sweden, august 611, 2017, proceedings, pages 291309, 2017. [pdf] [doi]
Replacing conjectures by positive knowledge: Inferring proven precise worstcase execution time bounds using symbolic execution
Jens Knoop, Laura Kovacs, Jakob Zwirchmayr. Journal of Symbolic Computation, volume 80, pages 101124, 2017. [doi]
Instantiation and pretending to be an SMT solver with vampire
Giles Reger, Martin Suda, Andrei Voronkov. 2017.
Polynomial invariant generation for multipath loops
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs. 2017.
Firstorder interpolation and interpolating proof systems
Laura Kovacs, Andrei Voronkov. LPAR21. 21st international conference on logic for programming, artificial intelligence and reasoning, pages 4964, 2017.
A supervisory control algorithm based on propertydirected reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovacs, Bengt Lennartson. 13th international haifa verification conference (HVC), pages 115130, 2017. [doi]
Theoryspecific 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 260270, 2017. [pdf] [doi]
Testing a saturationbased 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 1920, 2017, proceedings, pages 152161, 2017. [pdf] [doi]
Automated generation of nonlinear 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 221228, 2017. [pdf] [doi]
Firstorder 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] 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 5371, 2016. [pdf]
AVATAR modulo theories
Giles Reger, Nikolaj Bjorner, Martin Suda, Andrei Voronkov. GCAI 2016. 2nd global conference on artificial intelligence, pages 3952, 2016. [pdf]
New techniques in clausal form generation
Giles Reger, Martin Suda, Andrei Voronkov. GCAI 2016. 2nd global conference on artificial intelligence, pages 1123, 2016. [pdf]
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 313329, 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 2027, 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 3748, 2016. [pdf] [doi]
Finding finite models in multisorted firstorder logic
Giles Reger, Martin Suda, Andrei Voronkov. Theory and applications of satisfiability testing  SAT 2016  19th international conference, bordeaux, france, july 58, 2016, proceedings, pages 323341, 2016. [pdf] [doi] 2012
Vinter: A vampirebased tool for interpolation
Krystof Hoder, Andreas Holzer, Laura Kovacs, Andrei Voronkov. APLAS, pages 148156, 2012. [doi] 2011
Decision procedures in soft, hard and bioware  follow up (dagstuhl seminar 11272)
Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov. Dagstuhl Reports, volume 1, pages 2335, 2011. [pdf] [doi] 