サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
パリ五輪
www.chargueraud.org
CFML is a tool for the interactive verification of OCaml programs, using Coq and Separation Logic. The source files can be obtained from: git clone git@github.com:charguer/cfml.git For installation instruction, read the README file.The developments rely on my Coq library TLC.All the files are distributed under the GNU-LGPL license.
This paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then prove that the program satisfies a given specification by reasoning interactively about the characteristic formula using a proof assistant such as Coq
このページを最初にブックマークしてみませんか?
『www.chargueraud.org』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く