summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * Added expression evaluation APIGravatar Unknown2012-12-27
| * AbstractHoudini optimization: replace summary predicate with Boolean variablesGravatar Unknown2012-12-21
* | MergeGravatar Unknown2012-12-20
|\|
* | Support for "do_not_predicate" in predication of requires and ensuresGravatar Unknown2012-12-20
| * Bug fix for ExplainHoudini. Made it robust under timeouts.Gravatar Unknown2012-12-20
| * AbstractHoudini: more fixes, for self-recursionGravatar akashlal2012-12-16
| * AbstractHoudini: bug fixesGravatar akashlal2012-12-16
| * AbstractHoudini: support for generating a witnessGravatar Unknown2012-12-15
| * Added some commentsGravatar akashlal2012-12-12
| * Missed checking this in.Gravatar akashlal2012-12-12
| * MergeGravatar akashlal2012-12-12
| |\
| * | First implementation of ExplainHoudiniGravatar Unknown2012-12-12
| | * Houdini: allow cross-dependencies between procedures that occurs when assumeGravatar Unknown2012-12-11
| * | More stuff for abstract houdini; updated test caseGravatar Unknown2012-12-10
| |/
| * Bug fix for abstract-houdiniGravatar Unknown2012-12-07
| * Allow richer spec for abs-houdiniGravatar Unknown2012-12-03
* | A simplification to predication of requires and ensures.Gravatar Unknown2012-11-29
* | Fixes to uniformity analysis.Gravatar Unknown2012-11-29
| * when a query times out, all asserted candidates are droppedGravatar Unknown2012-11-25
| * Boogie build failedGravatar CodeplexBot2012-11-23
| * Disengaged Dafny testsGravatar Rustan Leino2012-11-20
| * Incorporated contribution 3667, which fixes bug in /z3exe flag (http://boogie...Gravatar Rustan Leino2012-11-20
| * Chalice build succeeded, 87 test(s) failedGravatar CodeplexBot2012-11-20
| * Gather set of procedures with irreducible loops.Gravatar Unknown2012-11-18
| * Minor refactorings for integrating corralGravatar Unknown2012-11-18
| * Added Abstract Houdini: an implementation of Houdini based on abstract domains.Gravatar Unknown2012-11-05
| * Updated PrepareBoogieZip.bat file for the binary release that just went out o...Gravatar Rustan Leino2012-10-22
| * MergeGravatar Unknown2012-10-22
| |\
| * | include Test/datatypesGravatar Unknown2012-10-22
| | * Dafny: adjusted Answer file for reorderingGravatar Rustan Leino2012-10-18
| |/
| * MergeGravatar Unknown2012-10-18
| |\ | |/ |/|
| * Dafny: added new SoundLoopUnrolling parameterGravatar Unknown2012-10-18
* | Fix for parsing error in MAXSAT computation in ProverInterface::CheckAssumpti...Gravatar Unknown2012-10-08
| * added sound loop unrollingGravatar Yannick Welsch2012-07-03
|/
* Boogie build failedGravatar CodeplexBot2012-10-05
* deleted unnecessary filesGravatar Unknown2012-10-04
* Dafny: fixed mergeGravatar Rustan Leino2012-10-04
* MergeGravatar Rustan Leino2012-10-04
|\
* | Dafny: complete implementation of iteratorsGravatar Rustan Leino2012-10-03
| * Boogie build failedGravatar CodeplexBot2012-10-04
* | Dafny: automatically update iterator _new field upon allocationsGravatar Rustan Leino2012-10-03
* | Dafny: fixed compiler bug in array allocation (reported as boogie:397957)Gravatar Rustan Leino2012-10-03
* | Dafny: good error locations for yield statements; other iterator improvements...Gravatar Rustan Leino2012-10-03
* | Dafny: more part of verifying iteratorsGravatar Rustan Leino2012-10-03
| * changed the signing to ..\InterimKey.snkGravatar qadeer2012-10-03
| * bunch of refactoringsGravatar Unknown2012-10-03
* | Dafny: changed iterator body to resolve to implicit fields rather than to the...Gravatar Rustan Leino2012-10-02
* | Dafny: handle decreases clause for iteratorsGravatar Rustan Leino2012-10-02
* | Dafny: incomplete snapshot of verification of iteratorsGravatar Rustan Leino2012-10-02
| * Fixed GPUVerify solution.Gravatar Unknown2012-10-01