Conference item icon

Conference item

Lifting CDCL to template-based abstract domains for program verification

Abstract:

The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis called Abstract Conflict Driven Learning for Programs (ACDLP). ACDLP alternates between model search, which performs over-approximate deduction with constraint propagation, and conflict analysis, which performs under-approximate abduction with heuristic choice. We instantiate the model search and conflict analysis algor...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-319-68167-2_21

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Oxford college:
Balliol College
Role:
Author
More from this funder
Grant:
280053 (CPROVER), the H2020 FET OPEN 712689 SC2
Publisher:
Springer, Cham Publisher's website
Journal:
15th International Symposium on Automated Technology for Verification and Analysis: ATVA 2017 Journal website
Volume:
10482
Pages:
307-326
Series:
Lecture Notes in Computer Science
Host title:
ATVA 2017: Automated Technology for Verification and Analysis
Publication date:
2017-09-27
Acceptance date:
2017-06-15
DOI:
ISSN:
0302-9743
Source identifiers:
707826
ISBN:
9783319681672
Pubs id:
pubs:707826
UUID:
uuid:396f9644-1bb7-43b8-9f90-74d424553d7f
Local pid:
pubs:707826
Deposit date:
2017-07-12

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP