--- res: bibo_abstract: - 'One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.@eng' bibo_authorlist: - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Ranjit foaf_name: Jhala, Ranjit foaf_surname: Jhala - foaf_Person: foaf_givenName: Ritankar foaf_name: Majumdar, Ritankar foaf_surname: Majumdar - foaf_Person: foaf_givenName: Grégoire foaf_name: Sutre, Grégoire foaf_surname: Sutre bibo_doi: 10.1145/503272.503279 dct_date: 2002^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/9781581134506 dct_language: eng dct_publisher: ACM@ dct_title: Lazy abstraction@ ...