Article

Enhancing Program Verification with Lemmas

Authors:

Huu Hai Nguyen,

Wei-Ngan ChinAuthors Info & Claims

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

Pages 355 - 369

https://doi.org/10.1007/978-3-540-70545-1_34

Published: 07 July 2008 Publication History

Abstract

One promising approach to verifying heap-manipulating programs is based on <em>user-defined</em>inductive predicates in separation logic. This approach can describe data structures with complex invariants and sound reasoning based on unfold/fold. However, an important component towards more expressive program verification is the use of <em>lemmas</em>that can soundly relate predicates beyond their original definitions. This paper outlines a new <em>automatic</em>mechanism for proving and applying <em>user-specified lemmas</em>under separation logic.

References

[1]

Berdine, J., Calcagno, C., O'Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52-68. Springer, Heidelberg (2005)

Digital Library

[2]

Berdine, J., Calcagno, C., O'Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO. LNCS. Springer, Heidelberg (2006)

Digital Library

[3]

Berdine, J., Cook, B., Distefano, D., O'Hearn, P.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386-400. Springer, Heidelberg (2006)

Digital Library

[4]

Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 87-103. Springer, Heidelberg (2007)

Digital Library

[5]

Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: LICS, pp. 51-62 (2007)

Digital Library

[6]

Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247-260 (2008)

Digital Library

[7]

Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ICFP, Tallinn, Estonia (September 2005)

Digital Library

[8]

Distefano, D., O'Hearn, P.W., Yang, H.: A Local Shape Analysis based on Separation Logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 287-302. Springer, Heidelberg (2006)

Digital Library

[9]

Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In: PLDI, Tucson, Arizona, June 2008. ACM Press, New York (2008)

Digital Library

[10]

Gotsman, A., Berdine, J., Cook, B.: Interprocedural Shape Analysis with Separated Heap Abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240-260. Springer, Heidelberg (2006)

Digital Library

[11]

Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp. 266-277 (2007)

Digital Library

[12]

Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI, pp. 256-265 (2007)

Digital Library

[13]

Jia, L., Walker, D.: ILC: A Foundation for Automated Reasoning About Pointer Programs. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 131-145. Springer, Heidelberg (2006)

Digital Library

[14]

Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 124-140. Springer, Heidelberg (2005)

Digital Library

[15]

Marti, N., Affeldt, R., Yonezawa, A.: Formal Verification of the Heap Manager of an Operating system using Separation Logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400-419. Springer, Heidelberg (2006)

Digital Library

[16]

Nguyen, H.H., David, C., Qin, S.C., Chin, W.N.: Automated Verification of Shape and Size Properties via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251-266. Springer, Heidelberg (2007)

Digital Library

[17]

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL--A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

Digital Library

[18]

Owre, S., Rushby, J.M., Shankar, N., Stringer-Calvert, D.W.J.: PVS: An experience report. In: FM-Trends, pp. 338-345 (1998)

Digital Library

[19]

Parkinson, M., Bornat, R., O'Hearn, P.: Modular verification of a non-blocking stack. In: POPL, Nice, France (January 2007)

Digital Library

[20]

Preoteasa, V.: Mechanical verification of recursive procedures manipulating pointers using separation logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 508-523. Springer, Heidelberg (2006)

Digital Library

[21]

Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. CACM 8, 102-114 (1992)

Digital Library

[22]

Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS, Copenhagen, Denmark (July 2002)

Digital Library

[23]

Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 500-504. Springer, Heidelberg (2002)

Digital Library

Cited By

Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Murali APeña LBlanchard ELöding CMadhusudan P(2022)Model-guided synthesis of inductive lemmas for FOL with least fixpointsProceedings of the ACM on Programming Languages10.1145/35633546:OOPSLA2(1873-1902)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563354
Ta QLe TKhoo SChin W(2019)Automated mutual induction proof in separation logicFormal Aspects of Computing10.1007/s00165-018-0471-531:2(207-230)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s00165-018-0471-5
Show More Cited By

Index Terms

Enhancing Program Verification with Lemmas
1. Software and its engineering
  1. Software creation and management
    1. Software development process management
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Cyclic proofs of program termination in separation logic
POPL '08

We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system.Judgements in this system express (guaranteed) termination of the program when ...
Cyclic proofs of program termination in separation logic
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system.Judgements in this system express (guaranteed) termination of the program when ...
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

July 2008

555 pages

ISBN:9783540705437

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 July 2008

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Murali APeña LBlanchard ELöding CMadhusudan P(2022)Model-guided synthesis of inductive lemmas for FOL with least fixpointsProceedings of the ACM on Programming Languages10.1145/35633546:OOPSLA2(1873-1902)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563354
Ta QLe TKhoo SChin W(2019)Automated mutual induction proof in separation logicFormal Aspects of Computing10.1007/s00165-018-0471-531:2(207-230)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s00165-018-0471-5
Krishna SShasha DWies T(2017)Go with the flow: compositional abstractions for concurrent data structuresProceedings of the ACM on Programming Languages10.1145/31581252:POPL(1-31)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158125
Löding CMadhusudan PPeña L(2017)Foundations for natural proofs and quantifier instantiationProceedings of the ACM on Programming Languages10.1145/31580982:POPL(1-30)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158098
Ta QLe TKhoo SChin W(2017)Automated lemma synthesis in symbolic-heap separation logicProceedings of the ACM on Programming Languages10.1145/31580972:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158097
(2016)Completeness for recursive procedures in separation logicTheoretical Computer Science10.1016/j.tcs.2016.04.004631:C(73-96)Online publication date: 6-Jun-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.04.004
Chu DJaffar JTrinh M(2015)Automatic induction proofs of data-structures in imperative programsACM SIGPLAN Notices10.1145/2813885.273798450:6(457-466)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737984
Chu DJaffar JTrinh MGrove DBlackburn S(2015)Automatic induction proofs of data-structures in imperative programsProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737984(457-466)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737984
Lee WPark S(2014)A proof system for separation logic with magic wandACM SIGPLAN Notices10.1145/2578855.253587149:1(477-490)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535871
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents