Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | 2013-12-14 | |
|\ | |||
* | | fixed type checking errors in QED stuff | 2013-12-14 | |
| | | |||
| * | Resolve a concurrency issue (reported by Alex Summers). | 2013-12-12 | |
|/ | |||
* | fixes to type checking code | 2013-12-11 | |
| | |||
* | Updates on YieldTypeCheck | 2013-12-11 | |
| | |||
* | Remove some (redundant) preconditions to avoid 'ccrewrite' errors. | 2013-12-11 | |
| | |||
* | some refactoring of QED stuff | 2013-12-10 | |
| | |||
* | various updates | 2013-12-09 | |
| | |||
* | Merge | 2013-12-09 | |
|\ | |||
* | | Small change related to CVC4 support. Patch by Pantazis Deligiannis | 2013-12-09 | |
| | | |||
| * | Expose certain program transformations in the execution engine to invoke ↵ | 2013-12-09 | |
| | | | | | | | | them from Dafny. | ||
| * | debug hastags are inserted to yieldtypechecker | 2013-12-08 | |
| | | |||
| * | changed the output path for the QED build configuration to the Binaries folder | 2013-12-08 | |
| | | |||
| * | The back pred files have been eliminated. The small backpred string is now ↵ | 2013-12-08 | |
| | | | | | | | | directly included in ProverInterface.cs. | ||
| * | removed bitvector analysis from Boogie | 2013-12-08 | |
|/ | | | | an advanced version has been moved to Corral | ||
* | Proper transition tags added for providing language containtment between two ↵ | 2013-12-07 | |
| | | | | Autos. | ||
* | fixed a bug regarding invocation of modsetanalysis w.r.t. OG desugaring | 2013-12-07 | |
| | |||
* | Automata.dll functions are used to create Automata from Graph | 2013-12-06 | |
| | |||
* | Some bugs on yieldtypechecker graph solved | 2013-12-05 | |
| | |||
* | Building raw graphs of YieldTypeChecker for building Automata is added | 2013-12-04 | |
| | |||
* | first check in | 2013-12-04 | |
| | |||
* | updated the reference in Concurrency.csproj to Microsoft.Automata.dll (after ↵ | 2013-12-02 | |
| | | | | Margus supplied the signed dll) | ||
* | forgot to add this file | 2013-12-02 | |
| | |||
* | Merge | 2013-12-02 | |
|\ | |||
* | | added the QED build configuration | 2013-12-02 | |
| | | |||
| * | Patch by Nathan Chong: iterative version of remove empty blocks algorithm. ↵ | 2013-12-02 | |
|/ | | | | This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems. | ||
* | binary tree of ANDs saves stack space | 2013-11-29 | |
| | |||
* | added some type checking code | 2013-11-25 | |
| | |||
* | moved some files around | 2013-11-22 | |
| | |||
* | factored the concurrency checking code into a separate project | 2013-11-22 | |
| | |||
* | do monomorphic checking | 2013-11-22 | |
| | |||
* | Fixedpoint VC catch up with recent changes | 2013-11-11 | |
| | |||
* | Merge duality changes to mainline | 2013-11-09 | |
|\ | |||
| * | handling timeouts for fixedpoint engines | 2013-11-09 | |
| | | |||
* | | Merge | 2013-11-07 | |
|\ \ | |||
| * | | Fixes to predication. Patch by Jeroen Ketema. | 2013-11-06 | |
| | | | |||
| * | | code cleanup | 2013-11-02 | |
| | | | |||
| * | | AbsHoudini: Support timeout, MakeTop, InlineFunctions | 2013-11-02 | |
| | | | |||
| * | | ProverInterface: model isn't available on timeout | 2013-11-02 | |
| | | | |||
| * | | Merge | 2013-10-25 | |
| |\ \ | |||
| * | | | minor refactoring | 2013-10-25 | |
| | | | | | | | | | | | | | | | | moved the call to EliminateDeadVariablesAndInline to after the OG sequentialization | ||
| * | | | a minor refactoring + implemented mover checking | 2013-10-25 | |
| | | | | |||
| | * | | and a test case | 2013-10-25 | |
| | | | | |||
| | * | | Stratified inlining: inject free requires as assumes at call site | 2013-10-25 | |
| | | | | |||
| | * | | change of identifier names in OG | 2013-10-25 | |
| |/ / | |||
| * | | And a test case | 2013-10-21 | |
| | | | |||
| * | | Bug fix in stratified inlining (triggered by {:inline} functions) | 2013-10-21 | |
| | | | |||
* | | | Merge | 2013-10-16 | |
|\| | | |||
* | | | small fix in the parallel refutation sharing | 2013-10-16 | |
| | | | |||
| * | | Merge | 2013-10-15 | |
| |\ \ |