Establishing properties of binary programs by proof is a desirable goal when the properties of interest are crucial, such as those that arise in safety- and security-critical applications. Practical development of proofs for binary programs requires a substantial infrastructure to disassemble the program, define the machine semantics, and actually undertake the required proofs. At the center of these infrastructure requirements is the need to document semantics in a formal language. In this paper we present a work-in-progress proof infrastructure for binary programs based on AdaCore and Altran’s integrated development and verification environment, SPARKPro. We illustrate the infrastructure with proof of a security property.
CITATION STYLE
Hocking, A. B., Rodes, B. D., Knight, J. C., Davidson, J. W., & Coleman, C. L. (2016). A proof infrastructure for binary programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9690, pp. 337–343). Springer Verlag. https://doi.org/10.1007/978-3-319-40648-0_25
Mendeley helps you to discover research relevant for your work.