Incremental determinization for quantifier elimination and functional synthesis

DOI10.1007/978-3-030-25543-5_6MaRDI QIDQ6154873zbMATH OpenOpenAlexFDO

Authors Markus Rabe

Publication date 16 February 2024

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_6

Mathematics Subject Classification ID

Logic in computer science (03B70) Quantifier elimination, model completeness, and related topics (03C10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Quantifier Elimination via Functional Composition
• Understanding and extending incremental determinization for 2QBF
• Verification and synthesis using real quantifier elimination
• Incremental determinization
• Syntax-guided quantifier instantiation

Cited in

(3)

• Boolean functional synthesis: from under the hood of solvers
• Partial quantifier elimination and property generation
• Automated synthesis of decision lists for polynomial specifications over integers

This page was built for publication: Incremental determinization for quantifier elimination and functional synthesis

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