Bitte wählen Sie ihr Lieferland und ihre Kundengruppe
This project laid the foundation for a novel methodology for correcting erroneous program executions using specifications at run-time. The basis of the methodology is a view of the specification as a non-deterministic implementation, which may permit a high degree of non-determinism. The key insight is to use likely correct actions by an otherwise erroneous execution to prune the non-determinism in the specification, thereby transmuting the specification to an implementation at run-time and reducing the performance overhead. A suite of techniques and tools were designed, developed, optimized and rigorously evaluated in this project. It leveraged the Alloy specification language and its SAT-based tool-set as an enabling technology for specification- based analysis. The ideas, techniques, tools, and evaluation results from this project contributed in part to archival publications, Masters theses, and PhD dissertations.