Automating relatively complete verification of higher-order functional programs

Access this Article

Abstract

We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs.

Journal

  • Proceeding POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

    Proceeding POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 75-86, 2013-01

    ACM

Keywords

Codes

  • NII Article ID (NAID)
    120006669372
  • Text Lang
    ENG
  • Article Type
    conference paper
  • Data Source
    IR 
Page Top