Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 6 of 6 for “"Loop invariant"”.
-
A component-based approach to proving the correctness of the Schorr-Waite algorithm
… pre- and post-conditions, and a complex loop invariant. Additional operations for the Resolve pointer component are introduced that preserve the accessibility of a system. These operations are used in the implementation of the algorithm. They simplify the proof of correctness and make the …
-
Testing in learning conjunctive invariants
We show a new approach in learning conjunctive invariants using dynamic testing of the program. Coming up with correct set of loop invariant is the most challenging part of any verification methods. Although new methods tend to generate a large number of possible invariants hoping this set contains …
-
How should compilers represent fork-join parallelism?
… optimizations for serial code -- including loop-invariant-code motion, commonsubexpression elimination, and tail-recursion elimination -- to work with parallel control constructs such as spawning and parallel loops. Tapir also supports parallel optimizations such as loop scheduling. This …
-
Control Flow Merging: A Compiler Transformation to Mitigate Branch Misprediction by Branch Elimination
… and simple predication, are effective only for loop-invariant conditions or small side-effect-free branches. This work introduces Control Flow Merging (CFM), a compiler transformation that eliminates branches by converting control dependencies into data dependencies. CFM systematically replaces …
-
Software and architecture support for the bulk multicore
… compiler optimizations using speculation. Loop Invariant Code Motion, a widely used traditional compiler pass, is run as an example client pass to test the potential of the new alias analysis.
-
Techniques for Foundational End-to-End Verification of Systems Stacks
… feature is that instead of stating lengthy loop invariants, the user only needs to give the diff between the symbolic state before the loop and the desired loop invariant, resulting in shorter and more maintainable annotations. Finally, in order to make Live Verification practical, a number …