Paper Info
Title
A web-integrated verifying compiler for RESOLVE: a research perspective
Abstract
RESOLVE is an integrated language that combines imperative programming and mathematical specifications for full functional verification of component-based programs. From a researcher's perspective, this paper summarizes the elements of RESOLVE's web IDE that includes a verifying compiler. We use a variety of in-language examples to demonstrate the following: Extensible mathematical units that contain definitions and results, higher-order specifications of generic components that use those mathematical units, alternative implementations of specifications, and automated generation of verification conditions and proofs for implementation correctness. While verification and research are the focus of this paper, it's worth mentioning that the compiler translates RESOLVE code to Java (or C) for execution, and has been utilized in a variety of computer science classes at multiple institutions over the last five years.
Year
DOI
Venue
2014
10.1145/2590748.2590760
ISEC
Keywords
Field
DocType
verifying compiler,verification,automation,components,specification,languages,reliability,formal methods,metrics
Functional verification,Programming language,Functional compiler,Computer science,Correctness,Compiler correctness,Imperative programming,Theoretical computer science,Compiler,Compiler construction,Formal methods
Conference
Citations 
PageRank 
References 
3
0.43
11
Authors
4
Name
Order
Citations
PageRank
Daniel Welch151.84
Charles T. Cook2202.74
Yu-Shan Sun3115.93
Murali Sitaraman427040.99