MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)

DOI10.1007/978-3-031-63498-7_23MaRDI QIDQ7034852zbMATH OpenFDO

Authors Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_23

zbMATH Keywords

finite fieldsMCSatpolynomial arithmeticSMT solving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A model-constructing satisfiability calculus
• Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs
• Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
• Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings
• Elimination methods
• Logic for Programming, Artificial Intelligence, and Reasoning
• Satisfiability modulo finite fields
• SMT solving over finite field arithmetic
• Solving bitvectors with MCSAT: explanations from bits and pieces
• Solving non-linear arithmetic
• Solving nonlinear integer arithmetic with MCSAT
• The Knowledge Complexity of Interactive Proof Systems
• Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Pa

Cited in

(1)

• Boosting MCSat modulo nonlinear integer arithmetic via local search

This page was built for publication: MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)

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