Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Normalise line endings using a .gitattributes file. Unfortunately | 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. | 2014-05-19 | |
| | |||
* | various updates | 2013-12-09 | |
| | |||
* | changed the output path for the QED build configuration to the Binaries folder | 2013-12-08 | |
| | |||
* | added the QED build configuration | 2013-12-02 | |
| | |||
* | merge | 2013-07-06 | |
|\ | |||
| * | Did some refactoring in the execution engine and worked on the parallelization. | 2013-06-21 | |
| | | |||
| * | Removed unused code. | 2013-06-13 | |
| | | |||
* | | CVC4 Parser | 2013-06-12 | |
|/ | |||
* | Did some refactoring in the Boogie driver. | 2013-06-03 | |
| | |||
* | Did some refactoring in the Boogie driver. | 2013-06-03 | |
| | |||
* | Did some refactoring in the Boogie driver. | 2013-06-03 | |
| | |||
* | Did some refactoring in the Boogie driver. | 2013-06-03 | |
| | |||
* | Did some refactoring in the Boogie driver. | 2013-06-03 | |
| | |||
* | Fixed an issue with discovering program snapshots. | 2013-06-03 | |
| | |||
* | Added a feature for verifying several program snapshots (incl. result ↵ | 2013-06-02 | |
| | | | | caching and prioritization). | ||
* | Changed the prover interface to report traces for time outs and out of memory. | 2013-05-30 | |
| | |||
* | fixed bug in reporting the number of typechecking errors | 2013-05-22 | |
| | | | | updated answer file | ||
* | Merge | 2013-05-18 | |
|\ | |||
* | | reworked the linear and og implementation based on available variables theory | 2013-05-18 | |
| | | |||
| * | Adapted Houdini algorithm to take staging into account | 2013-05-18 | |
|/ | |||
* | AbsHoudini: Tolerate some assertion failing. Updated regression baseline. | 2013-05-10 | |
| | |||
* | merging changes for fixedpoint engine backend | 2013-05-07 | |
|\ | |||
* | | Adding fixedpoint engine backend | 2013-05-07 | |
| | | |||
| * | AbsHoudini: Each function can specify its own abstract domain. Also added | 2013-05-05 | |
| | | | | | | | | typechecking | ||
| * | Merge | 2013-05-04 | |
| |\ | |||
| * | | fixed bug reported by Akash | 2013-05-04 | |
|/ / | |||
| * | Some code refactoring | 2013-05-03 | |
|/ | |||
* | Merge | 2013-04-30 | |
|\ | |||
* | | Staged Houdini | 2013-04-30 | |
| | | |||
| * | AbsHoudini: Added support for /errorLimit:n, n > 1 | 2013-04-25 | |
| | | |||
| * | AbsHoudini: Added predicate-abstraction domain and some examples. | 2013-04-25 | |
| | | |||
| * | AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini, | 2013-04-25 | |
| | | | | | | | | few bug fixes, hack to support missing prover declarations. | ||
| * | AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute, | 2013-04-19 | |
| | | | | | | | | intervals domain | ||
| * | AbsHoudini: Added support for /inlineDepth, and fixed the regression tests | 2013-04-18 | |
| | | | | | | | | (all pass) | ||
| * | Nice clean re-implementation of AbstractHoudini. And tests | 2013-04-18 | |
|/ | |||
* | fixed bugs in both parallel calls and linear stuff (reported by Chris) | 2013-03-03 | |
| | | | | also added improved error reporting suggested by Chris | ||
* | fixed bug in OG | 2013-02-01 | |
| | | | | added another OG sample illustrating rely-guarantee encoding | ||
* | made a whole bunch of changes to linear and og stuff | 2013-01-29 | |
| | |||
* | bug fix reported by Chris | 2013-01-28 | |
| | |||
* | added owicki-gries and linear-set to boogiedriver | 2013-01-25 | |
| | | | | cleaned up the async type checking | ||
* | Output to Boogie\Binaries even in the Release version | 2013-01-25 | |
| | |||
* | Some more changes to AbsHoudini | 2012-12-28 | |
| | |||
* | AbstractHoudini: bug fixes | 2012-12-16 | |
| | |||
* | More stuff for abstract houdini; updated test case | 2012-12-10 | |
| | |||
* | Allow richer spec for abs-houdini | 2012-12-03 | |
| | |||
* | Added Abstract Houdini: an implementation of Houdini based on abstract domains. | 2012-11-05 | |
| | | | | Currently only predicate-abstraction domain is supported. | ||
* | added sound loop unrolling | 2012-07-03 | |
| | |||
* | bunch of refactorings | 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 ↵ | 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. |