6 citations · 11 across the 10 of their papers we have counts for
11 papers
A Modern View on MCSat
Thomas Hader, Theo Jauschneg, Daniela Kaufmann +1
The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear inte…
Saturating Sorting without Sorts
Pamina Georgiou, Márton Hajdu, Laura Kovács
We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formal…
Rewriting and Inductive Reasoning
Márton Hajdu, Laura Kovács, Michael Rawson
Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem…
Spanning Matrices via Satisfiability Solving
Clemens Eisenhofer, Michael Rawson, Laura Kovács
We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour…
MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Thomas Hader, Daniela Kaufmann, Ahmed Irfan +2
This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits…
Linear Loop Synthesis for Quadratic Invariants
S. Hitarth, George Kenison, Laura Kovács +1
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task a…
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Julian Müllner, Marcel Moosbrugger, Laura Kovács
We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decida…
(Un)Solvable Loop Analysis
Daneshvar Amrollahi, Ezio Bartocci, George Kenison +3
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the…
SMT Solving over Finite Field Arithmetic
Thomas Hader, Daniela Kaufmann, Laura Kovács
Non-linear polynomial systems over finite fields are used to model functional behavior of cryptosystems, with applications in system security, computer cryptography, and post-quant…
Automated Sensitivity Analysis for Probabilistic Loops
Marcel Moosbrugger, Julian Müllner, Laura Kovács
We present an exact approach to analyze and quantify the sensitivity of higher moments of probabilistic loops with symbolic parameters, polynomial arithmetic and potentially uncoun…
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
Simon Jeanteur, Laura Kovács, Matteo Maffei +1
Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable au…