summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Boogie build succeeded, 29 test(s) failedGravatar codeplexbot2010-10-08
* Add one more fileGravatar MichalMoskal2010-10-07
* Get rid of some CCI dependencies in DriverGravatar MichalMoskal2010-10-07
* Update to include all build artifacts, also from DafnyGravatar MichalMoskal2010-10-07
* Update to VS2010.Gravatar MichalMoskal2010-10-07
* Chalice: fix a bug where output variables of a method were not decoupled.Gravatar kyessenov2010-10-05
* Minor fix to recursion depth in stratified inlining algorithm.Gravatar akashlal2010-10-02
* Util: Minor changes to the LaTeX listings packages for Boogie and Dafny.Gravatar wuestholz2010-09-30
* Boogie:Gravatar rustanleino2010-09-24
* Boogie build succeededGravatar codeplexbot2010-09-23
* Boogie:Gravatar rustanleino2010-09-23
* Dafny: Compilation of multi-dimensional arraysGravatar rustanleino2010-09-21
* Boogie build succeededGravatar codeplexbot2010-09-20
* Some simplifications to coverage reporting for StratifiedInlining.Gravatar akashlal2010-09-19
* Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.Gravatar akashlal2010-09-18
* Added test for loop extractionGravatar akashlal2010-09-18
* Boogie build succeededGravatar codeplexbot2010-09-17
* Dafny:Gravatar rustanleino2010-09-17
* Added more stat printingGravatar akashlal2010-09-16
* Boogie build succeededGravatar codeplexbot2010-09-15
* Dafny:Gravatar rustanleino2010-09-14
* Boogie build succeededGravatar codeplexbot2010-09-11
* added an optimization to extract loops so that only loop targets are treated ...Gravatar qadeer2010-09-10
* Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal tha...Gravatar akashlal2010-09-05
* Delete unreachable Blocks of an Impl before calling ExtractLoops().Gravatar akashlal2010-09-05
* Fixed a performance issue with StratifiedInliningGravatar akashlal2010-09-05
* Added tests for extractloopsGravatar akashlal2010-09-04
* Fix for extractLoopsGravatar akashlal2010-09-04
* Henrique's addition to the the ErrorHandler API to retrieve modelsGravatar qadeer2010-09-03
* Chalice: incorporate another regression testGravatar kyessenov2010-09-03
* more fixes to ExtractLoopsGravatar qadeer2010-09-03
* Added a fix to extract loops code so that it returns a more comprehensive map...Gravatar qadeer2010-09-03
* Changed the interface of Parse so that it can consume a program from a StreamGravatar akashlal2010-09-03
* bunch of fixes related to Boogie error model generation from the Z3 error mod...Gravatar qadeer2010-09-03
* Vim: add keywords to ChaliceGravatar kyessenov2010-09-02
* VS 2010: add "spec" as keyword in ChaliceGravatar kyessenov2010-09-02
* Chalice: added Duplicates refinement from Verification Corner videoGravatar kyessenov2010-09-02
* Chalice: fix in refinement loop target resolution; added "spec" as a keyword ...Gravatar kyessenov2010-09-02
* Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ...Gravatar akashlal2010-09-02
* fixed bug in extract loops by ensuring that loop extraction is done in nestin...Gravatar qadeer2010-09-01
* Minor fix to my previous commitGravatar akashlal2010-09-01
* Added a way of recovering counterexample paths after loop extraction. Stable,...Gravatar akashlal2010-09-01
* Version-stamp CCE assemblyGravatar stobies2010-09-01
* Boogie build succeededGravatar codeplexbot2010-09-01
* Added a new class LoopProcedure to represent the procedures representing extr...Gravatar qadeer2010-09-01
* Dafny: Added Dafny solutions to the VSComp 2010 problemsGravatar rustanleino2010-09-01
* VS2010 mode for Dafny and Boogie: updated, for example to properly deal with...Gravatar rustanleino2010-09-01
* Boogie build succeededGravatar codeplexbot2010-08-31
* Dafny: added a command-line option to change the prelude fileGravatar sboehme2010-08-30
* added a new api to Z3apiProcessTheoremProver for asserting axiomsGravatar qadeer2010-08-29