微信服务号

微信订阅号

2025-4-13- 3
Home > Archive>Volume 28, Issue 4, 2017 >786-803. DOI:10.13328/j.cnki.jos.005195
PDF HTML XML Export Cite reminder
Verification of Concrete Programs with Respect to Abstract Programs
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61632015, 61561146394); National Basic Research Program of China (973) (2016YFB1000802)

  • Article
    • | |
  • Metrics
    • |
  • Reference [30]
    • |
  • Related
    • |
  • Cited by [1]
    • | |
  • Comments
    Abstract:

    This paper presents an approach to prove that a concrete program correctly implements its corresponding abstract program. Here, an abstract program uses some abstract data types such as set, list and map, and abstract operations upon those data types. A concrete program uses the types in the C-like language. The approach presented in the paper requires to specify correspondences between the abstract program and the concrete program, including correspondences between program points and correspondences between variables. Based on the correspondences, the verification task can be divided into small subtasks that can be easily and mostly automatically verified.

    Reference
    [1] Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F. Verifast:A powerful, sound, predictable, fast verifier for C and Java. In:Bobaru M, ed. NASA Formal Methods. Springer-Verlag, 2011. 41-55.[doi:10.1007/978-3-642-20398-5_4]
    [2] Chlipala A. Mostly-Automated verification of low-level programs in computational separation logic. In:Hall M, ed. Proc. of the Programming Language Design and Implementation. ACM Press, 2011. 234-245.[doi:10.1145/1993498.1993526]
    [3] Pek E, Qiu X, Madhusudan P. Natural proofs for data structure manipulation in C using separation logic. In:Proc. of the 35th ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2014,49(6):440-451.[doi:10.1145/2594291.2594325]
    [4] Distefano D, O'hearn PW, Yang H. A local shape analysis based on separation logic. In:Hermanns H, ed. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Vienna:Springer-Verlag, 2006. 287-302.[doi:10.1007/11691372_19]
    [5] Lev-Ami T, Immerman N, Reps T, Sagiv M, Srivastava S, Yorsh G. Simulating reachability using first-order logic with applications to verification of linked data structures. In:Nieuwenhuis R, ed. Proc. of the Automated Deduction (CADE-20). Tallinn:Springer-Verlag, 2005. 99-115.[doi:10.1007/11532231_8]
    [6] Lev-Ami T, Sagiv M. TVLA:A system for implementing static analyses. In:Palsberg J, ed. Proc. of the Static Analysis. Santa Barbara:Springer-Verlag, 2000. 280-301.[doi:10.1007/978-3-540-45099-3_15]
    [7] Balaban I, Pnueli A, Zuck LD. Shape analysis by predicate abstraction. In:Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. Paris:Springer-Verlag, 2005. 164-180.[doi:10.1007/978-3-540-30579-8_12]
    [8] Chatterjee S, Lahiri SK, Qadeer S, Rakamarić Z. A reachability predicate for analyzing low-level software. In:Grumberg O, ed. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Braga:Springer-Verlag, 2007. 19-33.[doi:10. 1007/978-3-540-71209-1_4]
    [9] Lahiri SK, Qadeer S. Verifying properties of well-founded linked lists. ACM SIGPLAN Notices, 2006,41(1):115-126.[doi:10. 1145/1111320.1111048]
    [10] Lahiri S, Qadeer S. Back to the future:Revisiting precise program verification using SMT solvers. ACM SIGPLAN Notices, 2008, 43(1):171-182.[doi:10.1145/1328897.1328461]
    [11] Cao J, Fu M, Feng X. Practical tactics for verifying C programs in Coq. In:Leroy X, ed. Proc. of the 2015 Conf. on Certified Programs and Proofs. Mumbai:ACM Press, 2015. 97-108.[doi:10.1145/2676724.2693162]
    [12] Gries D, Prins J. A new notion of encapsulation. ACM SIGPLAN Notices, 1985,20(7):131-139.[doi:10.1145/17919.806834]
    [13] Zhao JH, Li XD. Scope logic:An extension to Hoare logic for pointers and recursive data structures. In:Liu ZM, ed. Proc. of the Theoretical Aspects of Computing (CICTAC 2013). Shanghai:Springer-Verlag, 2013. 409-426.[doi:10.1007/978-3-642-39718-9_24]
    [14] Back RJR. A calculus of refinements for program derivations. Acta Informatica, 1988,25(6):593-624.[doi:10.1007/BF00291051]
    [15] Back RJR. Correctness preserving program refinements:Proof theory and applications. MC Tracts, 1980,131:1-118.
    [16] Morgan C, Robinson K. Specification statements and refinement. IBM Journal of Research and Development, 1987,31(5):546-555.[doi:10.1147/rd.315.0546]
    [17] Morris JM. A theoretical basis for stepwise refinement and the programming calculus. In:Sintzoff M, ed. Proc. of the Science of Computer programming. Amsterdam:Elsevier, 1987. 287-306.[doi:10.1016/0167-6423(87)90011-6]
    [18] Morgan C. The specification statement. ACM Trans. on Programming Languages and Systems (TOPLAS), 1988,10(3):403-419.[doi:10.1145/44501.44503]
    [19] Gardiner PH, Morgan CC. Data refinement of predicate transformers. Theoretical Computer Science, 1991,87(1):143-162.[doi:10. 1016/0304-3975(91)90029-2]
    [20] Morgan C. Auxiliary variables in data refinement. Information Processing Letters, 1988,29(6):293-296.[doi:10.1016/0020-0190(88)90227-X]
    [21] Morris JM. Laws of data refinement. Acta Informatica, 1989,26(4):287-308.[doi:10.1007/BF00276019]
    [22] Morgan C, Gardiner PH. Data refinement by calculation. Acta Informatica, 1990,27(6):481-503.[doi:10.1007/BF00277386]
    [23] Chen W, Udding JT. Towards a calculus of data refinement. In:van de Snepscheut JLA, ed. Proc. of the Mathematics of Program Construction. London:Springer-Verlag, 1989. 197-218.[doi:10.1007/3-540-51305-1_11]
    [24] Leuschel M, Butler M. Automatic refinement checking for B. In:Lau KK, ed. Proc. of the Formal Methods and Software Engineering. Manchester:Springer-Verlag, 2005. 345-359.[doi:10.1007/11576280_24]
    [25] Burdy L, Meynadier JM. Automatic refinement. In:Proc. of the BUGM at FM. 1999. 99. https://link.springer.com/book/10.1007%2F3-540-48118-4
    [26] Cohen E, Dahlweid M, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S. VCC:A practical system for verifying concurrent C. In:Berghofer S, ed. Proc. of the Theorem Proving in Higher Order Logics. Munich:Springer-Verlag, 2009. 23-42.[doi:10.1007/978-3-642-03359-9_2]
    [27] Leino KR. Dafny:An automatic program verifier for functional correctness. In:Clarke EM, ed. Proc. of the Logic for Programming, Artificial Intelligence, and Reasoning. Dakar:Springer-Verlag, 2010. 348-370.[doi:10.1007/978-3-642-17511-4_20]
    [28] Condit J, Hackett B, Lahiri SK, Qadeer S. Unifying type checking and property checking for low-level code. In:Shao Z, ed. Proc. of the Principles of Programming Languages. Savannah:ACM Press, 2009. 302-314.[doi:10.1145/1594834.1480921]
    [29] Distefano D, Parkinson JMJ. jStar:Towards practical verification for Java. ACM Sigplan Notices, 2008,43(10):213-226.[doi:10. 1145/1449955.1449782]
    [30] Berdine J, Calcagno C, O'hearn PW. Smallfoot:Modular automatic assertion checking with separation logic. In:de Boer FS, ed. Proc. of the Formal Methods for Components and Objects. Amsterdam:Springer-Verlag, 2006. 115-137.[doi:10.1007/11804192_6]
    Related
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李彬,汤震浩,翟娟,赵建华.通过抽象程序证明复杂具体程序.软件学报,2017,28(4):786-803

Copy
Share
Article Metrics
  • Abstract:4056
  • PDF: 6015
  • HTML: 2947
  • Cited by: 0
History
  • Received:June 20,2016
  • Revised:November 26,2016
  • Online: January 24,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034785Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063