Record link: 
http://hdl.handle.net/20.500.12708/189828
-
Title: 
On Incremental Pre-processing for SMT
en
Citation: 
Bjørner, N., & Fazekas, K. (2023). On Incremental Pre-processing for SMT. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 41–60). Springer. https://doi.org/10.1007/978-3-031-38499-8_3
-
Publisher DOI: 
10.1007/978-3-031-38499-8_3
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Bjørner, Nikolaj 
Fazekas, Katalin 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings 
-
ISBN: 
978-3-031-38498-1
-
Volume: 
14132
-
DOI of the book: 
10.1007/978-3-031-38499-8
-
Date (published): 
2-Sep-2023
-
Event name: 
29th International Conference on Automated Deduction 
en
Event date: 
1-Jul-2023 - 4-Jul-2023
-
Event place: 
Rome, Italy
-
Number of Pages: 
20
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
SMT solving; Preprocessing
en
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
Project title: 
Inkrementelles SAT und SMT für skalierbare Verifikation: T1306-N (FWF Fonds zur Förderung der wissenschaftlichen Forschung (FWF)) 
-
Research Areas: 
Mathematical and Algorithmic Foundations: 100%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

135
checked on Nov 23, 2023

Google ScholarTM

Check