Model generation for quantified formulas: a taint-based approach

DOI10.1007/978-3-319-96142-2_19MaRDI QIDQ6039409zbMATH OpenOpenAlexFDO

Authors Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1802.05616

Mathematics Subject Classification ID

Logic in computer science (03B70) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: We focus in this paper on generating models of quantified first-order formulas over built-in theories, which is paramount in software verification and bug finding. While standard methods are either geared toward proving the absence of solution or targeted to specific theories, we propose a generic approach based on a reduction to the quantifier-free case. Our technique allows thus to reuse all the efficient machinery developed for that context. Experiments show a substantial improvement over state-of-the-art methods.

Recommendations

• Satisfiability solving and model generation for quantified first-order logic formulas
• Quantifier instantiation techniques for finite model finding in SMT
• Solving quantified verification conditions using satisfiability modulo theories
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Constraint solving for finite model finding in SMT solvers

Cited in

(4)

• Satisfiability solving and model generation for quantified first-order logic formulas
• Exploring theories with a model-finding assistant
• Trapezoidal generalization over linear constraints
• Not all bugs are created equal, but robust reachability can tell the difference

This page was built for publication: Model generation for quantified formulas: a taint-based approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6039409)