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
-
Erschienen in:
Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings
-
Band:
3185
-
Datum (veröffentlicht):
14-Aug-2022
-
Veranstaltungsname:
20th Internal Workshop on Satisfiability Modulo Theories
en
Veranstaltungszeitraum:
11-Aug-2022 - 12-Aug-2022
-
Veranstaltungsort:
Haifa, Israel
-
Umfang:
9
-
Verlag:
CEUR-WS.org
-
Peer Reviewed:
Ja
-
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
Forschungsinfrastruktur:
Universitäre Service-Einrichtung für Transmissionselektronenmikroskopie
-
Projekttitel:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
CC BY 4.0
