<div class="csl-bib-body">
<div class="csl-entry">Bjørner, N., & Fazekas, K. (2023). On Incremental Pre-processing for SMT. In B. Pientka & C. Tinelli (Eds.), <i>Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings</i> (pp. 41–60). Springer. https://doi.org/10.1007/978-3-031-38499-8_3</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/189828
-
dc.description.abstract
We introduce a calculus for incremental pre-processing for SMT and instantiate it in the context of z3. It identifies when powerful formula simplifications can be retained when adding new constraints. Use cases that could not be solved in incremental mode can now be solved incrementally thanks to the availability of pre-processing. Our approach admits a class of transformations that preserve satisfiability, but not equivalence. We establish a taxonomy of pre-processing techniques that distinguishes cases where new constraints are modified or constraints previously added have to be replayed. We then justify the soundness of the proposed incremental pre-processing calculus.
en
dc.description.sponsorship
FWF Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
-
dc.language.iso
en
-
dc.subject
SMT solving
en
dc.subject
Preprocessing
en
dc.title
On Incremental Pre-processing for SMT
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
Microsoft Research New England (United States), United States of America (the)
-
dc.contributor.editoraffiliation
McGill University, Canada
-
dc.contributor.editoraffiliation
University of Iowa, United States of America (the)
-
dc.relation.isbn
978-3-031-38498-1
-
dc.relation.doi
10.1007/978-3-031-38499-8
-
dc.description.startpage
41
-
dc.description.endpage
60
-
dc.relation.grantno
T1306-N
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings
-
tuw.container.volume
14132
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.project.title
Inkrementelles SAT und SMT für skalierbare Verifikation
-
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-38499-8_3
-
dc.description.numberOfPages
20
-
tuw.author.orcid
0000-0002-1695-2810
-
tuw.editor.orcid
0000-0002-2549-4276
-
tuw.event.name
29th International Conference on Automated Deduction
en
tuw.event.startdate
01-07-2023
-
tuw.event.enddate
04-07-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Rome
-
tuw.event.country
IT
-
tuw.event.presenter
Bjørner, Nikolaj
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
none
-
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
