| Commit message (Expand) | Author | Age |
* | Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ... | Jason Koenig | 2012-07-17 |
* | Dafny: Implemented abstract modules | Jason Koenig | 2012-06-26 |
* | Dafny: fixed a couple of compiler bugs | Unknown | 2012-06-14 |
* | Dafny: beefed up allocation axioms for boxes stored in fields | Unknown | 2012-06-12 |
* | Dafny: Added map comprehensions and updated display syntax | Unknown | 2012-05-31 |
* | Dafny: Added compilation of finite maps | Unknown | 2012-05-25 |
* | Dafny: added finite maps | Unknown | 2012-05-25 |
* | Dafny: fully qualify (with module names) names of types in the translation in... | Rustan Leino | 2012-01-05 |
* | Dafny: added comment about how to mark the run-time expression-sequencing met... | Rustan Leino | 2012-01-04 |
* | Dafny: compile let expressions efficiently (i.e., with an extra variable, not... | Rustan Leino | 2012-01-04 |
* | Dafny: moved definition of class.array into prelude, anticipating writing axi... | Rustan Leino | 2011-11-09 |
* | Dafny: removed support for assigning to an array-range (that is, an assignmen... | Rustan Leino | 2011-10-26 |
* | Dafny: implemented compilation of parallel statements | Rustan Leino | 2011-10-25 |
* | Updated 'PrepareBoogieZip.bat' to include Houdini. | wuestholz | 2011-08-23 |
* | Fixed axiom for Take/Update commuting. | Jason Koenig | 2011-07-19 |
* | Added compilation support for multisets and sequences from arrays. | Jason Koenig | 2011-07-15 |
* | Strengthened axioms for multisets and sequences. | Jason Koenig | 2011-07-14 |
* | Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi... | Jason Koenig | 2011-07-13 |
* | Multiset forming operators added. | Jason Koenig | 2011-07-11 |
* | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
* | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run... | Jason Koenig | 2011-07-08 |
* | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions | Rustan Leino | 2011-06-29 |
* | Dafny: fixed soundness problem with HeapSucc axiom | Rustan Leino | 2011-06-01 |
* | Dafny: added set comprehension expressions | Rustan Leino | 2011-05-18 |
* | Dafny: To help verifications involving sequences of (boxed) booleans along, a... | Rustan Leino | 2011-05-16 |
* | Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid... | Rustan Leino | 2011-05-11 |
* | Don't set logic to UFNIA when /useArrayTheory | Michal Moskal | 2011-05-09 |
* | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 |
* | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
* | Updated PrepareBoogieZip.bat to include BVD and smt2 | rustanleino | 2011-03-10 |
* | Add tickleBool | MichalMoskal | 2011-02-18 |
* | Dafny: | rustanleino | 2011-02-17 |
* | Provide /p: as the short form of /proverOpt:. | MichalMoskal | 2011-02-17 |
* | Make it possible to run Z3 on pipe; use generic PROVER_LOG options | MichalMoskal | 2011-02-17 |
* | Workaround bug in Z3 SMT parser | MichalMoskal | 2011-02-15 |
* | Background predicate for SMT2 | MichalMoskal | 2011-02-15 |
* | Dafny: replaced the user-defined $ite function with Boogie's built-in if-then... | rustanleino | 2011-02-03 |
* | Dafny: removed CEV instrumentation | rustanleino | 2011-02-03 |
* | Boogie: Updated 'PrepareBoogieZip.ba?t'. | wuestholz | 2011-01-10 |
* | Remove FSharp DLLs (no longer needed) and obsolete Makefile | MichalMoskal | 2010-12-06 |
* | Remove the checked in Microsoft.Contracts | MichalMoskal | 2010-12-06 |
* | Boogie: Updated 'PrepareBoogieZip.bat'. | wuestholz | 2010-12-06 |
* | Factored out the ParserHelper class into a separate project and updated the f... | wuestholz | 2010-12-02 |
* | Dafny: a partial first crack at a Dafny model-viewer provider, including capt... | rustanleino | 2010-11-01 |
* | Miscellaneous changes: | rustanleino | 2010-10-22 |
* | Dafny: Compilation of multi-dimensional arrays | rustanleino | 2010-09-21 |
* | Dafny: | rustanleino | 2010-09-17 |
* | Dafny: | rustanleino | 2010-09-14 |
* | Dafny: added inlined functions making reads and updates of the heap explicit | sboehme | 2010-08-27 |
* | Boogie: Added boolean code expressions (sans well-formedness checks on the in... | rustanleino | 2010-08-10 |