---
_id: '4458'
abstract:
- lang: eng
text: 'The success of model checking for large programs depends crucially on the
ability to efficiently construct parsimonious abstractions. A predicate abstraction
is parsimonious if at each control location, it specifies only relationships between
current values of variables, and only those which are required for proving correctness.
Previous methods for automatically refining predicate abstractions until sufficient
precision is obtained do not systematically construct parsimonious abstractions:
predicates usually contain symbolic variables, and are added heuristically and
often uniformly to many or all control locations at once. We use Craig interpolation
to efficiently construct, from a given abstract error trace which cannot be concretized,
a parsominous abstraction that removes the trace. At each location of the trace,
we infer the relevant predicates as an interpolant between the two formulas that
define the past and the future segment of the trace. Each interpolant is a relationship
between current values of program variables, and is relevant only at that particular
program location. It can be found by a linear scan of the proof of infeasibility
of the trace.We develop our method for programs with arithmetic and pointer expressions,
and call-by-value function calls. For function calls, Craig interpolation offers
a systematic way of generating relevant predicates that contain only the local
variables of the function and the values of the formal parameters when the function
was called. We have extended our model checker Blast with predicate discovery
by Craig interpolation, and applied it successfully to C programs with more than
130,000 lines of code, which was not possible with approaches that build less
parsimonious abstractions.'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Kenneth
full_name: McMillan, Kenneth L
last_name: Mcmillan
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In:
ACM; 2004:232-244. doi:10.1145/964001.964021'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Mcmillan, K. (2004). Abstractions
from proofs (pp. 232–244). Presented at the POPL: Principles of Programming Languages,
ACM. https://doi.org/10.1145/964001.964021'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan.
“Abstractions from Proofs,” 232–44. ACM, 2004. https://doi.org/10.1145/964001.964021.
ieee: 'T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, “Abstractions from
proofs,” presented at the POPL: Principles of Programming Languages, 2004, pp.
232–244.'
ista: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs.
POPL: Principles of Programming Languages 232–244.'
mla: Henzinger, Thomas A., et al. *Abstractions from Proofs*. ACM, 2004, pp.
232–44, doi:10.1145/964001.964021.
short: T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, ACM, 2004, pp. 232–244.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:08:57Z
date_published: 2004-04-01T00:00:00Z
date_updated: 2019-08-02T12:38:30Z
day: '01'
doi: 10.1145/964001.964021
extern: 1
month: '04'
page: 232 - 244
publication_status: published
publisher: ACM
publist_id: '270'
quality_controlled: 0
status: public
title: Abstractions from proofs
type: conference
year: '2004'
...