Data

Tools

Indexes

Applications

Experiments

Open Source Science

Recent Releases of vercors

vercors - VerCors 2.3.0

What's Changed

  • Don't try to delete nonexistent preprocessor output if clang fails by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1236
  • VeyMont: lightweight permissions by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1244
  • AutoValue unsoundness, Test Suite runner, Paths with spaces by @superaxander in https://github.com/utwente-fmt/vercors/pull/1252
  • Attempt to fix the test reporting by running the test report on the default branch by @superaxander in https://github.com/utwente-fmt/vercors/pull/1253
  • Update to setup-java@v4 by @superaxander in https://github.com/utwente-fmt/vercors/pull/1254
  • Restrict C++ character literals to a single UTF-8 char by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1249
  • Make contract of free (for C) conditional on ptr being non-null by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1250
  • Encode that malloc may return NULL in C (weaken postcondition) by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1239
  • Fix empty PVL enums causing verification failure by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1248
  • Update VCLLVM (now Pallas) to LLVM 17, update to newest VerCors version, and convert more instructions to COL by @superaxander in https://github.com/utwente-fmt/vercors/pull/1159
  • Add stringToName special case for all-underscores identifier strings by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1260
  • VeyMont: support inline, wrapped, and no stratified permissions, fix some of Wander's issues, update VeyMont pass order. by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1259
  • VeyMont: remove ChorPerm by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1269
  • VeyMont: remove PushInChor by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1276
  • Struct examples by @superaxander in https://github.com/utwente-fmt/vercors/pull/1270
  • Log and exit error if --compile (PVL-to-Java translation) mode fails by @wandernauta in https://github.com/utwente-fmt/vercors/pull/1278
  • Integrate Pallas FunctionContracts by @RobertMensing in https://github.com/utwente-fmt/vercors/pull/1280
  • Fix heap variables with pointer types in C, fixes #1286 by @superaxander in https://github.com/utwente-fmt/vercors/pull/1288
  • Fixed issue #924: context_everywhere was not propagated correctly in run methods. by @OmerSakar in https://github.com/utwente-fmt/vercors/pull/1297
  • Support specification-constructs in Pallas specifications by @RobertMensing in https://github.com/utwente-fmt/vercors/pull/1289
  • Quantifier fix by @sakehl in https://github.com/utwente-fmt/vercors/pull/1309
  • Extend pointer encoding by @superaxander in https://github.com/utwente-fmt/vercors/pull/1277
  • Small fixes by @superaxander in https://github.com/utwente-fmt/vercors/pull/1314

New Contributors

  • @wandernauta made their first contribution in https://github.com/utwente-fmt/vercors/pull/1236
  • @RobertMensing made their first contribution in https://github.com/utwente-fmt/vercors/pull/1280

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v2.2.0...v2.3.0

- Scala
Published by github-actions[bot] about 1 year ago

vercors - VerCors 2.2.0

What's Changed

  • Add challenge 3 from the verifyThis 2019 challenge by @sakehl in https://github.com/utwente-fmt/vercors/pull/1167
  • Generics for PVL classes by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1154
  • Watch input files by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1192
  • Add challenge 1 and challenge 2 of verifythis 2024 by @superaxander in https://github.com/utwente-fmt/vercors/pull/1190
  • Parser analysis by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1200
  • Small fix by @sakehl in https://github.com/utwente-fmt/vercors/pull/1197
  • Prepare formatting rules by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1205
  • VeyMont: name refactoring, implementation generation, endpoint context, channel invariant partial support by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1188
  • Small debug fixes 2 by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1048
  • Vector support in C, OpenCL and CUDA + Vector ADT in PVL by @sakehl in https://github.com/utwente-fmt/vercors/pull/1156
  • Rasi generator by @PBHTasche in https://github.com/utwente-fmt/vercors/pull/1208
  • Add AutoValue by @superaxander in https://github.com/utwente-fmt/vercors/pull/1207
  • VeyMont: channel invariant, stratified expression containers by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1209
  • Fix build on JDK 21+, resolves #1146 by @superaxander in https://github.com/utwente-fmt/vercors/pull/1212
  • Fix crash that can occur after vercors finishes executing by @superaxander in https://github.com/utwente-fmt/vercors/pull/1213
  • Performance improvements by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1218
  • Shared predicate node 2 by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1220
  • Only rewrite with knowledge up to now by @sakehl in https://github.com/utwente-fmt/vercors/pull/1217
  • Rasi generator by @PBHTasche in https://github.com/utwente-fmt/vercors/pull/1221
  • Fix protobuf build on CMake 3.30 by @superaxander in https://github.com/utwente-fmt/vercors/pull/1223
  • Middleware by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1224
  • VeyMont: stratified permissions by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1210
  • Integrate updates to LangCPPParser from the antlr/grammars-v4 repository by @superaxander in https://github.com/utwente-fmt/vercors/pull/1226
  • Remove unused rewrite pass by @superaxander in https://github.com/utwente-fmt/vercors/pull/1228
  • VeyMont: codegen by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1225

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v2.1.1...v2.2.0

