7 citations · 13 across the 3 of their papers we have counts for
3 papers
Program Synthesis in Saturation
Petra Hozzová, Laura Kovács, Chase Norman +1
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-ord…
Getting Saturated with Induction
Márton Hajdu, Petra Hozzová, Laura Kovács +2
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating indu…
Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
Petra Hozzová, Jaroslav Bendík, Alexander Nutz +1
The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproxima…