Skip to content

Releases: PrincetonUniversity/VST

VST version 2.6

30 Sep 19:06
@andrew-appel andrew-appel
v2.6
8504124
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
VST version 2.6 
v2.6

VST release X.Y, retag
Assets 2
Loading

VST version 2.5

30 Sep 19:07
@andrew-appel andrew-appel
v2.5
6c9694c
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
VST version 2.5 
v2.5

VST release 2.5
Assets 2
Loading

VST version 2.4

30 Sep 19:19
@andrew-appel andrew-appel
v2.4
caf21a0
Compare
Choose a tag to compare
VST version 2.4 
v2.4

VST release 2.4
Assets 2
Loading

VST version 2.1

19 Apr 12:03
@andrew-appel andrew-appel
v2.1
755b868
Compare
Choose a tag to compare
VST version 2.1

The packaged version of this release, which omits many inessential subdirectories, is available at
http://vst.cs.princeton.edu/download/vst-2.1.tgz.

It is compatible with CompCert 3.2 and Coq 8.7.0, 8.7.1, 8.7.2, 8.8.0.

Changes since version 2.0:

  • hint tactic, makes suggestions about what Verifiable C tactic to apply (see "Hint" chapter of VC.pdf)

  • Require Import VST.floyd.functional_base.
    If you have a theory file containing a pure functional model WITHOUT separation logic but WITH the theory of CompCert Integers, and you want to use a lot of relevant Floyd tactics and lemmas without having to import all of VST.floyd.proofauto, you can import this file instead.

  • Various efficiency improvements in forward, forward_call, entailer, with_library, make_compspecs, make_varspecs.

  • No holes in the proof: The entire VST development up to VST.floyd.proofauto is now proved without any axioms, assumptions, admitted lemmas, etc. except for some standard axioms: extensionality, proof irrelevance, excluded middle, and (for use by CompCert's floating-point stuff) a lengthy axiomatization of the real numbers.

  • Private global variables: better encapsulation of modules that use private extern (or static) variables: see the chapter "gvars: Private global variables" in the reference manual (VC.pdf).

  • Ramification tactics, for more flexible framing than the ordinary freezer or frame rule: tactics localize, unlocalize; documentation to follow.

  • Magic wand as frame: new library of lemmas and tactics, documentation to follow (but see the hash-table exercise).

  • Concurrency with ghost state: Verifiable C now supports shared-memory concurrent programming with ghost state in the form of (for example) partial commutative monoids. Documentation to follow.

  • Overhaul of the control-flow tactics: forward_for deprecated, forward_if more intelligent, forward_loop very capable. See the reference manual chapters "If, While, For" and "For loops (general iterators)" .

  • Improved rep_omega tactic, which is a more powerful replacement for the previous repable_signed tactic. See chapter "rep_omega".

  • Fixed issues: 48, 90, 107, 113, 120, 133, 134, 136, 142, 145, 147, 148, 159, 162, 187.

Assets 2
Loading

VST version 2.0

19 Jan 18:42
@andrew-appel andrew-appel
v2.0
cf34639
Compare
Choose a tag to compare
VST version 2.0

The packaged version of this release, which omits many inessential subdirectories, is available at
http://vst.cs.princeton.edu/download/vst-2.0.tgz.

It is compatible with CompCert 3.2 and Coq 8.7.1.

Assets 2
Loading

VST version 1.9

24 Aug 20:35
@andrew-appel andrew-appel
v1.9
c71b589
Compare
Choose a tag to compare
VST version 1.9

The packaged version of this release, which omits many inessential subdirectories, is available at
http://vst.cs.princeton.edu/download/vst-1.9.tgz.

It is compatible with CompCert 2.7.2.1 and Coq 8.6 or 8.6.1.

Assets 2
Loading