summaryrefslogtreecommitdiff
path: root/Chalice
Commit message (Expand)AuthorAge
...
* Chalice: refinement of a list with nodes (instead of lists pointing to sublists)Gravatar kyessenov2010-08-06
* Chalice: terminate Boogie subprocess manually on interrupt; Z3 still stays al...Gravatar kyessenov2010-08-06
* Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); ...Gravatar kyessenov2010-08-06
* Chalice: try using output coupling assertion as loop invariantGravatar kyessenov2010-08-05
* Chalice: testing refinement of a linked listGravatar kyessenov2010-08-04
* Chalice: testing refinement of CounterGravatar kyessenov2010-08-04
* Chalice: abstract Shorr-Waite algorithm verifiedGravatar kyessenov2010-08-03
* Chalice: deriving SchorrWaite algorithm with ChaliceGravatar kyessenov2010-08-03
* Chalice: added Tarjan's SCC algorithm for computing function call graph and r...Gravatar kyessenov2010-08-03
* Chalice:Gravatar kyessenov2010-08-02
* Chalice:Gravatar kyessenov2010-08-02
* Chalice:Gravatar kyessenov2010-07-30
* Chalice: pretty printer now prints element type for sequences; fixed a bug in...Gravatar kyessenov2010-07-27
* Chalice: bug -- permissions were implicity converted to Booge expressions (du...Gravatar kyessenov2010-07-22
* Chalice: bug -- expression substitution should preserve typingGravatar kyessenov2010-07-22
* Chalice: sequence access wildcards a[*].* and a[*].f have been implemented (s...Gravatar kyessenov2010-07-22
* Chalice: introduced proper AST nodes for permission expressions and permissio...Gravatar kyessenov2010-07-21
* Chalice: fixed typos in strings; trying out committing with TFSGravatar kyessenov2010-07-21
* Chalice: added surface syntax for acc(s[*].*) and acc(s[*].f); extended AST, ...Gravatar kyessenov2010-07-20
* Chalice: fixed a bug with permission operations treating AccessAll not as a p...Gravatar kyessenov2010-07-20
* Chalice: added type information for sequences ("where" clauses in local varia...Gravatar kyessenov2010-07-20
* Chalice: adding support for sequence local variables; removed ClassType from ...Gravatar kyessenov2010-07-20
* Chalice: extended substitutor to handle "exists" quantifier and sequence cont...Gravatar kyessenov2010-07-20
* VS2010 integration: fixed typo in Boogie mode (install for .bpl files, not .d...Gravatar rustanleino2010-07-19
* Chalice: added sequence containment surface syntax ("in" comparison operator)...Gravatar kyessenov2010-07-19
* Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S }'....Gravatar rustanleino2010-07-19
* Chalice: added "exists" quantifier; changed surface syntax for quantifier exp...Gravatar kyessenov2010-07-19
* Chalice: Re-designed lockchange on methods and loops. The lockchange clause i...Gravatar mueller2010-07-18
* Chalice: Removed the restriction that "holds" must occur only in positive pos...Gravatar mueller2010-07-16
* Chalice: revert minor commit; add cygwin python make scriptGravatar kyessenov2010-07-15
* Oops, reverted my local changes to the build script.Gravatar kyessenov2010-07-15
* Chalice: fix a bug for boogie print-out of a sequence classGravatar kyessenov2010-07-15
* Chalice: No longer use Mask for "held" field; instead, only use the value of...Gravatar rustanleino2010-07-14
* Chalice: Changed definition of waitlevel to take into account rdlock. Adapted...Gravatar mueller2010-07-03
* Chalice:Gravatar rustanleino2010-06-25
* Chalice: Applied patch #6192Gravatar mueller2010-06-25
* Chalice: fixed bug in the exhale of permissions (to handle negative epsilons)Gravatar mueller2010-06-09
* Chalice: Implemented -vs switch, for use when running Chalice from inside Vi...Gravatar rustanleino2010-01-15
* Chalice: updated Prelude to match new Boogie parsing of function parameters; ...Gravatar rustanleino2010-01-06
* Applied patch 4316, which fixes an unsoundness in the axiomatization of seque...Gravatar rustanleino2009-11-05
* - Sieve.chalice verifies + executes fasterGravatar jansmans2009-10-20
* - the "-gen" option works only if the program verifiesGravatar jansmans2009-10-16
* Implicitly declare as local variables undeclared variables occurring as LHS's...Gravatar rustanleino2009-10-16
* Sieve of Eratosthenes, written in Chalice.Gravatar rustanleino2009-10-15
* - fixed a positioning bug in Parser.scalaGravatar jansmans2009-10-07
* - extended to example to use acknowledgements (but uses sending debit)Gravatar jansmans2009-10-07
* - verified a program inpsired by "Copyless Message Passing" in ChaliceGravatar jansmans2009-10-07
* - where clauses are now properly type-checkedGravatar jansmans2009-10-02
* Implemented -noDeadlockChecks mode. With this mode, it is possible to give s...Gravatar rustanleino2009-10-01
* - made the output of the Chalice-to-C# translator slightly nicerGravatar jansmans2009-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 09:45:02 +0000