DC Field
Value
Language
dc.contributor.author
Fazekas, Katalin
-
dc.contributor.author
Pollitt, Florian
-
dc.contributor.author
Fleury, Mathias
-
dc.contributor.author
Biere, Armin
-
dc.date.accessioned
2025-01-30T09:30:52Z
-
dc.date.available
2025-01-30T09:30:52Z
-
dc.date.issued
2024-07-23
-
dc.identifier.citation
<div class="csl-bib-body"> <div class="csl-entry">Fazekas, K., Pollitt, F., Fleury, M., &#38; Biere, A. (2024, July 23). <i>Certifying Incremental SAT Solving</i> [Conference Presentation]. 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada. http://hdl.handle.net/20.500.12708/210159</div> </div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/210159
-
dc.description.abstract
Certifying results by checking proofs and models is an essential feature of modern SAT solving. While incremental solving with assumptions and core extraction is crucial for many applications, support for incremental proof certificates remains lacking. We propose a proof format and corresponding checkers for incremental SAT solving. We further extend it to leverage resolution hints. Experiments on incremental SAT solving for Bounded Model Checking and Satisfiability Modulo Theories demonstrate the feasibility of our approach, further confirming that resolution hints substantially reduce checking time.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.subject
Certification
en
dc.subject
Incremental SAT
en
dc.subject
Proof checking
en
dc.title
Certifying Incremental SAT Solving
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.contributor.affiliation
University of Freiburg, Germany
-
dc.contributor.affiliation
University of Freiburg, Germany
-
dc.relation.grantno
T 1306-N
-
dc.type.category
Conference Presentation
-
tuw.project.title
Inkrementelles SAT und SMT für skalierbare Verifikation
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
20
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.author.orcid
0000-0002-0497-3059
-
tuw.author.orcid
0009-0001-4337-6919
-
tuw.author.orcid
0000-0002-1705-3083
-
tuw.author.orcid
0000-0001-7170-9242
-
tuw.event.name
22nd International Workshop on Satisfiability Modulo Theories (SMT 2024)
en
tuw.event.startdate
22-07-2024
-
tuw.event.enddate
23-07-2024
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Montreal
-
tuw.event.country
CA
-
tuw.event.presenter
Fazekas, Katalin
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.grantfulltext
none
-
item.cerifentitytype
Publications
-
item.fulltext
no Fulltext
-
item.openairetype
conference paper not in proceedings
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
item.languageiso639-1
en
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
University of Freiburg
-
crisitem.author.dept
University of Freiburg
-
crisitem.author.dept
University of Freiburg
-
crisitem.author.orcid
0000-0002-0497-3059
-
crisitem.author.orcid
0009-0001-4337-6919
-
crisitem.author.orcid
0000-0002-1705-3083
-
crisitem.author.orcid
0000-0001-7170-9242
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.grantno
T 1306-N
-
Appears in Collections:
Presentation
Show simple item record

Page view(s)

113
checked on Jan 30, 2025

Google ScholarTM

Check