Satisfiability Modulo Custom Theories in Z3

Bjørner, Nikolaj; Eisenhofer, Clemens; Kovács, Laura

doi:10.1007/978-3-031-24950-1_5

Record link:

http://hdl.handle.net/20.500.12708/175984

Title:

Satisfiability Modulo Custom Theories in Z3

Citation:

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

Publisher DOI:

10.1007/978-3-031-24950-1_5

Publication Type:

Inproceedings - Full-Paper Contribution

Konferenzbeitrag - Full-Paper Contribution

Language:

English

Authors:

Bjørner, Nikolaj
Eisenhofer, Clemens
Kovács, Laura

Organisational Unit:

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:

Publisher:

Springer

Peer reviewed:

Yes

Keywords:

SMT solving; SMT theories; Automated reasoning; Program verification

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.

Project title:

Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)

Research Areas:

Mathematical and Algorithmic Foundations: 100%

Science Branch:

1020 - Informatik: 100%

License:

CC BY-SA 4.0