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
Authors
Funding
National University of Singapore
More from this funder
National Natural Science Foundation of China
More from this funder
Bibliographic Details
- Publisher:
- Association for Computing Machinery Publisher's website
- Host title:
- 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017)
- Journal:
- 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017) Journal website
- Publication date:
- 2017-10-01
- Acceptance date:
- 2017-07-21
- DOI:
Item Description
- Pubs id:
-
pubs:735472
- UUID:
-
uuid:3e2eadf1-8d2c-41e5-9f24-2cc43196d4df
- Local pid:
- pubs:735472
- Source identifiers:
-
735472
- Deposit date:
- 2017-10-15
Terms of use
- Copyright holder:
- Institute for Electrical and Electronics Engineers
- Copyright date:
- 2017
- Notes:
- © 2017 IEEE
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record