Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Normalise line endings using a .gitattributes file. Unfortunately | Dan Liew | 2015-06-28 |
| | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | ||
* | Made the Boogie driver return an exit code. | wuestholz | 2014-05-19 |
| | |||
* | various updates | qadeer | 2013-12-09 |
| | |||
* | changed the output path for the QED build configuration to the Binaries folder | qadeer | 2013-12-08 |
| | |||
* | added the QED build configuration | qadeer | 2013-12-02 |
| | |||
* | merge | Pantazis Deligiannis | 2013-07-06 |
|\ | |||
| * | Did some refactoring in the execution engine and worked on the parallelization. | wuestholz | 2013-06-21 |
| | | |||
| * | Removed unused code. | wuestholz | 2013-06-13 |
| | | |||
* | | CVC4 Parser | pantazis | 2013-06-12 |
|/ | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Fixed an issue with discovering program snapshots. | wuestholz | 2013-06-03 |
| | |||
* | Added a feature for verifying several program snapshots (incl. result ↵ | wuestholz | 2013-06-02 |
| | | | | caching and prioritization). | ||
* | Changed the prover interface to report traces for time outs and out of memory. | wuestholz | 2013-05-30 |
| | |||
* | fixed bug in reporting the number of typechecking errors | Unknown | 2013-05-22 |
| | | | | updated answer file | ||
* | Merge | Unknown | 2013-05-18 |
|\ | |||
* | | reworked the linear and og implementation based on available variables theory | Unknown | 2013-05-18 |
| | | |||
| * | Adapted Houdini algorithm to take staging into account | allydonaldson | 2013-05-18 |
|/ | |||
* | AbsHoudini: Tolerate some assertion failing. Updated regression baseline. | akashlal | 2013-05-10 |
| | |||
* | merging changes for fixedpoint engine backend | Ken McMillan | 2013-05-07 |
|\ | |||
* | | Adding fixedpoint engine backend | Ken McMillan | 2013-05-07 |
| | | |||
| * | AbsHoudini: Each function can specify its own abstract domain. Also added | akashlal | 2013-05-05 |
| | | | | | | | | typechecking | ||
| * | Merge | Unknown | 2013-05-04 |
| |\ | |||
| * | | fixed bug reported by Akash | Unknown | 2013-05-04 |
|/ / | |||
| * | Some code refactoring | akashlal | 2013-05-03 |
|/ | |||
* | Merge | allydonaldson | 2013-04-30 |
|\ | |||
* | | Staged Houdini | allydonaldson | 2013-04-30 |
| | | |||
| * | AbsHoudini: Added support for /errorLimit:n, n > 1 | akashlal | 2013-04-25 |
| | | |||
| * | AbsHoudini: Added predicate-abstraction domain and some examples. | akashlal | 2013-04-25 |
| | | |||
| * | AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini, | akashlal | 2013-04-25 |
| | | | | | | | | few bug fixes, hack to support missing prover declarations. | ||
| * | AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute, | akashlal | 2013-04-19 |
| | | | | | | | | intervals domain | ||
| * | AbsHoudini: Added support for /inlineDepth, and fixed the regression tests | akashlal | 2013-04-18 |
| | | | | | | | | (all pass) | ||
| * | Nice clean re-implementation of AbstractHoudini. And tests | akashlal | 2013-04-18 |
|/ | |||
* | fixed bugs in both parallel calls and linear stuff (reported by Chris) | Unknown | 2013-03-03 |
| | | | | also added improved error reporting suggested by Chris | ||
* | fixed bug in OG | Unknown | 2013-02-01 |
| | | | | added another OG sample illustrating rely-guarantee encoding | ||
* | made a whole bunch of changes to linear and og stuff | Unknown | 2013-01-29 |
| | |||
* | bug fix reported by Chris | Unknown | 2013-01-28 |
| | |||
* | added owicki-gries and linear-set to boogiedriver | Unknown | 2013-01-25 |
| | | | | cleaned up the async type checking | ||
* | Output to Boogie\Binaries even in the Release version | Unknown | 2013-01-25 |
| | |||
* | Some more changes to AbsHoudini | akashlal | 2012-12-28 |
| | |||
* | AbstractHoudini: bug fixes | akashlal | 2012-12-16 |
| | |||
* | More stuff for abstract houdini; updated test case | Unknown | 2012-12-10 |
| | |||
* | Allow richer spec for abs-houdini | Unknown | 2012-12-03 |
| | |||
* | Added Abstract Houdini: an implementation of Houdini based on abstract domains. | Unknown | 2012-11-05 |
| | | | | Currently only predicate-abstraction domain is supported. | ||
* | added sound loop unrolling | Yannick Welsch | 2012-07-03 |
| | |||
* | bunch of refactorings | Unknown | 2012-10-03 |
| | | | | | | | | | - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs | ||
* | Removed AIFramework from Boogie -- use native trivial or native ↵ | boehmes | 2012-09-27 |
| | | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped. |