./devel/verifast, VeriFast code verifier in separation logic

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]


Branch: CURRENT, Version: 17.06, Package name: verifast-17.06, Maintainer: ryoon

VeriFast is a research prototype of a tool for modular formal
verification of correctness properties of single-threaded and
multithreaded C and Java programs annotated with preconditions and
postconditions written in separation logic.


Required to run:
[lang/ocaml] [lang/camlp4] [x11/ocaml-lablgtk]

Required to build:
[pkgtools/x11-links] [x11/compositeproto] [x11/glproto] [x11/renderproto] [x11/xproto] [x11/xf86vidmodeproto] [x11/xf86driproto] [x11/damageproto] [x11/inputproto] [x11/xextproto] [x11/randrproto] [x11/dri2proto] [lang/vala] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [lang/camlp4]

Master sites:

SHA1: 9c918c6fa88ab11315fe80abfa097dcc8d0f85cd
RMD160: 8808173823c6697272450ba0eac71cfc4824af54
Filesize: 1658.247 KB

Version history: (Expand)


CVS history: (Expand)


   2017-07-12 03:54:16 by Ryo ONODERA | Files touched by this commit (5)
Log message:
Import verifast-17.06 as devel/verifast.

VeriFast is a research prototype of a tool for modular formal
verification of correctness properties of single-threaded and
multithreaded C and Java programs annotated with preconditions and
postconditions written in separation logic.

This is recommended by Kiwamu Okabe in Japan NetBSD Users' Group BOF 2017
at the University of Tokyo.