Conference item icon

Conference item

More effective interpolations in software model checking

Abstract:

An approach to CEGAR-based model checking which has proved to be successful on large models employs Craig interpolation to efficiently construct parsimonious abstractions. Following this design, we introduce new applications, universal safety interpolant and existential error interpolant, of Craig interpolation that can systematically reduce the program state space to be explored for safety verification. Whenever the universal safety interpolant is implied by the current path, all paths emana...

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

Actions


Access Document


Files:
Publisher copy:
10.1109/ASE.2017.8115631

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Merton College
Role:
Author
National Natural Science Foundation of China More from this funder
National University of Singapore More from this funder
Publisher:
Association for Computing Machinery Publisher's website
Journal:
32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017) Journal website
Host title:
32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017)
Publication date:
2017-10-01
Acceptance date:
2017-07-21
DOI:
Source identifiers:
735472
Pubs id:
pubs:735472
UUID:
uuid:3e2eadf1-8d2c-41e5-9f24-2cc43196d4df
Local pid:
pubs:735472
Deposit date:
2017-10-15

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