- Scala
Published by github-actions[bot] over 1 year ago

vercors - VerCors 2.1.1

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: https://github.com/utwente-fmt/vercors/compare/v2.1.0...v2.1.1

- Scala
Published by github-actions[bot] almost 2 years ago

vercors - VerCors 2.1.0

What's Changed

  • Generic parameters java by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/983
  • add forperm, polarity_dependent by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/987
  • VeSUV working for now by @PBHTasche in https://github.com/utwente-fmt/vercors/pull/985
  • Framed proof heap values by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/988
  • add perf stats via jna for unix (linux/mac) by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/978
  • Veymont pre by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/984
  • [VCLLVM] LLVM to COL rewriter for LLVM specific nodes by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/990
  • Reorganize by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/996
  • add resourceusage fallback, used immediately in non-unix by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/997
  • [VCLLVM] Add llvm loop and llvm loop contract nodes by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/994
  • Nested foralls patch by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/998
  • Nested Quantifiers improvements by @sakehl in https://github.com/utwente-fmt/vercors/pull/991
  • fix Issue 992 by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/999
  • [VCLLVM] Add proper label, goto, and branch support to LlvmFunctionDefinitions by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/1002
  • Implement scaling of instance predicates by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1003
  • fix inline triggers with \unfolding by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/1005
  • Redo pretty-printing by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1006
  • allow wand-chunk-not-found as falsity of assertions by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1008
  • replace :: with +: by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1009
  • print veymont nodes by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1010
  • map viper prover types to vercors by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1016
  • improve loop contract options in pvl by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1017
  • Add DeserializeOrigin to LLVMOrigin rewriter by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/1007
  • Windows build stuff by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1020
  • update boogie by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1024
  • bump viper by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1027
  • [VCLLVM] Deserialize origin "provider" by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/1023
  • Add context to VerificationError and print nodes in context by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/1026
  • fix #1025 and better inline binding origins by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1029
  • Smtlib types by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1030
  • update realpath command to be equivalent, osx compatible readlink -f by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/1032
  • java version specified explicitly by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/1033
  • [VCLLVM] Add function call support for LLVM by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/1036
  • Fixes for examples by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/1037
  • Add flag to turn off smart heap inference by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1041
  • Ranged for syntax in PVL by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1043
  • Improve ranged for to not be annoying on use of heap locations by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1044
  • add global heap variables by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1047
  • [VCLLVM] Add partial contract support for LLVM by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/1034
  • Implemented basic C++ support by @Ellen-Wittingen in https://github.com/utwente-fmt/vercors/pull/1052
  • [VCLLVM] Add support for pure functions by @Drevanoorschot in https://github.com/utwente-fmt/vercors/pull/1049
  • Veymont gen par by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/1053
  • remove the implicit scope of AbstractMethod - should be covered by Scope by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1062
  • Add the enum reference when an enum constant is resolved by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1066
  • fix #463: consider whether the context is static by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1067
  • fix #1061: propagate c_e to framedproof by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1071
  • fix #1050: set git buildinfos for caching properly by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1072
  • error when this makes no sense in a context by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1074
  • do not emit permissions for final fields in pvl constructors by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1075
  • Resolve javabip warnings by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1073
  • fix #1000, fix #749: inline appropriate let bindings in patterns by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1076
  • Refactor origin add req names by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/1077
  • Warnings by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1078
  • VeyMont: Add communicate statement by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1079
  • Support for SYCL's basic and nd-range kernels by @Ellen-Wittingen in https://github.com/utwente-fmt/vercors/pull/1070
  • fix #1060, actually fix #789: stop all non-daemon threads and timers by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1084
  • fix #742: yields variables are not referencable in requires/context/c_e by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1085
  • Improve ci caching by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1086
  • Refactor origin by @Naum-Tomov in https://github.com/utwente-fmt/vercors/pull/1089
  • Resource values by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1087
  • Make printing nodes in verificationerrors easier by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1091
  • VeyMont: refactor SeqProgram into PVLSeqProgram & SeqProgram by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1090
  • bump viper by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1093
  • VeyMont: resolution improvements by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1092
  • Refactor resolution error to have a more precise error code by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1098
  • VeyMont: seq_run, :=, structure checks and initial sequential program tranformation by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1095
  • VeyMont: seq_prog initialization & permission generation by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1102
  • Added support for SYCL's accessors and declarators. by @Ellen-Wittingen in https://github.com/utwente-fmt/vercors/pull/1100
  • Fixed problems with the Viper (language) support by @OmerSakar in https://github.com/utwente-fmt/vercors/pull/1105
  • Origin cleanup by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1104
  • warnings by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1107
  • VeyMont: loop & branch unanimity by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1106
  • VeyMont: full permission generation & auxiliary methods by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1110
  • Better c support by @sakehl in https://github.com/utwente-fmt/vercors/pull/1059
  • Added support for SYCL's local accessors plus minor changes by @Ellen-Wittingen in https://github.com/utwente-fmt/vercors/pull/1121
  • Redo helpers: make a proper meta-model of Node.scala by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1118
  • add Nele's topological sort to examples directory by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/1130
  • Add ArrayList from Joost Sessink to test suite by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1131
  • Move JavaBIP case study to publications folder by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1132
  • Quantifier triggers are now also processed when they are location by @sakehl in https://github.com/utwente-fmt/vercors/pull/1124
  • VeyMont: reinstate old tests & case studies by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/1114
  • More sycl examples and bugfixes by @Ellen-Wittingen in https://github.com/utwente-fmt/vercors/pull/1126
  • perf: fix #1116 by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1135
  • Fix for #1141 by @sakehl in https://github.com/utwente-fmt/vercors/pull/1142
  • Vcllvm by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1144
  • Fix bug which caused VCLLVM to get stuck by @superaxander in https://github.com/utwente-fmt/vercors/pull/1149
  • run ci on pull request when forked by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1155
  • Quick fixes by @sakehl in https://github.com/utwente-fmt/vercors/pull/1127
  • Actually skip backend by @sakehl in https://github.com/utwente-fmt/vercors/pull/1157
  • add syntax for indeterminate branch for pvl by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/1174
  • Fix VCLLVM compilation for the artifact by @superaxander in https://github.com/utwente-fmt/vercors/pull/1180
  • Some fixes for GPUs shared memory by @sakehl in https://github.com/utwente-fmt/vercors/pull/1177
  • Add some simplify quantifiers examples by @sakehl in https://github.com/utwente-fmt/vercors/pull/1181
  • Java system fix by @sakehl in https://github.com/utwente-fmt/vercors/pull/1185
  • RASI Generator by @PBHTasche in https://github.com/utwente-fmt/vercors/pull/1171

