Abstract
For many safety-critical systems besides functional correctness, termination properties are especially important. Ideally, such properties are not only established for high-level representations of a system, but also for low-level representations.
In this paper, we therefore present a compositional semantics and a related proof calculus for possibly non-deterministic low-level languages. The calculus facilitates total correctness proofs about program representations given in a low-level language. We cope with the complexity inherent to such proofs by mechanizing the entire theory using the theorem prover Isabelle/HOL and exploiting the provers mechanisms for constructing well-founded relations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Affeldt, R., Nowak, D., Yamada, K.: Certifying assembly with formal security proofs: The case of bbs, vol. 77, pp. 1058–1074. Elsevier North-Holland, Inc., Amsterdam (2012)
Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report 75, Dept. of Computer Science,University of Toronto (1975)
Jensen, J.B., Benton, N., Kennedy, A.: High-level separation logic for low-level code. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 301–314. ACM, New York (2013)
Jones, C.B.: Specification and Design of (Parallel) Programs. In: IFIP Congress, pp. 321–332 (1983)
Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568–582. Springer, Heidelberg (2007)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 103–119. Springer, Heidelberg (2002)
Olderog, E.-R.: On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science 24(3), 337–347 (1983)
Saabas, A., Uustalu, T.: A compositional natural semantics and hoare logic for low-level languages. Electron. Notes Theor. Comput. Sci. 156(1), 151–168 (2006)
Schreiber, T.: Auxiliary variables and recursive procedures. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 697–711. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bartels, B., Jähnig, N. (2014). Mechanized, Compositional Verification of Low-Level Code. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)