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 |
|
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
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]
ProbInG: Distribution recovery for invariant generation of probabilistic programs
Ezio Bartocci, Laura Kovacs, Efstathia Bura. 2020.
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]
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]
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]
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]
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]
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] 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]
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]
Trace reasoning for formal verification using the first-order superposition calculus
Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei. 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]
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 170-178, 2019. [pdf] [doi] 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.
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]
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]
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] 2017
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]
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]
Polynomial invariant generation for multi-path loops
Andreas Humenberger, Maximilian Jaroschek, Laura Kovacs. 2017.
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.
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]
Instantiation and pretending to be an SMT solver with 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]
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] 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]
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]
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]
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] 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] |