New Contributors

  • @Ellen-Wittingen made their first contribution in https://github.com/utwente-fmt/vercors/pull/1052
  • @superaxander made their first contribution in https://github.com/utwente-fmt/vercors/pull/1149

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v2.0.0...v2.1.0

- Scala
Published by github-actions[bot] almost 2 years ago

vercors - VerCors 1.4.1

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

  • Print an error when the language is not specified by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/723
  • Add vim plugin (syntax and filetype detection) by @Jesse-Bakker in https://github.com/utwente-fmt/vercors/pull/737
  • Veymont etaps extensions by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/727
  • Backport backend options flag by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/784
  • Add big integer support to PVL by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/726
  • Require constructor for lock invariant by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/720
  • Partially reinstate problem fail tests by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/658
  • Disable casting in parblockencoder by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/660
  • Veymont (v1) by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/972
  • Gpgpu optimizations by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/976

New Contributors

  • @Jesse-Bakker made their first contribution in https://github.com/utwente-fmt/vercors/pull/737

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v1.4.0...v1.4.1

What's Changed

  • Print an error when the language is not specified by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/723
  • Add vim plugin (syntax and filetype detection) by @Jesse-Bakker in https://github.com/utwente-fmt/vercors/pull/737
  • Veymont etaps extensions by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/727
  • Backport backend options flag by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/784
  • Add big integer support to PVL by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/726
  • Require constructor for lock invariant by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/720
  • Partially reinstate problem fail tests by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/658
  • Disable casting in parblockencoder by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/660
  • Veymont (v1) by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/972
  • Gpgpu optimizations by @pieter-bos in https://github.com/utwente-fmt/vercors/pull/976

