Bjorner, N., Eisenhofer, C., & Kovács, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings
-
Volume:
3185
-
Date (published):
14-Aug-2022
-
Event name:
20th Internal Workshop on Satisfiability Modulo Theories
en
Event date:
11-Aug-2022 - 12-Aug-2022
-
Event place:
Haifa, Israel
-
Number of Pages:
9
-
Publisher:
CEUR-WS.org
-
Peer reviewed:
Yes
-
Keywords:
theory reasoning; lazy encoding; SMT callbacks
en
Abstract:
We present ongoing work on developing a user-propagator framework in SMT solving. We argue that the integration of user-propagators in SMT solving yields an efficient approach towards custom theory reasoning, without bringing fundamental changes in the underlining SMT architecture. We showcase our approach in the SMT solver Z3, provide practical evidence of our work, and also discuss potential venues for further improvements.
en
Research facilities:
Universitäre Service-Einrichtung für Transmissionselektronenmikroskopie
-
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
CC BY 4.0
