summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Expand)AuthorAge
* Added compilation support for multisets and sequences from arrays.Gravatar Jason Koenig2011-07-15
* Strengthened axioms for multisets and sequences.Gravatar Jason Koenig2011-07-14
* Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...Gravatar Jason Koenig2011-07-13
* Multiset forming operators added.Gravatar Jason Koenig2011-07-11
* Partial implementation of multisets.Gravatar Jason Koenig2011-07-11
* Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run...Gravatar Jason Koenig2011-07-08
* Dafny: Fixed axioms for Seq#Contains vs. the sequence building functionsGravatar Rustan Leino2011-06-29
* Dafny: fixed soundness problem with HeapSucc axiomGravatar Rustan Leino2011-06-01
* Dafny: added set comprehension expressionsGravatar Rustan Leino2011-05-18
* Dafny: To help verifications involving sequences of (boxed) booleans along, a...Gravatar Rustan Leino2011-05-16
* Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid...Gravatar Rustan Leino2011-05-11
* Don't set logic to UFNIA when /useArrayTheoryGravatar Michal Moskal2011-05-09
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Updated PrepareBoogieZip.bat to include BVD and smt2Gravatar rustanleino2011-03-10
* Add tickleBoolGravatar MichalMoskal2011-02-18
* Dafny:Gravatar rustanleino2011-02-17
* Provide /p: as the short form of /proverOpt:.Gravatar MichalMoskal2011-02-17
* Make it possible to run Z3 on pipe; use generic PROVER_LOG optionsGravatar MichalMoskal2011-02-17
* Workaround bug in Z3 SMT parserGravatar MichalMoskal2011-02-15
* Background predicate for SMT2Gravatar MichalMoskal2011-02-15
* Dafny: replaced the user-defined $ite function with Boogie's built-in if-then...Gravatar rustanleino2011-02-03
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
* Boogie: Updated 'PrepareBoogieZip.ba?t'.Gravatar wuestholz2011-01-10
* Remove FSharp DLLs (no longer needed) and obsolete MakefileGravatar MichalMoskal2010-12-06
* Remove the checked in Microsoft.ContractsGravatar MichalMoskal2010-12-06
* Boogie: Updated 'PrepareBoogieZip.bat'.Gravatar wuestholz2010-12-06
* Factored out the ParserHelper class into a separate project and updated the f...Gravatar wuestholz2010-12-02
* Dafny: a partial first crack at a Dafny model-viewer provider, including capt...Gravatar rustanleino2010-11-01
* Miscellaneous changes:Gravatar rustanleino2010-10-22
* Dafny: Compilation of multi-dimensional arraysGravatar rustanleino2010-09-21
* Dafny:Gravatar rustanleino2010-09-17
* Dafny:Gravatar rustanleino2010-09-14
* Dafny: added inlined functions making reads and updates of the heap explicitGravatar sboehme2010-08-27
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* Reverting accidental check-inGravatar stobies2010-08-06
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
* <Boogie> This dll is not one that needs to be in the depot. It should be add...Gravatar tabarbe2010-07-15
* Missing file needed for new C# projects.Gravatar mikebarnett2010-07-14
* Dafny: Axiom about inverting a set union operation, similar to the recent on...Gravatar rustanleino2010-07-09
* Boogie:Gravatar rustanleino2010-06-22
* Dafny:Gravatar rustanleino2010-06-18
* Dafny:Gravatar rustanleino2010-05-21
* Script that gathers the files for the binary distribution Boogie.zip.Gravatar rustanleino2010-05-17
* Dafny:Gravatar rustanleino2010-05-13
* Changed the 'svn:ignore' property of /Binaries such that ALL currently not sv...Gravatar mschwerhoff2010-05-12
* Dafny:Gravatar rustanleino2010-05-06
* Dafny:Gravatar rustanleino2010-05-06
* Dafny:Gravatar rustanleino2010-03-31
* Dafny: Ensures that function axioms are not being used while their consisten...Gravatar rustanleino2010-03-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 05:08:18 +0000