New Contributors

  • @Jesse-Bakker made their first contribution in https://github.com/utwente-fmt/vercors/pull/737

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v1.4.0...v1.4.1

- Scala
Published by pieter-bos almost 2 years ago

vercors - VerCors 2.0.0

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

  • @Jesse-Bakker made their first contribution in https://github.com/utwente-fmt/vercors/pull/737
  • @sakehl made their first contribution in https://github.com/utwente-fmt/vercors/pull/771
  • @PBHTasche made their first contribution in https://github.com/utwente-fmt/vercors/pull/981

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v1.4.0...v2.0.0

- Scala
Published by pieter-bos almost 3 years ago

vercors - VerCors Wiki PDF

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

- Scala
Published by github-actions[bot] almost 4 years ago

vercors - VerCors 1.4.0

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 * Windows support by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/582 * Reinstate carbon by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/577 * Guide pass progression by AST properties (features) by @niomaster in https://github.com/utwente-fmt/vercors/pull/541 * rename DivAssign to FloorDivAssign by @Vescatur in https://github.com/utwente-fmt/vercors/pull/590 * permission values should be rationals; some formatting fixes by @niomaster in https://github.com/utwente-fmt/vercors/pull/575 * Fix grammar warnings by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/587 * support given/yields for kernels, support multiple upper bounds in quantified relational expressions by @niomaster in https://github.com/utwente-fmt/vercors/pull/591 * fixed NullPointerException in CreateReturnParameter.java by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/606 * use Path objects instead of plain Strings to track file origins. Fixes #601 by @Jankoekenpan in https://github.com/utwente-fmt/vercors/pull/602 * Standardize "resource functions" to predicates by @niomaster in https://github.com/utwente-fmt/vercors/pull/607 * Upgrade to viper 21.01 by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/580 * changes to PVL and JavaPrinter and PVLSyntax by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/616 * Update options of VerCors by @Sophietje in https://github.com/utwente-fmt/vercors/pull/586 * Issue 614 by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/617 * order of annotations is now preserved almost by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/618 * run sbt for classpath from repo root by @niomaster in https://github.com/utwente-fmt/vercors/pull/611 * Issue #621: improved support for set comprehension by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/622 * Remove unused rewrite passes by @Sophietje in https://github.com/utwente-fmt/vercors/pull/615 * disabled fail-fast strategy #issue-626 by @Vescatur in https://github.com/utwente-fmt/vercors/pull/627 * Issue 628 shared run configurations and list of failing tests by @Vescatur in https://github.com/utwente-fmt/vercors/pull/630 * Fix ArrayNullValuesSpec: make sequence as primitive type (not old style) by @niomaster in https://github.com/utwente-fmt/vercors/pull/638 * Issue 633 by @Vescatur in https://github.com/utwente-fmt/vercors/pull/634 * Predicate refactor 2 by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/639 * VeyMont merge into VerCors by @Sophietje in https://github.com/utwente-fmt/vercors/pull/641 * reduce veymont code smells by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/645 * Upgrade SBT to 1.5.1 by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/632 * Add exception patterns case study & re-enable elect.pvl by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/635 * Issue 449 - sonarcloud by @Vescatur in https://github.com/utwente-fmt/vercors/pull/647 * Issue 449 remove commented code by @Vescatur in https://github.com/utwente-fmt/vercors/pull/648 * Fork examples by @petravandenbos-utwente in https://github.com/utwente-fmt/vercors/pull/652 * Add coverage by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/487 * Testsuite verdict strict by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/599 * Final fix for coverage by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/656 * Skip backend & skip transformations flags by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/657 * Proper error when unfolding abstract predicate by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/659 * Issue 509 slow tests by @Vescatur in https://github.com/utwente-fmt/vercors/pull/649 * Fix simple-ltid.cu by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/661 * Reinstate History.pvl by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/662 * Reinstate monotonicBool & monotonicBoolBroken by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/667 * Issue 663 2 by @Vescatur in https://github.com/utwente-fmt/vercors/pull/669 * fix sonar test by @Vescatur in https://github.com/utwente-fmt/vercors/pull/670 * Veymont fix bugs and test cases by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/672 * Run VeyMont in CI by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/673 * Add a trait which makes the main method explicit by @Vescatur in https://github.com/utwente-fmt/vercors/pull/677 * Issue 664 - removing unused code by @Vescatur in https://github.com/utwente-fmt/vercors/pull/671 * added examples from verifyThis competitions by @ArmborstL in https://github.com/utwente-fmt/vercors/pull/697 * Make formatting of printed information consistent and print verification start time. by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/698 * Change vsum axioms to only return null upon an empty range, and not an invalid range by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/699 * Viper 21.07 by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/700 * Ensure vercors package works in the presence of long paths by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/702 * Fix trigger generation for `\values` by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/706 * Enhance exists by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/705 * Add more detailed version info to `--version` by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/707 * Generate triggers more conservatively by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/708 * Replace old in syntax with slash syntax by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/709 * More explicitly print the context if a name cannot be resolved by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/710 * Also print trigger candidates if body is not eq, ne, etc. by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/711 * Add Wiki to PDF/HTML workflow by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/712 * Add injectivity/equality axiom to Option by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/713 * Enable GPGPU examples for testing by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/715 * Test wiki snippets in CI by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/714 * Move old rewrite rules to file in util/ by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/716 * Take `synchronized` into account when computing features by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/717 * Fix that a return parameter assignment is not created on function calls by @bobismijnnaam in https://github.com/utwente-fmt/vercors/pull/719

