Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), Verification, Model Checking, and Abstract Interpretation. VMCAI 2023 (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Verification, Model Checking, and Abstract Interpretation. VMCAI 2023
-
ISBN:
978-3-031-24950-1
-
Volume:
13881
-
Date (published):
Jan-2023
-
Event name:
International Conference on Verification, Model Checking, and Abstract Interpretation 2023
-
Event date:
16-Jan-2023 - 17-Jan-2023
-
Event place:
Boston, United States of America (the)
-
Number of Pages:
15
-
Publisher:
Springer
-
Keywords:
SMT solving; SMT theories; Automated reasoning; Program verification
en
Abstract:
We introduce user-propagators as a new feature of the Z3 SMT solver. User-propagation allows users to write custom theory extensions for Z3, by implementing callbacks via the Z3 API. These callbacks are invoked by Z3 and eliminate eager processing and instantiation of theory axioms with quantifiers. We report on application scenarios of user-propagation and describe further use-cases.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
CC BY-SA 4.0
