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: white space delta in test file
rustanleino
2010-11-17
*
Chalice: Automatically created a simple class diagram of the current AST
mschwerhoff
2010-11-13
*
Chalice: Added axioms about div and mod. Updated DuplicatesVideo.chalice
rustanleino
2010-11-06
*
Miscellaneous changes:
rustanleino
2010-10-22
*
Chalice: Now compiles with Scala 2.7.7 and 2.8.0, the latter yields many warn...
mschwerhoff
2010-10-21
*
Chalice: allow replace by to match LocalVar
kyessenov
2010-10-09
*
Chalice:
rustanleino
2010-10-09
*
Chalice: permit replaces by to match assign clauses
kyessenov
2010-10-09
*
Chalice: fix a bug where output variables of a method were not decoupled.
kyessenov
2010-10-05
*
Chalice: incorporate another regression test
kyessenov
2010-09-03
*
Chalice: added Duplicates refinement from Verification Corner video
kyessenov
2010-09-02
*
Chalice: fix in refinement loop target resolution; added "spec" as a keyword ...
kyessenov
2010-09-02
*
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
[next]