2 citations · 2 across the 2 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2025
From MBQI to Enumerative Instantiation and Back
Marek Dančo, Petra Hozzová, Mikoláš Janota
This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at…
cs.LO2024★ 2 cited
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…