Skip to content

VerCors 1.0.0
Compare
Choose a tag to compare
@pieter-bos pieter-bos released this 11 Oct 10:37
· 3956 commits to master since this release
v1.0.0
3f561de
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.

Features

  • Generation of quantifier triggers by @HenkMulder.
  • Verification time learning for AST constructs by @HenkMulder.
  • Added a leader election protocol example by @wytseoortwijn.
  • Added SplitVerify, a tool to split verfication of files, currently by method. The results are then cached by chunk. By @sjcjoosten.
  • Add options --debug-before, --debug-after to debug intermediate AST structure
  • The viper backend is now a reference to the repository instead of a copy, enabling SBT to parallelize more.
  • Viper and Z3 have been updated.
  • Travis now splits the tests across jobs, so the build is 3x faster.
  • Travis build includes foldable sections, so the build log is more readable.
  • invariant is renamed to context_everywhere.
  • add \pointer_index, the equivalent of \pointer at one index.

Bugfixes

  • Fixed a case where the logging facility would recurse infinitely
  • Cleanup of OperatorExpression type check, fixes a missing null check.
  • Repaired Reducible, which was not available for a while.
  • Fixed a bug in \matrix, which now requires read permission for inspecting the rows.
Assets 3
Loading