23.07-RC

ViperServer: commit 493a228
Silicon: commit b6cde9dcc447622e7cd745ebff43b2e97251a996
Carbon: commit 5b2547cc888e7e9fe1fc52c6c08e5600956aa62e
Silver: commit 7f1385bfc648e3e8296e60d1d7fc46aeaade3261

January 2023 release

ViperServer: commit 9a23518
Silicon: commit 7f2e6823cc24e86638609e40b24827e2c6676d00
Carbon: commit e07c8960748aa3e69b22bd327a4ebf572301bc8e
Silver: commit 1c959056bb343dd5346705eef0a6b25a140d1465

23.01-RC

ViperServer: commit d9fda3f
Silicon: commit e5fecda16eb3e4995995735483db7cd680ce174d
Carbon: commit 1adecea5ed5f35b873fae9c55f17756e8a45812a
Silver: commit f0fe19419ebc17c14d976440d8f88ff1d631c930

November 2022 release

ViperServer uses Viper's July 2022 release for its dependencies (i.e. the verification backends) and provides several bug fixes related to ViperServer's LSP functionality.

ViperServer: commit 366c33e
Silicon: commit 098881005e53a0784ed1862bea4c07408b9b6e2d
Carbon: commit 4df61d8e37d8952d0eeb69d4bb797d5934e1d2f0
Silver: commit 918bafa770a88e1b488d9a93ad5eb250be41e983

July 2022 release

Release 2022.7

Date 29/07/22

Changes in Viper Language

• ADT plugin added. It is enabled by default, and can be disabled with the --disableAdtPlugin command-line option. This plugin converts ADT (abstract datatype) declarations of the form adt (name) { Constructor1(args) ... } into domain types with constructors, destructors, discriminants, and corresponding axioms. More information can be found in the tutorial (Silver#574)
• Added support for a refute (expression) statement. This statement behaves like an assertion, except the expression is expected to be provably false. More information can be found in the tutorial (Silver#583)
• Division of two Perm-typed expressions is now allowed. (Silver#572)
• Typed function application syntax ((foo(...) : T)) now parses properly. (Silver#584)

Backend-specific upgrades/changes

Symbolic Execution Verifier (Silicon)

• Output sent to the backend solver is now SMT-LIB 2.6 conformant. Additionally, there is experimental support for the CVC5 solver using the --prover cvc5 command-line option. (Silicon#609)
• Improved counterexamples. Counterexamples are now generated for domain types as well, and are included in the output with the --counterexample mapped command-line option. (Silicon#631)

Verification Condition Generation Verifier (Carbon)

• Breaking change: wildcard acc expressions in exhale statements are no longer reordered. Behaviour is now consistent with Silicon and all permissions in an exhale statement are always exhaled left to right. (Silicon#30, Carbon#411)

Miscellaneous

• "Chopper" API is now available to front ends. This functionality allows a single Viper file to be split into multiple smaller files that can be verified separately. Dependencies between functions, methods, and predicates are correctly determined to minimise the size of the individual Viper files. (Silver#589)
• Upgraded projects to use sbt version 1.6.2. (Silicon#627, Silver#592)
• Viper IDE uses .vpr as its default file extension. (viper-ide#223)
• Viper IDE now requires at least Java version 11. (viper-ide#250)
• Cache improvements. (Silver#578)
• Various bug fixes. (Carbon#423, Carbon#425, viper-ide#248, Silver#496, Silver#587, Silver#590)

ViperServer: commit 22fe7b8
Silicon: commit 098881005e53a0784ed1862bea4c07408b9b6e2d
Carbon: commit 4df61d8e37d8952d0eeb69d4bb797d5934e1d2f0
Silver: commit 918bafa770a88e1b488d9a93ad5eb250be41e983

February 2022 release

ViperServer: commit b62f762
Silicon: commit cd20cf02b31ccd82a2cfdca7003947fd4380fe7b
Carbon: commit ef14316accc1add1effd3c2c2b1969f16891ba91
Silver: commit aeaebeaef7bf977c037e6390839aeb2f5c8b384b

22.02-RC

ViperServer: commit d2115c6
Silicon: commit cd20cf02b31ccd82a2cfdca7003947fd4380fe7b
Carbon: commit ef14316accc1add1effd3c2c2b1969f16891ba91
Silver: commit aeaebeaef7bf977c037e6390839aeb2f5c8b384b

v.21.07-release

ViperServer: commit 3e7d117
Silicon: commit 4dbb81fc9c3470ba9608eda5f08932962aee5479
Carbon: commit 4cdea1baeefbfd741ee2d0157e7c43337d84fe44
Silver: commit 3ea54220f1d2bc4adcc3151fa2080c198dbbd641

21.07-RC

ViperServer: commit dd1fe3f
Silicon: commit 8a017406684c5f5301c99a06873d0416388e89f2
Carbon: commit 4cdea1baeefbfd741ee2d0157e7c43337d84fe44
Silver: commit 44129b9d3870d2ca26c6f567405aa8abc51b9365

v.21.07-alpha2

ViperServer: commit a9ec059
Silicon: commit 3a31f3917f47b7734044d4ccfd1aa46b250dca34
Carbon: commit d6008c5da7d5b506c34d06b98b15811af77d9504
Silver: commit 47705f930fef963d58fb42ac9cd713d48af048d3