Higher-Order Strategic Programming: A Road to Software Assurance

V.L. Winter, S. Roach, and F. Fraij (USA)


program transformation, higher-order rules, distributed data problem, Java class loader, Sandia Secure Processor


Program transformation through the repeated application of simple rewrite rules is conducive to formal verification. In practice, program transformation oftentimes requires data to be moved throughout the program structure. This ar ticle explores the use of higher-order rewrite rules as the mechanism for accomplishing such data movement. The effectiveness of higher-order rewrite rules is demonstrated by showing how they can be used to perform field distri bution within a Java class loader. An approach to formal verification of a higher-order strategic implementation of a class loader is also briefly discussed.

Important Links:

Go Back