summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Expand)AuthorAge
* minor changesGravatar Checkmate502016-06-06
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
* Added initial support for float additionGravatar Checkmate502015-09-17
* Added the fp32 class, copied from the previously existing BigDec class. No s...Gravatar Dietrich2015-04-17
* The back pred files have been eliminated. The small backpred string is now d...Gravatar qadeer2013-12-08
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl...Gravatar Rustan Leino2013-03-05
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl...Gravatar Rustan Leino2013-03-05
* Updated PrepareBoogieZip.bat file for the binary release that just went out o...Gravatar Rustan Leino2012-10-22
* deleted unnecessary filesGravatar Unknown2012-10-04
* Dafny: fixed mergeGravatar Rustan Leino2012-10-04
* MergeGravatar Rustan Leino2012-10-04
|\
* | Dafny: complete implementation of iteratorsGravatar Rustan Leino2012-10-03
* | Dafny: more part of verifying iteratorsGravatar Rustan Leino2012-10-03
* | Dafny: incomplete snapshot of verification of iteratorsGravatar Rustan Leino2012-10-02
| * Updated the 'PrepareBoogieZip.bat' script.Gravatar wuestholz2012-10-01
| * Dafny: removed div/mod axioms, since Boogie now interprets div/modGravatar Unknown2012-09-28
| * Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
| * Boogie: new syntax for integer division and modulus: use div and mod instead ...Gravatar boehmes2012-09-27
|/
* Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ...Gravatar Unknown2012-09-12
* Implement support for alternative SMT solvers -- CVC3 and CVC4Gravatar Peter Collingbourne2012-09-06
* Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ...Gravatar Jason Koenig2012-07-17
* Dafny: Implemented abstract modulesGravatar Jason Koenig2012-06-26
* Dafny: fixed a couple of compiler bugsGravatar Unknown2012-06-14
* Dafny: beefed up allocation axioms for boxes stored in fieldsGravatar Unknown2012-06-12
* Dafny: Added map comprehensions and updated display syntaxGravatar Unknown2012-05-31
* Dafny: Added compilation of finite mapsGravatar Unknown2012-05-25
* Dafny: added finite mapsGravatar Unknown2012-05-25
* Dafny: fully qualify (with module names) names of types in the translation in...Gravatar Rustan Leino2012-01-05
* Dafny: added comment about how to mark the run-time expression-sequencing met...Gravatar Rustan Leino2012-01-04
* Dafny: compile let expressions efficiently (i.e., with an extra variable, not...Gravatar Rustan Leino2012-01-04
* Dafny: moved definition of class.array into prelude, anticipating writing axi...Gravatar Rustan Leino2011-11-09
* Dafny: removed support for assigning to an array-range (that is, an assignmen...Gravatar Rustan Leino2011-10-26
* Dafny: implemented compilation of parallel statementsGravatar Rustan Leino2011-10-25
* Updated 'PrepareBoogieZip.bat' to include Houdini.Gravatar wuestholz2011-08-23
* Fixed axiom for Take/Update commuting.Gravatar Jason Koenig2011-07-19
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-25 14:57:28 +0000