Towards a scalable software model checker for higher-order programs

Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

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

29 Citations (Scopus)

Abstract

In our recent paper, we have shown how to construct a fully- automated program verification tool (so called a "software model checker") for a tiny subset of functional language ML, by combin- ing higher-order model checking, predicate abstraction, and CE- GAR. This can be viewed as a higher-order counterpart of previ- ous software model checkers for imperative languages like BLAST and SLAM. The naïve application of the proposed approach, how- ever, suffered from scalability problems, both in terms of efficiency and supported language features. To obtain more scalable software model checkers for full-scale functional languages, we propose a series of optimizations and extensions of the previous approach. Among others, we introduce (i) selective CPS transformation, (ii) selective predicate abstraction, and (iii) refined predicate discovery as optimization techniques; and propose (iv) functional encoding of recursive data structures and control operations to support a larger subset of ML. We have implemented the proposed methods, and obtained promising results.

Original languageEnglish
Title of host publicationPEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013
Pages53-62
Number of pages10
DOIs
Publication statusPublished - 2013
EventACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013 - Rome, Italy
Duration: Jan 21 2013Jan 22 2013

Publication series

NamePEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013

Other

OtherACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013
CountryItaly
CityRome
Period1/21/131/22/13

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Software

Fingerprint Dive into the research topics of 'Towards a scalable software model checker for higher-order programs'. Together they form a unique fingerprint.

Cite this