index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Binaries
Commit message (
Expand
)
Author
Age
*
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
*
Reverting accidental check-in
stobies
2010-08-06
[next]