<div class="csl-bib-body">
<div class="csl-entry">Bjørner, N., Eisenhofer, C., & Kovács, L. (2023). Satisfiability Modulo Custom Theories in Z3. In C. Dragoi, M. Emmi, & J. Wang (Eds.), <i>Verification, Model Checking, and Abstract Interpretation. VMCAI 2023</i> (pp. 91–105). Springer. https://doi.org/10.1007/978-3-031-24950-1_5</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/175984
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by-sa/4.0/
-
dc.subject
SMT solving
en
dc.subject
SMT theories
en
dc.subject
Automated reasoning
en
dc.subject
Program verification
en
dc.title
Satisfiability Modulo Custom Theories in Z3
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung - Weitergabe unter gleichen Bedingungen 4.0 International
de
dc.rights.license
Creative Commons Attribution - ShareAlike 4.0 International
en
dc.contributor.affiliation
Microsoft Research New England (United States), United States of America (the)
-
dc.relation.isbn
978-3-031-24950-1
-
dc.description.startpage
91
-
dc.description.endpage
105
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dcterms.dateSubmitted
2023
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Verification, Model Checking, and Abstract Interpretation. VMCAI 2023
-
tuw.container.volume
13881
-
tuw.relation.publisher
Springer
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.researchTopic.id
C4
-
tuw.researchTopic.name
Mathematical and Algorithmic Foundations
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1007/978-3-031-24950-1_5
-
dc.description.numberOfPages
15
-
tuw.author.orcid
0000-0002-1695-2810
-
tuw.author.orcid
0000-0003-0339-1580
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
CC BY-SA 4.0
de
dc.rights.identifier
CC BY-SA 4.0
en
tuw.event.name
International Conference on Verification, Model Checking, and Abstract Interpretation 2023
-
tuw.event.startdate
16-01-2023
-
tuw.event.enddate
17-01-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Boston
-
tuw.event.country
US
-
tuw.event.presenter
Eisenhofer, Clemens
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
restricted
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
crisitem.author.dept
Microsoft Research New England (United States)
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
