Paper Info
Title
Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses
Abstract
This paper describes our experience using the interactive theorem prover Athena for proving the correctness of abstract interpretation-based dataflow analyses. For each analysis, our methodology requires the analysis designer to formally specify the property lattice, the transfer functions, and the desired modeling relation between the concrete program states and the results computed by the analysis. The goal of the correctness proof is to prove that the desired modeling relation holds. The proof allows the analysis clients to rely on the modeling relation for their own correctness. To reduce the complexity of the proofs, we separate the proof of each dataflow analysis into two parts: a generic part, proven once, independent of any specific analysis; and several analysis-specific conditions proven in Athena.
Year
DOI
Venue
2005
10.1016/j.entcs.2005.02.043
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
dataflow analysis,analysis designer,intra-procedural dataflow analyses,interactive theorem proving,modeling relation,analysis client,correctness proof,athena,analysis-specific condition,correctness proofs,specific analysis,abstract interpretation-based dataflow analysis,own correctness,concrete program state,machine-checkable correctness proofs,interactive,theorem prover,transfer function
Discrete mathematics,Programming language,Correctness proofs,Abstract interpretation,Computer science,Correctness,Theoretical computer science,Dataflow,Mathematical proof,Transfer function,Proof assistant
Journal
Volume
Issue
ISSN
141
2
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
4
0.53
16
Authors
2
Name
Order
Citations
PageRank
Alexandru Sălcianu140.53
Konstantine Arkoudas218619.63