index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
Commit message (
Expand
)
Author
Age
*
Merge
Unknown
2012-08-09
|
\
*
|
Unstructured and smart predication are now default options for GPUVerify.
Unknown
2012-08-09
|
*
DafnyExtension: improvements
Rustan Leino
2012-08-08
|
*
Merge
Unknown
2012-08-08
|
|
\
|
*
|
Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and v...
Unknown
2012-08-08
*
|
|
Merge
Unknown
2012-08-07
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Revised candidate invariant generation for barrier divergence checking.
Unknown
2012-08-07
|
*
|
Houdini: recognise candidates of the form (p => (q => (... => (e => phi)))) w...
Peter Collingbourne
2012-08-07
|
/
/
*
|
Smart block predicator: track parents, and use to emit the invariant that if ...
Peter Collingbourne
2012-08-06
*
|
Smart block predicator: move *Map from parameters to fields
Peter Collingbourne
2012-08-06
*
|
Smart block predicator: drop the unused createCandidateInvariants parameter
Peter Collingbourne
2012-08-06
*
|
Dafny: corrected comment
Jason Koenig
2012-08-03
*
|
Core: attach :partition to assumes generated from structured ifs and whiles
Peter Collingbourne
2012-08-03
|
/
*
Dafny: fixed bug in reverifying allowing old locals to be modified.
Jason Koenig
2012-08-01
*
Dafny: reverify if the refining method modifies the heap.
Jason Koenig
2012-08-01
*
Dafny: fixed bug where expressions were not replaced.
Jason Koenig
2012-08-01
*
Dafny: support opening modules into the local scope
Jason Koenig
2012-07-30
*
Dafny: removed allocated keyword, changed module import syntax. "opened" keyw...
Jason Koenig
2012-07-30
*
GPUVerify: add an option which controls whether to use smart predication
Peter Collingbourne
2012-07-30
*
VCGeneration: implement smart predication
Peter Collingbourne
2012-07-30
*
Graph: make DomRelation and DominatorMap public
Peter Collingbourne
2012-07-11
*
BoogieDriver: correctly display time taken by prover if >60 seconds
Peter Collingbourne
2012-07-30
*
Dafny: removed allocated, changed semantics of fresh
Jason Koenig
2012-07-29
*
Dafny: added structural refinement check
Jason Koenig
2012-07-29
*
Merge
Unknown
2012-07-20
|
\
*
|
Implemented Houdini-based pointer analysis. Made inter-group race checking d...
Unknown
2012-07-20
|
*
Dafny: fixed datatype GetHashCode() to make it consistent with Equals()
Jason Koenig
2012-07-18
|
*
Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ...
Jason Koenig
2012-07-17
|
*
Dafny: compilation of abstract modules, including local definitions (as in mo...
Jason Koenig
2012-07-17
|
*
Dafny: allow implict self (as in "`field") in frame declarations.
Jason Koenig
2012-07-16
|
/
*
Merge
Unknown
2012-07-17
|
\
*
|
GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already e...
Unknown
2012-07-17
|
*
Dafny: update statements match up correctly in skeletons.
Jason Koenig
2012-07-13
|
*
Dafny: fixed bug in which old locals were not properly forbidden from being m...
Jason Koenig
2012-07-12
|
*
Dafny: labeled (and unlabled) block statements are now matched during refinem...
Jason Koenig
2012-07-12
|
*
Dafny: check that resolution successfully resolved all types, where appropriate.
Jason Koenig
2012-07-12
|
*
Dafny: restored soundness for refinement by disallowing certain updates and m...
Jason Koenig
2012-07-11
|
*
Dafny: fixed translation bug in maps with objects in the domain, added test case
Jason Koenig
2012-07-11
|
*
Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ...
Jason Koenig
2012-07-10
|
/
*
Merge
Unknown
2012-07-10
|
\
*
|
Read and write logging variables are now only generated if they do not alread...
Unknown
2012-07-10
|
*
Dafny: fixed bad merge
Rustan Leino
2012-07-09
|
*
Dafny: rebuilt parser/scanner after previous merge
Rustan Leino
2012-07-09
|
*
Merge
Rustan Leino
2012-07-09
|
|
\
|
*
|
Dafny: More work on the coinduction principle
Rustan Leino
2012-07-09
|
|
*
Merge
Jason Koenig
2012-07-09
|
|
|
\
|
|
*
|
Dafny: added verification that replaced expressions are the same as the original
Jason Koenig
2012-07-09
|
|
*
|
Dafny: added named expressions and replacement
Jason Koenig
2012-07-09
|
|
|
*
GPUVerify: merge blocks into predecessors before and after predication
Peter Collingbourne
2012-07-09
|
|
|
*
VCGen: add MergeBlocksIntoPredecessors function
Peter Collingbourne
2012-07-09
|
|
|
/
[next]