summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl...Gravatar Rustan Leino2013-03-05
* fixed a bug in ogGravatar Unknown2013-03-04
* fixed bugs in both parallel calls and linear stuff (reported by Chris)Gravatar Unknown2013-03-03
* bug in OG for parallel callGravatar Unknown2013-03-02
* added parallel callsGravatar Unknown2013-03-01
* removed call forall and * args to callsGravatar Unknown2013-02-23
* CR/LF line ending deltaGravatar Rustan Leino2013-02-19
* MergeGravatar Rustan Leino2013-02-19
|\
* | Fixed some type bugs in the interval domain.Gravatar Rustan Leino2013-02-19
| * AbstractHoudini: more details for computing a tighter predicate coverGravatar Unknown2013-02-15
| * fixed bugs in typechecking of linear setsGravatar Unknown2013-02-13
| * fixed another bug reported by ChrisHawGravatar Unknown2013-02-12
| * Further bug fixes in OGGravatar Unknown2013-02-05
| * fixed bug in OGGravatar Unknown2013-02-01
| * handling old() in stable assertionsGravatar Unknown2013-01-30
| * MergeGravatar Unknown2013-01-29
| |\
| * | made a whole bunch of changes to linear and og stuffGravatar Unknown2013-01-29
| | * Parse integers returned by Z3 into BigNumGravatar akashlal2013-01-29
| |/
| * bug fix reported by ChrisGravatar Unknown2013-01-28
| * added owicki-gries and linear-set to boogiedriverGravatar Unknown2013-01-25
| * first check in of Owicki-Gries and linear setsGravatar Unknown2013-01-24
| * Output to Boogie\Binaries even in the Release versionGravatar Unknown2013-01-25
|/
* Let Boogie clients determine their own version stringGravatar Rustan Leino2013-01-23
* Refactored code that generates an axiom for a function, and changed the prett...Gravatar Rustan Leino2013-01-17
* Timeout in AbstractHoudiniGravatar akashlal2013-01-16
* Allow attributes on procedure formals, function formals, and bound variablesGravatar Unknown2013-01-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 12:17:52 +0000