summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
* Fixes crash when modifies set includes a variable twice.Gravatar mkawa2009-11-07
* Added a sequence update expression in Dafny.Gravatar rustanleino2009-11-06
* Redesigned the encoding of Dafny generics, including the built-in types set a...Gravatar rustanleino2009-11-06
* Applied patch 4316, which fixes an unsoundness in the axiomatization of seque...Gravatar rustanleino2009-11-05
* The Dafny call statement now automatically declares left-hand sides as local ...Gravatar rustanleino2009-11-05
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "...Gravatar rustanleino2009-11-05
* Added loop invariants to make VSI-Benchmarks/b8.dfy verify. (Still to do: un...Gravatar rustanleino2009-11-04
* Look for Boogie.exe also in Program Files (x86)Gravatar MichalMoskal2009-11-03
* vc:doomed does not use the console anymore to report resultsGravatar schaef2009-11-02
* Fixed PreLoopHeap counting bug.Gravatar rustanleino2009-10-31
* Initial version of VSI Benchmarks 1 - 8Gravatar RMonahan2009-10-30
* Use the new F# names for bigint typeGravatar MichalMoskal2009-10-30
* Update F# binaries to Oct09 CTPGravatar MichalMoskal2009-10-30
* Fixed problem where Dafny filenames with unusual characters in filenames had ...Gravatar rustanleino2009-10-29
* - Sieve.chalice verifies + executes fasterGravatar jansmans2009-10-20
* - the "-gen" option works only if the program verifiesGravatar jansmans2009-10-16
* Implicitly declare as local variables undeclared variables occurring as LHS's...Gravatar rustanleino2009-10-16
* Sieve of Eratosthenes, written in Chalice.Gravatar rustanleino2009-10-15
* Changed how Boogie looks for Z3: first look in the directory where Boogie is...Gravatar rustanleino2009-10-14
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie filenam...Gravatar rustanleino2009-10-14
* Fixed bugs in inlining, and added a test case.Gravatar rustanleino2009-10-14
* In the TypeDeclCollector, call RegisterType for the bound variables in a quan...Gravatar stobies2009-10-12
* - fixed a positioning bug in Parser.scalaGravatar jansmans2009-10-07
* - extended to example to use acknowledgements (but uses sending debit)Gravatar jansmans2009-10-07
* - verified a program inpsired by "Copyless Message Passing" in ChaliceGravatar jansmans2009-10-07
* Added /z3lets switch, which governs which kinds of LET expressions are sent t...Gravatar rustanleino2009-10-04
* - where clauses are now properly type-checkedGravatar jansmans2009-10-02
* Implemented -noDeadlockChecks mode. With this mode, it is possible to give s...Gravatar rustanleino2009-10-01
* Handle new Z3 'Memout' message.Gravatar stobies2009-09-30
* Restoring Spec# binariesGravatar stobies2009-09-30
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
* Use type-erased result type to make decision about whether or not to include ...Gravatar rustanleino2009-09-27
* Optimized the number of Z3 queries in doomed program point detection.Gravatar schaef2009-09-25
* Added antecedent to select-of-store axioms to make them sound even when trigg...Gravatar rustanleino2009-09-24
* Added /z3multipleErrors flag for generation of multiple counterexamples per a...Gravatar mkawa2009-09-23
* * Boogie and Dafny: added /cev:<file> optionGravatar rustanleino2009-09-15
* Dafny: Added axioms for division and modulo.Gravatar rustanleino2009-09-15
* Dafny:Gravatar rustanleino2009-09-14
* Report prover warnings during smoke test via the VerifierCallbackGravatar stobies2009-09-07
* Use callback mechanism to report prover warnings; do not just write them to s...Gravatar stobies2009-09-07
* Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other bit...Gravatar stobies2009-09-07
* Full (?) support in Dafny for Counterexample Visualizer predicates.Gravatar rustanleino2009-08-19
* Please ignore. Just testing my account.Gravatar schaef2009-08-19
* Improve token-dumping in the inspector interfaceGravatar MichalMoskal2009-08-18
* Also sign AbsInt.dllGravatar stobies2009-08-18
* Added files to stamp drop builds with generated version numbersGravatar stobies2009-08-18
* - made the output of the Chalice-to-C# translator slightly nicerGravatar jansmans2009-08-17
* - Chalice-to-C# compiler now supports channelsGravatar jansmans2009-08-17
* Sign assembliesGravatar stobies2009-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-20 01:30:14 +0000