A Certified Verifier for a Fragment of Separation Logic

スポンサーリンク

概要

• 論文の詳細を見る

• Separation logic is an extension of Hoare logic to verify imperative programs with pointers and mutable data-structures. Although there exist several implementations of verifiers for separation logic, none of them has actually been itself verified. In this paper, we present a verifier for a fragment of separation logic that is verified inside the Coq proof assistant. This verifier is implemented as a Coq tactic by reflection to verify separation logic triples. Thanks to the extraction facility to OCaml, we can also derive a certified, stand-alone and efficient verifier for separation logic.

• Information and Media Technologies 編集運営会議の論文

著者

• Marti Nicolas

  Dept. of Computer Science, University of Tokyo

• Affeldt Reynald

  Research Center for Information Security (RCIS), National Institute of Advanced Industrial Science and Technology (AIST)

関連論文

• A Certified Verifier for a Fragment of Separation Logic

スポンサーリンク