Wallenberg Academy Fellowsip 2014

TheProSE: Theorem Proving and Symbol Elimination
for Software Analysis and Verification

Principal Investigator: Laura Kovács
Funding Agency: Knut and Alice Wallenberg Foundation
Project Period: July 2015 - June 2020
Host Institution: Chalmers University of Technology


Project members

Publications

Events

Project publications:

  • Jens Knoop, Laura Kovács, and Jakob Zwirchmayr: "Replacing Conjectures by Positive Knowledge: Inferring Proven Precise Worst-Case Execution Time Bounds Using Symbolic Execution". Journal of Symbolic Computation, 2016. To appear.
  • Laura Kovács: "Symbolic Computation and Automated Reasoning for Program Analysis". Proceedings of the International Conference on integrated Formal Methods (iFM), pages 20-27, volume 9681 of LNCS, 2016.
  • Giles Reger, Martin Suda and Andrei Voronkov: "Finding Finite Models in Multi-Sorted First Order Logic". Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), 2016. To appear. [link]
  • Giles Reger, Martin Suda and Andrei Voronkov: "Selecting the Selection".Proceedings of the 19th International Joint Conference on Automated Reasoning (IJCAR), 2016. To appear\ . [link]
  • Evgenii Kotelnikov, Laura Kovács, Giles Reger and Andrei Voronkov: "The Vampire and the FOOL". Proceedings of the International ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), pages 37-48, ACM, 2016. [link]
  • Wolfgang Ahrendt, Laura Kovács, and Simon Robillard: "Reasoning About Loops Using Vampire in KeY". Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pages 434-443, volume 9450 of LNCS, 2015.
  • Evgenii Kotelnikov, Laura Kovács, and Andrei Voronkov: "A First Class Boolean Sort in First-Order Theorem Proving and TPTP". Proceedings of the International Conference on Intelligent Computer Mathematics (CICM) - Calculemus Track, pages 71-86, volume 9150 of LNCS, 2015. [link]
  • Laura Kovács and Simon Robillard: "Reasoning About Loops Using Vampire". Proceedings of the 1st and 2nd Vampire Workshops, pages 52-62, volume 38 of the EPiC Series in Computing, 2016. [link]