summaryrefslogtreecommitdiff
path: root/Chalice/refinements
Commit message (Expand)AuthorAge
* Miscellaneous changes:Gravatar rustanleino2010-10-22
* Chalice:Gravatar rustanleino2010-10-09
* Chalice: fix a bug where output variables of a method were not decoupled.Gravatar kyessenov2010-10-05
* Chalice: incorporate another regression testGravatar kyessenov2010-09-03
* Chalice: added Duplicates refinement from Verification Corner videoGravatar kyessenov2010-09-02
* Chalice: working out mask transfers between concrete and abstract heaps -- ne...Gravatar kyessenov2010-08-24
* Chalice:Gravatar kyessenov2010-08-24
* Chalice: exhale spec statement post condition in refinement block translation...Gravatar kyessenov2010-08-23
* Chalice: copy concrete values for every permission in coupling invariants of ...Gravatar kyessenov2010-08-23
* Chalice:Gravatar kyessenov2010-08-23
* Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces e...Gravatar kyessenov2010-08-22
* Chalice: start of a DSW refinementGravatar kyessenov2010-08-22
* Chalice: refining lists doesn't quite work yet...Gravatar kyessenov2010-08-22
* Chalice: limited functions are still problematic (see Calculator.chalice)Gravatar kyessenov2010-08-22
* Chalice:Gravatar kyessenov2010-08-22
* Chalice:Gravatar kyessenov2010-08-21
* server-side renameGravatar kyessenov2010-08-21
* Chalice: more regression tests; cosmetic changes to codeGravatar kyessenov2010-08-19
* Chalice: added finite differencing refinementGravatar kyessenov2010-08-19
* Chalice:Gravatar kyessenov2010-08-19
* Chalice:Gravatar kyessenov2010-08-19