summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Some code clean-upGravatar Unknown2013-01-07
* Removed old comments about "BASEMOVE" and other constructor calls, where the ...Gravatar Unknown2013-01-07
* bug fix for interaction between inlining and loopsGravatar Unknown2013-01-04
* bug fix in model printingGravatar Unknown2013-01-04
* Use the new ProverInterface's Evaluate method in stratified inlinigGravatar Unknown2013-01-03
* bug fixGravatar Unknown2012-12-28
* extended Evaluate to handle more typesGravatar Unknown2012-12-28
* Some more changes to AbsHoudiniGravatar akashlal2012-12-28
* minor bug fixGravatar Unknown2012-12-27
* Added expression evaluation APIGravatar Unknown2012-12-27
* AbstractHoudini optimization: replace summary predicate with Boolean variablesGravatar Unknown2012-12-21
* 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
* 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