Abstract
A simple semantic model for the NRB logic of program verification is provided here, and the logic is shown to be sound and complete with respect to it. That provides guarantees in support of the logic’s use in the automated verification of large imperative code bases, such as the Linux kernel source. ‘Soundness’ implies that no breaches of safety conditions are missed, and ‘completeness’ implies that symbolic reasoning is as powerful as model-checking here.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
American National Standards Institute. American national standard for information systems - programming language C, ANSI X3.159-1989 (1989)
Apt, K.R.: Ten years of Hoare’s logic: a survey: part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)
Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010)
Breuer, P.T., Pickin, S.: Checking for deadlock, double-free and other abuses in the Linux kernel source code. In: Alexandrov, V.N., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds.) ICCS 2006. LNCS, vol. 3994, pp. 765–772. Springer, Heidelberg (2006)
Breuer, P.T., Valls, M.: Static deadlock detection in the Linux kernel. In: Llamosí, A., Strohmeier, A. (eds.) Ada-Europe 2004. LNCS, vol. 3063, pp. 52–64. Springer, Heidelberg (2004)
Breuer, P.T., Pickin, S.: Symbolic approximation: an approach to verification in the large. Innovations Syst. Softw. Eng. 2(3), 147–163 (2006)
Breuer, P.T., Pickin, S.: Verification in the large via symbolic approximation. In: Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), pp. 408–415. IEEE (2006)
Breuer, P.T., Pickin, S.: Open source verification in an anonymous volunteer network. Sci. Comput. Program. (2013). doi: 10.1016/j.scico.2013.08.010
Breuer, P.T., Pickin, S., Petrie, M.L.: Detecting deadlock, double-free and other abuses in a million lines of Linux kernel source. In: Proceedings of the 30th Annual Software Engineering Workshop 2006 (SEW’06), pp. 223–233. IEEE/NASA (2006)
Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Syst. (TOPLAS) 8(2), 244–253 (1986)
Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proceedings of the 4th Symposium on Operating System Design and Implementation (OSDI 2000), pp. 1–16, October 2000
International Standards Organisation. ISO/IEC 9899-1999, programming languages - C (1999)
Acknowledgments
Simon Pickin’s research has been partially supported by the Spanish MEC project ESTuDIo (TIN2012-36812-C02-01).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Breuer, P.T., Pickin, S.J. (2014). Soundness and Completeness of the NRB Verification Logic. In: Counsell, S., Núñez, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science(), vol 8368. Springer, Cham. https://doi.org/10.1007/978-3-319-05032-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-05032-4_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05031-7
Online ISBN: 978-3-319-05032-4
eBook Packages: Computer ScienceComputer Science (R0)