Skip to content

Releases: utwente-fmt/vercors

VerCors Nightly

04 Jan 15:59
ab31613
Compare
Choose a tag to compare
VerCors Nightly Pre-release
Pre-release

Nightly Build

VerCors Wiki PDF

01 Nov 09:11
Compare
Choose a tag to compare
VerCors Wiki PDF Pre-release
Pre-release

These are automatically generated versions of the tutorial on the VerCors wiki. There are two artefacts of interest: the Latex/PDF version, suitable for printing, and the HTML version, suitable for offline viewing.

VerCors 2.2.0

14 Aug 13:59
Compare
Choose a tag to compare

What's Changed

Full Changelog: v2.1.1...v2.2.0

VerCors 2.1.1

18 Apr 13:30
Compare
Choose a tag to compare

What's Changed

  • Resolved a rare concurrency bug in the rendering of progress messages in aef15a4
  • Restored SysCIR as a dependency in b13e385

Full Changelog: v2.1.0...v2.1.1

VerCors 2.1.0

07 Apr 15:12
Compare
Choose a tag to compare

What's Changed

Read more

VerCors 1.4.1

02 Apr 14:53
Compare
Choose a tag to compare

NB: This is a release of backported changes to the v1 branch of VerCors. Please consider using a v2 version where possible. The VerCors executable is renamed to vercors1 to enable installing a v1 version alongside a v2 version.

What's Changed

New Contributors

Full Changelog: v1.4.0...v1.4.1

What's Changed

New Contributors

Full Changelog: v1.4.0...v1.4.1

VerCors 2.0.0

16 Mar 10:45
Compare
Choose a tag to compare

What's Changed

  • The internal data structure for syntax trees was redesigned, making many things more stable and consistent
  • Verification failures are translated to more specific errors
  • The options were re-done, try --help
  • Various bits of syntax have changed, see also the wiki
  • You can introspect the progress of the verification backend in more detail: a report is printed when it is stuck, and see e.g. --silicon-print-quantifier-stats

New Contributors

Full Changelog: v1.4.0...v2.0.0

VerCors 1.4.0

21 Jan 11:49
Compare
Choose a tag to compare

Warning: this release has a path problem on windows. If you are a windows user, please use dev branch release: https://github.com/utwente-fmt/vercors/releases/tag/dev-prerelease

What's Changed

What's Changed

New Contributors

Full Changelog: v1.3.0...v1.4.0

VerCors Wiki PDF

03 Mar 11:54
Compare
Choose a tag to compare
VerCors Wiki PDF Pre-release
Pre-release

This is an automatically generated LaTeX/PDF version of the tutorial on the VerCors wiki.

VerCors 1.3.0

03 Feb 14:16
Compare
Choose a tag to compare

Features

  • The webpage code was moved to a different repository
  • Added detection for contracts of which the requirements are unsatisfiable
  • Added type checking to jspec rewriting rules
  • Refactored the test framework
  • Warn users when using integer division in permission values
  • Updated viper to release 20.07
  • Improve the support for sequences, sets and options in PVL, and add support for Maps, Set comprehension (@OmerSakar)
  • Fixed all warnings in the build, greatly improving build time
  • Pointers may now be assigned by subscript
  • Updated z3 to 4.8.6
  • Added various simplifying rewrite rules
  • Added support for exceptions and exceptional statements (break, continue) (@bobismijnnaam)
  • Improved C and GPGPU support: pure methods and functions, ghost statements, CUDA kernel invocations, kernel invariants and atomics
  • Improved syntax highlighting for PVL
  • --version now outputs better diagnostic information, including the commit
  • Range syntax was changed from [a..b) to {a..b}
  • Parsing frontend was redone: specifications are parsed in the first pass and attached in the tree; the parse tree is transformed by destructuring pattern match in Scala
  • All expression classes are now case classes, and consequently have structural equality
  • Add support for the ambiguous boolean/bitwise operators in Java: ^, | and &
  • Contracts are attached correctly to labeled loops
  • NameScanner was refactored (@bobismijnnaam)
  • Pure function application is now allowed in invariants
  • The user can be notified of completion of verification with --notify
  • Switched to GitHub Actions
  • Added various new examples

Bugfixes

  • Fixed a case where the origin of contracts was not preserved
  • Fixed that vercors warned about simplification failures in simple quantified statements about arrays
  • Fixed an infinite loop in the array encoding
  • Map the Head operator to Viper again
  • ==> and -* are now right-associative
  • Fixed a case where an expression was extracted to a variable in flatten without effect
  • Some examples that used old backends were refactored to use silicon (@Sophietje)
  • Disallow writing to locals in parallel blocks (which caused unsoundness)
  • Disallow using \result in signals specifications
  • Warn that inner classes are not supported, instead of crashing