Record Details

A PVS based framework for validating compiler optimizations

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title A PVS based framework for validating compiler optimizations
 
Creator KANADE, A
SANYAL, A
KHEDKER, U
 
Description An optimization can be specified as sequential compositions of predefined transformation. primitives. For each primitive, we can. define soundness conditions which guarantee that the transformation is semantics preserving. An optimization of a program preserves semantics, if all applications of the primitives in. the optimization satisfy their respective soundness conditions on the versions of the input program on which the), are applied. This scheme does not directly check semantic equivalence of the input and the optimized programs and is therefore amenable to automation. Automating this scheme however requires a trusted framework for simulating transformation primitives and checking their soundness conditions. In this paper, we present the design of such a framework based on PVS. We have used it for specifying and validating several optimizations viz. common subexpression elimination, optimal code placement, lazy code motion, loop invariant code motion, full and partial dead code elimination, etc.
 
Publisher IEEE COMPUTER SOC
 
Date 2011-10-28T01:13:07Z
2011-12-15T09:12:51Z
2011-10-28T01:13:07Z
2011-12-15T09:12:51Z
2006
 
Type Proceedings Paper
 
Identifier SEFM 2006: FOURTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS,108-117
0-7695-2678-0
1551-0255
http://dspace.library.iitb.ac.in/xmlui/handle/10054/16469
http://hdl.handle.net/100/2944
 
Source 4th IEEE International Conference on Software Engineering and Formal Methods,Pune, INDIA,SEP 11-15, 2006
 
Language English