Predicate abstraction and CEGAR for higher-order model checking

Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

Research output: Chapter in Book/Report/Conference proceedingConference contribution

85 Citations (Scopus)

Abstract

Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.

Original languageEnglish
Title of host publicationPLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation
Pages222-233
Number of pages12
DOIs
Publication statusPublished - Jul 7 2011
Externally publishedYes
Event32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'11 - San Jose, CA, United States
Duration: Jun 4 2011Jun 8 2011

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'11
CountryUnited States
CitySan Jose, CA
Period6/4/116/8/11

Fingerprint

Model checking

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Kobayashi, N., Sato, R., & Unno, H. (2011). Predicate abstraction and CEGAR for higher-order model checking. In PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation (pp. 222-233). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/1993498.1993525

Predicate abstraction and CEGAR for higher-order model checking. / Kobayashi, Naoki; Sato, Ryosuke; Unno, Hiroshi.

PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation. 2011. p. 222-233 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kobayashi, N, Sato, R & Unno, H 2011, Predicate abstraction and CEGAR for higher-order model checking. in PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 222-233, 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'11, San Jose, CA, United States, 6/4/11. https://doi.org/10.1145/1993498.1993525
Kobayashi N, Sato R, Unno H. Predicate abstraction and CEGAR for higher-order model checking. In PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation. 2011. p. 222-233. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). https://doi.org/10.1145/1993498.1993525
Kobayashi, Naoki ; Sato, Ryosuke ; Unno, Hiroshi. / Predicate abstraction and CEGAR for higher-order model checking. PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation. 2011. pp. 222-233 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).
@inproceedings{efb4ae2ce77a40b4a0084fb6f3d5b941,
title = "Predicate abstraction and CEGAR for higher-order model checking",
abstract = "Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.",
author = "Naoki Kobayashi and Ryosuke Sato and Hiroshi Unno",
year = "2011",
month = "7",
day = "7",
doi = "10.1145/1993498.1993525",
language = "English",
isbn = "9781450306638",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
pages = "222--233",
booktitle = "PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation",

}

TY - GEN

T1 - Predicate abstraction and CEGAR for higher-order model checking

AU - Kobayashi, Naoki

AU - Sato, Ryosuke

AU - Unno, Hiroshi

PY - 2011/7/7

Y1 - 2011/7/7

N2 - Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.

AB - Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.

UR - http://www.scopus.com/inward/record.url?scp=79959909082&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79959909082&partnerID=8YFLogxK

U2 - 10.1145/1993498.1993525

DO - 10.1145/1993498.1993525

M3 - Conference contribution

AN - SCOPUS:79959909082

SN - 9781450306638

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 222

EP - 233

BT - PLDI'11 - Proceedings of the 2011 ACM Conference on Programming Language Design and Implementation

ER -