Abstract
Relational program verification refers to the verification of relational properties, which relate different programs, different versions of the same program, or the same program for different inputs. Recently, there is a growing interest in relational properties. One of the main reasons for this trend is that relational properties avoid the bottleneck of having to write complex requirement specifications. Instead, the programs that are compared serve as specification of each other. In this chapter, we give an overview of current trends in relational program verification. We describe the main scenarios where relational program verification is employed to ensure dependability of systems, including regression verification and proving non-interference properties. And we discuss recent trends in how to use deductive verification to prove relational properties.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Paul Ammann and Jeff Offutt. Introduction to software testing. Cambridge University Press, 2008. ISBN: 978-0-521-88038-1.
Torben Amtoft and Anindya Banerjee. “Information Flow Analysis in Logical Form”. In: Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26–28, 2004, Proceedings. Ed. by Roberto Giacobazzi. Vol. 3148. Lecture Notes in Computer Science. Springer, 2004, pp. 100–115. ISBN: 3-540-22791-1. https://doi.org/10.1007/978-3-540-27864-1_10.
Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. “Relational Logic with Framing and Hypotheses”. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13–15, 2016, Chennai, India. Ed. by Akash Lal et al. Vol. 65. LIPIcs. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2016, 11:1–11:16. ISBN: 978-3-95977-027-9. https://doi.org/10.4230/LIPIcs.FSTTCS.2016.11.
Gilles Barthe, Juan Manuel Crespo, and César Kunz. “Relational Verification Using Product Programs”. In: FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20–24, 2011. Proceedings. Ed. by Michael J. Butler and Wolfram Schulte. Vol. 6664. Lecture Notes in Computer Science. Springer, 2011, pp. 200–214. ISBN: 978-3-642-21436-3. https://doi.org/10.1007/978-3-642-21437-0_17.
Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. “Secure Information Flow by Self-Composition”. In: 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28–30 June 2004, Pacific Grove, CA, USA. IEEE Computer Society, 2004, pp. 100–114. ISBN: 0-7695-2169-X. https://doi.org/10.1109/CSFW.2004.17.
Bernhard Beckert, Vladimir Klebanov, and Mattias Ulbrich. “Regression verification for Java using a secure information flow calculus”. In: Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015, Prague, Czech Republic, July 7, 2015. Ed. by Rosemary Monahan. ACM, 2015, 6:1–6:6. ISBN: 978-1-4503-3656-7. https://doi.org/10.1145/2786536.2786544.
Bernhard Beckert et al. “Automated Verification for Functional and Relational Properties of Voting Rules”. In: Sixth International Workshop on Computational Social Choice (COMSOC 2016). June 2016.
Nick Benton. “Simple relational correctness proofs for static analyses and program transformations”. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14–16, 2004. Ed. by Neil D. Jones and Xavier Leroy. ACM, 2004, pp. 14–25. ISBN: 1-58113-729-X. https://doi.org/10.1145/964001.964003.
Marco Cadoli and Toni Mancini. “Using a Theorem Prover for Reasoning on Constraint Problems”. In: AI* IA 2005: Advances in Artificial Intelligence. Springer, 2005.
Michael R. Clarkson, Stephen Chong, and Andrew C. Myers. “Civitas: Toward a Secure Voting System”. In: 2008 IEEE Symposium on Security and Privacy (S&P 2008), 18–21 May 2008, Oakland, California, USA. IEEE Computer Society, 2008, pp. 354–368. ISBN: 978-0-7695-3168-7. https://doi.org/10.1109/SP.2008.32.
Ádám Darvas, Reiner Hähnle, and David Sands. “A Theorem Proving Approach to Analysis of Secure Information Flow”. In: Security in Pervasive Computing Second International Conference, SPC 2005, Boppard, Germany, April 6–8, 2005, Proceedings. Ed. by Dieter Hutter and Markus Ullmann. Vol. 3450. Lecture Notes in Computer Science. Springer, 2005, pp. 193–209. ISBN: 3–540-25521-4. https://doi.org/10.1007/978-3-540-32004-3_20.
Marco Eilers, Peter Müller, and Samuel Hitz. “Modular Product Programs”. In: Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings. Ed. by Amal Ahmed. Vol. 10801. Lecture Notes in Computer Science. Springer, 2018, pp. 502–529. ISBN: 978-3-319-89883-4. https://doi.org/10.1007/978-3-319-89884-1_18.
Dima Elenbogen, Shmuel Katz, and Ofer Strichman. “Proving mutual termination”. In: Formal Methods in System Design 47.2 (2015), pp. 204–229. https://doi.org/10.1007/s10703-015-0234-3.
Dennis Felsing et al. “Automating regression verification”. In: ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15–19, 2014. Ed. by Ivica Crnkovic, Marsha Chechik, and Paul Grünbacher. ACM, 2014, pp. 349–360. ISBN: 978-1-4503-3013-8. https://doi.org/10.1145/2642937.2642987.
Benny Godlin and Ofer Strichman. “Regression verification: proving the equivalence of similar programs”. In: Softw. Test., Verif. Reliab. 23.3 (2013), pp. 241–258. https://doi.org/10.1002/stvr.1472.
Christian Hammer and Gregor Snelting. “Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs”. In: Int. J. Inf. Sec. 8.6 (2009), pp. 399–422. https://doi.org/10.1007/s10207-009-0086-1.
David Harel, Dexter Kozen, and Jerzy Tiuryn. “Dynamic logic”. In: SIGACT News 32.1 (2001), pp. 66–69. https://doi.org/10.1145/568438.568456.
Chris Hawblitzel et al. “Towards Modularly Comparing Programs Using Automated Theorem Provers”. In: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Ed. by Maria Paola Bonacina. Vol. 7898. Lecture Notes in Computer Science. Springer, 2013, pp. 282–299. ISBN: 978-3-642-38573-5. https://doi.org/10.1007/978-3-642-38574-2_20.
Rajeev Joshi and K. Rustan M. Leino. “A semantic approach to secure information flow”. In: Sci. Comput. Program. 37.1-3 (2000), pp. 113–138. https://doi.org/10.1016/S0167-6423(99)00024-6.
Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich. “Relational Program Reasoning Using Compiler IR - Combining Static Verification and Dynamic Analysis”. In: J Autom. Reasoning 60.3 (2018), pp. 337–363. https://doi.org/10.1007/s10817-017-9433-5.
Vladimir Klebanov. “Precise quantitative information flow analysis - a symbolic approach”. In: Theor. Comput. Sci. 538 (2014), pp. 124–139. https://doi.org/10.1016/j.tcs.2014.04.022.
Nuno P. Lopes et al. “Provably correct peephole optimizations with alive”. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15–17, 2015. Ed. by David Grove and Steve Blackburn. ACM, 2015, pp. 22–32. ISBN: 978-1-4503-3468-6. https://doi.org/10.1145/2737924.2737965.
Toni Mancini and Marco Cadoli. “Detecting and Breaking Symmetries by Reasoning on Problem Specifications”. In: Abstraction, Reformulation and Approximation. Springer, 2005.
Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. “Game Semantic Analysis of Equivalence in IMJ”. In: Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12–15, 2015, Proceedings. Ed. by Bernd Finkbeiner, Geguang Pu, and Lijun Zhang. Vol. 9364. Lecture Notes in Computer Science. Springer, 2015, pp. 411–428. ISBN: 978-3-319-24952-0. https://doi.org/10.1007/978-3-319-24953-7_30.
Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak. “Classifying and Solving Horn Clauses for Verification”. In: Verified Software: Theories, Tools, Experiments 5th International Conference VSTTE 2013, Menlo Park, CA, USA, May 17–19, 2013, Revised Selected Papers Ed. by Ernie Cohen and Andrey Rybalchenko. Vol. 8164. Lecture Notes in Computer Science. Springer, 2013, pp. 1–21. ISBN: 978-3-642-54107-0. https://doi.org/10.1007/9783642541087_1
Andrei Sabelfeld and Andrew C. Myers. “Language-based information-flow security”. In: IEEE Journal on Selected Areas in Communications 21.1 (2003), pp. 5–19. https://doi.org/10.1109/JSAC.2002.806121.
Tachio Terauchi and Alexander Aiken. “Secure Information Flow as a Safety Problem”. In: Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7–9, 2005, Proceedings. Ed. by Chris Hankin and Igor Siveroni. Vol. 3672. Lecture Notes in Computer Science. Springer, 2005, pp. 352–367. ISBN: 3-540-28584-9. https://doi.org/10.1007/11547662_24.
Mattias Ulbrich. “Dynamic Logic for an Intermediate Language: Verification, Interaction and Refinement”. PhD thesis. Karlsruhe Institute of Technology, 2013.
Yannick Welsch and Arnd Poetzsch-Heffter. “A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries”. In: Sci. Comput. Program. 92 (2014), pp. 129–161. https://doi.org/10.1016/j.scico.2013.10.002.
Yannick Welsch and Arnd Poetzsch-Heffter. “Full Abstraction at Package Boundaries of Object-Oriented Languages”. In: Formal Methods, Foundations and Applications - 14th Brazilian Symposium, SBMF 2011, São Paulo, Brazil, September 26–30, 2011, Revised Selected Papers. Ed. by Adenilso da Silva Simão and Carroll Morgan. Vol. 7021. Lecture Notes in Computer Science. Springer, 2011, pp. 28–43. ISBN: 978-3-642-25031-6. https://doi.org/10.1007/978-3-642-25032-3_3.
Hongseok Yang. “Relational separation logic”. In: Theor. Comput. Sci. 375.1-3 (2007), pp. 308–334. https://doi.org/10.1016/j.tcs.2006.12.036.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Beckert, B., Ulbrich, M. (2018). Trends in Relational Program Verification. In: Müller, P., Schaefer, I. (eds) Principled Software Development. Springer, Cham. https://doi.org/10.1007/978-3-319-98047-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-98047-8_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98046-1
Online ISBN: 978-3-319-98047-8
eBook Packages: Computer ScienceComputer Science (R0)