summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
Commit message (Expand)AuthorAge
* Added several test cases and some basic documentation for fp usageGravatar Checkmate502016-01-04
* Made the Boogie driver return an exit code.Gravatar wuestholz2014-05-19
* various updatesGravatar qadeer2013-12-09
* changed the output path for the QED build configuration to the Binaries folderGravatar qadeer2013-12-08
* added the QED build configurationGravatar qadeer2013-12-02
* mergeGravatar Pantazis Deligiannis2013-07-06
|\
| * Did some refactoring in the execution engine and worked on the parallelization.Gravatar wuestholz2013-06-21
| * Removed unused code.Gravatar wuestholz2013-06-13
* | CVC4 ParserGravatar pantazis2013-06-12
|/
* Did some refactoring in the Boogie driver.Gravatar wuestholz2013-06-03
* Did some refactoring in the Boogie driver.Gravatar wuestholz2013-06-03
* Did some refactoring in the Boogie driver.Gravatar wuestholz2013-06-03
* Did some refactoring in the Boogie driver.Gravatar wuestholz2013-06-03
* Did some refactoring in the Boogie driver.Gravatar wuestholz2013-06-03
* Fixed an issue with discovering program snapshots.Gravatar wuestholz2013-06-03
* Added a feature for verifying several program snapshots (incl. result caching...Gravatar wuestholz2013-06-02
* Changed the prover interface to report traces for time outs and out of memory.Gravatar wuestholz2013-05-30
* fixed bug in reporting the number of typechecking errorsGravatar Unknown2013-05-22
* MergeGravatar Unknown2013-05-18
|\
* | reworked the linear and og implementation based on available variables theoryGravatar Unknown2013-05-18
| * Adapted Houdini algorithm to take staging into accountGravatar allydonaldson2013-05-18
|/
* AbsHoudini: Tolerate some assertion failing. Updated regression baseline.Gravatar akashlal2013-05-10
* merging changes for fixedpoint engine backendGravatar Ken McMillan2013-05-07
|\
* | Adding fixedpoint engine backendGravatar Ken McMillan2013-05-07
| * AbsHoudini: Each function can specify its own abstract domain. Also addedGravatar akashlal2013-05-05
| * MergeGravatar Unknown2013-05-04
| |\
| * | fixed bug reported by AkashGravatar Unknown2013-05-04
|/ /
| * Some code refactoringGravatar akashlal2013-05-03
|/
* MergeGravatar allydonaldson2013-04-30
|\
* | Staged HoudiniGravatar allydonaldson2013-04-30
| * AbsHoudini: Added support for /errorLimit:n, n > 1Gravatar akashlal2013-04-25
| * AbsHoudini: Added predicate-abstraction domain and some examples.Gravatar akashlal2013-04-25
| * AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,Gravatar akashlal2013-04-25
| * AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute,Gravatar akashlal2013-04-19
| * AbsHoudini: Added support for /inlineDepth, and fixed the regression testsGravatar akashlal2013-04-18
| * Nice clean re-implementation of AbstractHoudini. And testsGravatar akashlal2013-04-18
|/
* fixed bugs in both parallel calls and linear stuff (reported by Chris)Gravatar Unknown2013-03-03
* fixed bug in OGGravatar Unknown2013-02-01
* made a whole bunch of changes to linear and og stuffGravatar Unknown2013-01-29
* bug fix reported by ChrisGravatar Unknown2013-01-28
* added owicki-gries and linear-set to boogiedriverGravatar Unknown2013-01-25
* Output to Boogie\Binaries even in the Release versionGravatar Unknown2013-01-25
* Some more changes to AbsHoudiniGravatar akashlal2012-12-28
* AbstractHoudini: bug fixesGravatar akashlal2012-12-16
* More stuff for abstract houdini; updated test caseGravatar Unknown2012-12-10
* Allow richer spec for abs-houdiniGravatar Unknown2012-12-03
* Added Abstract Houdini: an implementation of Houdini based on abstract domains.Gravatar Unknown2012-11-05
* added sound loop unrollingGravatar Yannick Welsch2012-07-03
* bunch of refactoringsGravatar Unknown2012-10-03
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27