Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Minor Changes in YieldTypeChecker | kuruis | 2013-12-19 |
| | |||
* | Merge | qadeer | 2013-12-19 |
|\ | |||
* | | various updates and tighter integration of QED stuff into mainline | qadeer | 2013-12-19 |
| | | |||
| * | Epsilon reduction per phase automaton added | kuruis | 2013-12-18 |
| | | |||
| * | Updates on YieldTypeChecker done | kuruis | 2013-12-17 |
| | | |||
| * | Fixed another :never_pattern bug related to nested quantifiers | Rustan Leino | 2013-12-16 |
| | | |||
| * | Merge | Rustan Leino | 2013-12-16 |
| |\ | |/ |/| | |||
| * | Fixed bug in never_pattern functionality. In the new design, never_pattern ↵ | Rustan Leino | 2013-12-16 |
| | | | | | | | | does not assemble any nopats from nested quantifiers/lambdas. | ||
* | | regenerated after updating Parser.frame | qadeer | 2013-12-16 |
| | | |||
* | | added syntax for par call and ParCallCmd | qadeer | 2013-12-16 |
| | | |||
* | | Merge | qadeer | 2013-12-14 |
|\ \ | |||
* | | | fixed type checking errors in QED stuff | qadeer | 2013-12-14 |
| |/ |/| | |||
| * | Resolve a concurrency issue (reported by Alex Summers). | wuestholz | 2013-12-12 |
|/ | |||
* | fixes to type checking code | qadeer | 2013-12-11 |
| | |||
* | Updates on YieldTypeCheck | kuruis | 2013-12-11 |
| | |||
* | Remove some (redundant) preconditions to avoid 'ccrewrite' errors. | wuestholz | 2013-12-11 |
| | |||
* | some refactoring of QED stuff | qadeer | 2013-12-10 |
| | |||
* | various updates | qadeer | 2013-12-09 |
| | |||
* | Merge | Ally Donaldson | 2013-12-09 |
|\ | |||
* | | Small change related to CVC4 support. Patch by Pantazis Deligiannis | Ally Donaldson | 2013-12-09 |
| | | |||
| * | Expose certain program transformations in the execution engine to invoke ↵ | wuestholz | 2013-12-09 |
| | | | | | | | | them from Dafny. | ||
| * | debug hastags are inserted to yieldtypechecker | kuruis | 2013-12-08 |
| | | |||
| * | changed the output path for the QED build configuration to the Binaries folder | qadeer | 2013-12-08 |
| | | |||
| * | The back pred files have been eliminated. The small backpred string is now ↵ | qadeer | 2013-12-08 |
| | | | | | | | | directly included in ProverInterface.cs. | ||
| * | removed bitvector analysis from Boogie | qadeer | 2013-12-08 |
|/ | | | | an advanced version has been moved to Corral | ||
* | Proper transition tags added for providing language containtment between two ↵ | kuruis | 2013-12-07 |
| | | | | Autos. | ||
* | fixed a bug regarding invocation of modsetanalysis w.r.t. OG desugaring | qadeer | 2013-12-07 |
| | |||
* | Automata.dll functions are used to create Automata from Graph | kuruis | 2013-12-06 |
| | |||
* | Some bugs on yieldtypechecker graph solved | kuruis | 2013-12-05 |
| | |||
* | Building raw graphs of YieldTypeChecker for building Automata is added | kuruis | 2013-12-04 |
| | |||
* | updated the reference in Concurrency.csproj to Microsoft.Automata.dll (after ↵ | qadeer | 2013-12-02 |
| | | | | Margus supplied the signed dll) | ||
* | forgot to add this file | qadeer | 2013-12-02 |
| | |||
* | Merge | qadeer | 2013-12-02 |
|\ | |||
* | | added the QED build configuration | qadeer | 2013-12-02 |
| | | |||
| * | Patch by Nathan Chong: iterative version of remove empty blocks algorithm. ↵ | Ally Donaldson | 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 | akashlal | 2013-11-29 |
| | |||
* | added some type checking code | qadeer | 2013-11-25 |
| | |||
* | moved some files around | qadeer | 2013-11-22 |
| | |||
* | factored the concurrency checking code into a separate project | qadeer | 2013-11-22 |
| | |||
* | do monomorphic checking | qadeer | 2013-11-22 |
| | |||
* | Fixedpoint VC catch up with recent changes | Ken McMillan | 2013-11-11 |
| | |||
* | Merge duality changes to mainline | Ken McMillan | 2013-11-09 |
|\ | |||
| * | handling timeouts for fixedpoint engines | Ken McMillan | 2013-11-09 |
| | | |||
* | | Merge | Pantazis Deligiannis | 2013-11-07 |
|\ \ | |||
| * | | Fixes to predication. Patch by Jeroen Ketema. | Ally Donaldson | 2013-11-06 |
| | | | |||
| * | | code cleanup | akashlal | 2013-11-02 |
| | | | |||
| * | | AbsHoudini: Support timeout, MakeTop, InlineFunctions | akashlal | 2013-11-02 |
| | | | |||
| * | | ProverInterface: model isn't available on timeout | akashlal | 2013-11-02 |
| | | | |||
| * | | Merge | qadeer | 2013-10-25 |
| |\ \ | |||
| * | | | minor refactoring | qadeer | 2013-10-25 |
| | | | | | | | | | | | | | | | | moved the call to EliminateDeadVariablesAndInline to after the OG sequentialization |