New Contributors

  • @ArmborstL made their first contribution in https://github.com/utwente-fmt/vercors/pull/582
  • @Jankoekenpan made their first contribution in https://github.com/utwente-fmt/vercors/pull/602

Full Changelog: https://github.com/utwente-fmt/vercors/compare/v1.3.0...v1.4.0

- Scala
Published by pieter-bos about 4 years ago

vercors - VerCors Wiki PDF

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.

- Scala
Published by github-actions[bot] over 4 years ago

vercors - VerCors 1.3.0

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

- Scala
Published by pieter-bos about 5 years ago

vercors - Vercors Dev Build

This is an alpha build of the vercors development branch. It is updated automatically after each merge. Refer to the commit on the left for the last update.

- Scala
Published by github-actions[bot] about 5 years ago

vercors - VerCors 1.2.0

Features

  • Re-structured and cleaned up repository:
    • Removed dependency on ant: everything is now built by SBT
    • Moved to sbt-native-packager: we can now build platform-specific packages
    • Simplified run scripts; they no longer depend on sbt assembly
    • Removed distributed binaries of libraries, ant and sbt
  • Enabled support for method calls in if conditions. They are now also evaluated in the correct place (#189)

Bugfixes

  • Rename context_everywhere back to invariant for resource invariants
  • Fixed a bug where with did not work in par blocks (#63)
  • Fixed a bug in \matrix (#116)

- Scala
Published by pieter-bos over 6 years ago

vercors - VerCors 1.1.0

Features

  • Add syntax for slicing sequences and updating them functionally, by @wytseoortwijn.

Bugfixes

  • Compiled viper files were not being cached correctly in travis, now they are.

- Scala
Published by pieter-bos over 6 years ago

vercors - VerCors 1.0.0

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.

- Scala
Published by pieter-bos over 6 years ago