Design of critical embedded systems demands for guarantees on the reliability of the implementation/compilation of a specification. In general, this guarantee takes either the form...
Abstract. Following the translation validation approach to highassurance compilation, we describe a new algorithm for validating a posteriori the results of a run of register alloc...