Amy Patricia Felty - Berkeley Heights NJ Douglas J. Howe - Berkeley Heights NJ Abhik Roychoudhury - Stony Brook NY
Assignee:
Lucent Technologies Inc. - Murray Hill NJ
International Classification:
G06F 944
US Classification:
717 2, 717 4, 717 7, 703 2
Abstract:
A method of synthesizing an algorithm for transforming a program from a first form to a second form includes first formalizing a language associated with the program to be transformed in accordance with a theorem proving system. Then, a proof is built in accordance with the theorem proving system based on a theorem asserting a representability associated with the program, the representability being expressed as inductive predicates over semantic domains. The method then extracts the algorithm based on the proof. The algorithm is capable of transforming the program from the first form to the second form. In one embodiment, the algorithm is a correctness verified abstraction algorithm and the theorem proving system is Nuprl.
Type Annotation Method For Use In Verification Tools
A type annotation technique such that expressions are assigned and annotated with types in such a way that types can be efficiently maintained during inference without new syntactic restrictions being placed on the expressions or underlying logic within the verification system. More particularly, in accordance with the technique, expressions, i. e. terms, are annotated using a particular labeling scheme such that, during verification, if an expression is annotated the verification may proceed without any additional type inference or type checking with regard to that expression.