index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Chalice
Commit message (
Expand
)
Author
Age
*
Chalice: working out mask transfers between concrete and abstract heaps -- ne...
kyessenov
2010-08-24
*
Chalice:
kyessenov
2010-08-24
*
Chalice: exhale spec statement post condition in refinement block translation...
kyessenov
2010-08-23
*
Chalice: copy concrete values for every permission in coupling invariants of ...
kyessenov
2010-08-23
*
Chalice:
kyessenov
2010-08-23
*
Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces e...
kyessenov
2010-08-22
*
Chalice: start of a DSW refinement
kyessenov
2010-08-22
*
Chalice: refining lists doesn't quite work yet...
kyessenov
2010-08-22
*
Chalice: limited functions are still problematic (see Calculator.chalice)
kyessenov
2010-08-22
*
Chalice:
kyessenov
2010-08-22
*
Chalice:
kyessenov
2010-08-21
*
server-side rename
kyessenov
2010-08-21
*
Chalice: added syntax, printer and resolver for coupling invariants
kyessenov
2010-08-20
*
VS 2010 mode for Chalice: some errors didn't show up in the window because po...
kyessenov
2010-08-20
*
Chalice: more regression tests; cosmetic changes to code
kyessenov
2010-08-19
*
Chalice: added finite differencing refinement
kyessenov
2010-08-19
*
Chalice:
kyessenov
2010-08-19
*
Chalice:
kyessenov
2010-08-19
*
Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ...
kyessenov
2010-08-19
*
Chalice:
kyessenov
2010-08-18
*
Chalice:
kyessenov
2010-08-18
*
Chalice: added surface syntax for transform, AST matching algorithm
kyessenov
2010-08-17
*
Chalice: refactored AST code for class hierarchy (no need for caches since Sc...
kyessenov
2010-08-17
*
Chalice: bug fixes -- "check termination" flag was not properly preserved (i....
kyessenov
2010-08-16
*
Chalice: add pre-conditions to specification statements; semantically spec st...
kyessenov
2010-08-13
*
Chalice: add specification statement ( ghost? (const|var) (x (:T)?)+ [P(x)] )
kyessenov
2010-08-13
*
Chalice: accept many input files at once; read from stdin if no input file sp...
kyessenov
2010-08-12
*
Chalice: example proving a simple identity (for refinement demonstration), re...
kyessenov
2010-08-12
*
Chalice: put classes and objects into package "chalice"
kyessenov
2010-08-11
*
Chalice: fix "assume false" in the example (intended a spec statement)
kyessenov
2010-08-11
*
Chalice: finite differences with recursion instead of loops
kyessenov
2010-08-10
*
Chalice: added uninterpreted functions; attempting to re-verify Celebrity in ...
kyessenov
2010-08-10
*
Chalice: forcefully kill Boogie with taskkill /T /F on termination
kyessenov
2010-08-10
*
Chalice: refinement of a list with nodes (instead of lists pointing to sublists)
kyessenov
2010-08-06
*
Chalice: terminate Boogie subprocess manually on interrupt; Z3 still stays al...
kyessenov
2010-08-06
*
Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); ...
kyessenov
2010-08-06
*
Chalice: try using output coupling assertion as loop invariant
kyessenov
2010-08-05
*
Chalice: testing refinement of a linked list
kyessenov
2010-08-04
*
Chalice: testing refinement of Counter
kyessenov
2010-08-04
*
Chalice: abstract Shorr-Waite algorithm verified
kyessenov
2010-08-03
*
Chalice: deriving SchorrWaite algorithm with Chalice
kyessenov
2010-08-03
*
Chalice: added Tarjan's SCC algorithm for computing function call graph and r...
kyessenov
2010-08-03
*
Chalice:
kyessenov
2010-08-02
*
Chalice:
kyessenov
2010-08-02
*
Chalice:
kyessenov
2010-07-30
*
Chalice: pretty printer now prints element type for sequences; fixed a bug in...
kyessenov
2010-07-27
*
Chalice: bug -- permissions were implicity converted to Booge expressions (du...
kyessenov
2010-07-22
*
Chalice: bug -- expression substitution should preserve typing
kyessenov
2010-07-22
*
Chalice: sequence access wildcards a[*].* and a[*].f have been implemented (s...
kyessenov
2010-07-22
*
Chalice: introduced proper AST nodes for permission expressions and permissio...
kyessenov
2010-07-21
[next]