Abstract
Deductive program verification is a powerful tool to gain confidence in the correctness of software. However, its application to real programs faces a major hurdle: Each programming language requires development of dedicated verification tool support. In this work, we aim to advance deductive software verification to arbitrary programming languages. We developed a tool that derives algebraic specifications for the deductive proof assistant KIV from the syntax and operational semantics of a programming language specified in the \(\mathbb {K}\) semantic framework. We adapt and implement the generic One-Path Reachability calculus and provide instant tool support for deductive proofs. Through a sophisticated automation approach, we drastically reduce the manual proof steps.
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
Similar content being viewed by others
Notes
References
Bogdănaş, D., Roşu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL 2015), pp. 445–456. ACM, January 2015
Chen, X., Roşu, G.: A language-independent program verification framework. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 92–102. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_7
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All about Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, Berlin, Heidelberg (2007)
Şerbănuţă, T.F., Roşu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 104–122. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_8
Ştefănescu, A., Park, D., Yuwen, S., Li, Y., Roşu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), pp. 74–91. ACM, November 2016
Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transfer 17(6), 677–694 (2015)
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Haneberg, D., et al.: The User Interface of the KIV Verification System – A System Description. Electronic Notes in Theoretical Computer Science UITP special issue (2006)
Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of C. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 336–345. ACM, June 2015
Leino, K.R.M.: This is Boogie 2, June 2008. https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/
Meredith, P., Rosu, M.H.G.: An executable rewriting logic semantics of K-Scheme. In: Workshop on Scheme and Functional Programming, vol. 1, p. 10 (2007)
Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_2
Park, D., Ştefănescu, A., Roşu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 346–356. ACM, June 2015
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel ,W., Schmitt, P.H. (eds.) Automated Deduction – A Basis for Applications. Applied Logic Series, vol 9, pp. 13–39. Springer, Dordrecht (1998)
Roşu, G., Ştefănescu, A., Ciobâcă, Ş., Moore, B.M.: One-path reachability logic. In: Proceedings of the 28th Symposium on Logic in Computer Science (LICS 2013), pp. 358–367. IEEE, June 2013
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Programm. 79(6), 397–434 (2010)
Rosu, G., Stefanescu, A., Ciobaca, S., Moore, B.: Reachability Logic. Technical report July 2012. https://www.ideals.illinois.edu/handle/2142/32952
Şerbănuţă, T., Ştefănescu, G., Roşu, G.: Defining and executing P systems with structured data in K. In: Corne, D.W., Frisco, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 374–393. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-540-95885-7_26
Ştefănescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425–440. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08918-8_29
The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2004). http://coq.inria.fr, version 8.0
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Klumpp, D., Lenzen, P. (2021). \(\mathbb {K}\) and KIV: Towards Deductive Verification for Arbitrary Programming Languages. In: Roggenbach, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2020. Lecture Notes in Computer Science(), vol 12669. Springer, Cham. https://doi.org/10.1007/978-3-030-73785-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-73785-6_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-73784-9
Online ISBN: 978-3-030-73785-6
eBook Packages: Computer ScienceComputer Science (R0)