Verifying relational properties of functional programs by first-order refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

研究成果: Conference contribution

6 被引用数 (Scopus)

抄録

Much progress has been made recently on fully automated verification of higher-order functional programs, based on refinement types and higher-order model checking. Most of those verification techniques are, however, based on first-order refinement types, hence unable to verify certain properties of functions (such as the equality of two recursive functions and the monotonicity of a function, which we call relational properties). To relax this limitation, we introduce a restricted form of higher-order refinement types where refinement predicates can refer to functions, and formalize a systematic program transformation to reduce type checking/inference for higher-order refinement types to that for first-order refinement types, so that the latter can be automatically solved by using an existing software model checker. We also prove the soundness of the transformation, and report on preliminary implementation and experiments.

本文言語English
ホスト出版物のタイトルPEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015
出版社Association for Computing Machinery, Inc
ページ61-72
ページ数12
ISBN(電子版)9781450332972
DOI
出版ステータスPublished - 2015 1 13
外部発表はい
イベントACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015 - Mumbai, India
継続期間: 2015 1 132015 1 14

出版物シリーズ

名前PEPM 2015 - Proceedings of the 2015 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, co-located with POPL 2015

Conference

ConferenceACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015
国/地域India
CityMumbai
Period15/1/1315/1/14

ASJC Scopus subject areas

  • コンピュータ グラフィックスおよびコンピュータ支援設計
  • コンピュータ ビジョンおよびパターン認識
  • ソフトウェア

フィンガープリント

「Verifying relational properties of functional programs by first-order refinement」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル