index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
Commit message (
Expand
)
Author
Age
*
changed the semantics of requires and ensures for inlined procedures
qadeer
2011-11-17
*
/contractInfer always prints the computed assignment now
qadeer
2011-11-16
*
Merge
Rustan Leino
2011-11-15
|
\
*
|
Added Dafny solutions to the VSTTE 2012 program verification competition
Rustan Leino
2011-11-15
*
|
Dafny: added let expressions (syntax: "var x := E0; E1")
Rustan Leino
2011-11-14
|
*
added the option /inlineDepth:n. This option defaults to -1. If the user prov...
qadeer
2011-11-13
*
|
Dafny: implemented the wellformedness check that datatype destructors are onl...
Rustan Leino
2011-11-11
|
/
*
Many, many bug fixes related to generics and some other random problems.
Mike Barnett
2011-11-10
*
Dafny: allow assert/assume expressions in more places
Rustan Leino
2011-11-09
*
Dafny: added assert/assume expressions
Rustan Leino
2011-11-09
*
Dafny: fixed part of a type-inference issue with datatypes and the < operator...
Rustan Leino
2011-11-09
*
Dafny: fixed bug in reads checking of array-to-sequence conversions
Rustan Leino
2011-11-08
*
Dafny: Cleaned up proof of RevConcat in test case
Rustan Leino
2011-11-08
*
Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ...
Rustan Leino
2011-11-04
*
Added some Dafny and Boogie test cases, including Turing's factorial program,...
Rustan Leino
2011-11-03
*
Merge
Rustan Leino
2011-10-31
|
\
|
*
File to experiment with type encoding for .NET.
Mike Barnett
2011-10-31
*
|
Merge
Rustan Leino
2011-10-31
|
\
\
|
|
/
|
/
|
*
|
Removed prover option from runtest.bat because smtlib is now the default
Mike Barnett
2011-10-30
|
*
Merge
Rustan Leino
2011-10-29
|
|
\
|
|
/
|
/
|
|
*
Dafny induction:
Rustan Leino
2011-10-29
*
|
Boogie: Get rid of {:inline} attributes on axioms
Michal Moskal
2011-10-27
*
|
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...
Rustan Leino
2011-10-27
|
/
*
Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s...
Rustan Leino
2011-10-26
*
Dafny: removed support for assigning to an array-range (that is, an assignmen...
Rustan Leino
2011-10-26
*
Merge
Rustan Leino
2011-10-26
|
\
*
|
Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while performanc...
Rustan Leino
2011-10-26
|
*
Added batch script to run tests for datatypes tests.
Mike Barnett
2011-10-26
*
|
Dafny: implemented compilation of parallel statements
Rustan Leino
2011-10-25
*
|
Dafny: check subrange restriction in parallel Assign statement
Rustan Leino
2011-10-24
|
/
*
Dafny: continued translation of "parallel" statements (Assign and Proof forms...
Rustan Leino
2011-10-24
*
Dafny: added translation of Assign case of the parallel statement
Rustan Leino
2011-10-22
*
Dafny: changed triggers (which are never really used, anyhow) from having a s...
Rustan Leino
2011-10-21
*
Dafny: fixed performance-buggy translation of exists, and also added some oth...
Rustan Leino
2011-10-19
*
Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)
Unknown
2011-10-19
*
added houdini to regression
qadeer
2011-10-17
*
Dafny: added COST Verification Competition challenge programs to test suite
Rustan Leino
2011-10-07
*
added membership tests
qadeer
2011-10-05
*
implementing datatypes
qadeer
2011-10-05
*
Merge
Rustan Leino
2011-09-30
|
\
*
|
Dafny: Updated snapshotable tree to remove IsReadonly precondition for Create...
Rustan Leino
2011-09-30
*
|
Dafny: fixed bug in translator when LHS of a call was an array element or a nat
Rustan Leino
2011-09-30
|
*
Merge
qadeer
2011-09-30
|
|
\
|
*
|
bug fix in houdini
qadeer
2011-09-30
|
|
*
Dafny: Fixed the 'Answer' file for test 'dafny2'.
wuestholz
2011-09-30
|
|
/
*
/
Dafny: beautification in one test case, and fixed an Answer file
Rustan Leino
2011-09-29
|
/
*
Dafny: Added TreeBarrier as a test case
peter mueller peter.mueller@inf.ethz.ch
2011-09-29
*
Merge
Rustan Leino
2011-09-28
|
\
|
*
Updated the ANSWER file for 'test15'.
wuestholz
2011-09-27
*
|
Merge
Rustan Leino
2011-09-17
|
\
\
[next]