×
Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon

Unifying separation logic and region logic to allow interoperability. (English) Zbl 1398.68091

Formal Asp. Comput. 30, No. 3-4, 381-441 (2018).

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68P05 Data structures

Keywords:

separation logic; fine-grained region logic; framing; shared mutable data; formal specification; formal verification; Hoare logic; unified fine-grained region logic (UFRL)

Software:

Boogie; JML; Dafny; z3; Spec#; Smallfoot; GitHub; CVC4; VeriFast
Cite Review PDF
Full Text: DOI

References:

[1] Barnett, M; Chang, B-YE; DeLine, R; Jacobs, B; Leino, KRM, Boogie: a modular reusable verifier for object-oriented programs, No. 4111, 364-387, (2006), New York, NY
[2] Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C (2011) Cvc4. In: Proceedings of the 23rd international conference on computer aided verification, CAV’11. Springer, Berlin, pp 171-177
[3] Berdine, J., Calcagno, C., OHearn PW, : A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004: foundations of software technology and theoretical computer science. Lecture Notes in Computer Science, vol. 3328, pp. 97-109. Springer, Berlin (2004) · Zbl 1117.03337
[4] Berdine J, Calcagno C, O’Hearn PW (2006) Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of the 4th international conference on formal methods for components and objects, FMCO’05. Springer, Berlin, pp 115-137
[5] Berdine J, Calcagno C, O’Hearn PW, Mary Q (2005) Symbolic execution with separation logic. In: In APLAS. Springer, pp 52-68 · Zbl 1159.68363
[6] Bao Y, Ernst G (2016) A KIV project for defining semantics for intuitionistic separation logic. http://www.eecs.ucf.edu/ ybao/project/sl-semantics/index.xml
[7] Bao Y, Ernst G (2016) A KIV project for proving encoding supported separation logic into unified fine-grained region logic. http://www.eecs.ucf.edu/ ybao/project/frl-sep-expr/index.xml
[8] Bobot, B; Filliâtre, J-C, Separation predicates: a taste of separation logic in first-order logic, 167-181, (2012), Berlin · doi:10.1007/978-3-642-34281-3_14
[9] Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of object-oriented software: the KeY approach Lecture Notes in Computer Science, vol. 4334. Springer, Berlin (2007)
[10] Bao Y, Leavens GT, Ernst G (2015) Conditional effects in fine-grained region logic. In: Proceedings of the 17th Workshop on formal techniques for Java-like programs, FTfJP ’15. ACM, New York, NY, USA, pp 5:1-5:6
[11] Bao Y, Leavens GT, Ernst G (2016) Fine-grained region logic and unified fine-grained region logic. Technical report CS-TR-16-01, Computer Science, University of Central Florida, Orlando, FL, August 2016. http://www.eecs.ucf.edu/ ybao/tech-reports/FRL-UFRL-TR.pdf
[12] Barnett, M; Leino, KRM; Schulte, W; Barthe, G (ed.); Burdy, L (ed.); Huisman, M (ed.); Lanet, J-L (ed.); Muntean, T (ed.), The spec# programming system: an overview, No. 3362, 49-69, (2005), NY · doi:10.1007/978-3-540-30569-9_3
[13] Borgida, A; Mylopoulos, J; Reiter, R, On the frame problem in procedure specifications, IEEE Trans Softw Eng, 21, 785-798, (1995) · doi:10.1109/32.469460
[14] Banerjee B, Naumann DA (2013) Local reasoning for global invariants, part ii: dynamic boundaries. J ACM 60(3):19:1-19:73 · Zbl 1281.68153
[15] Banerjee, A; Naumann, DA, A logical analysis of framing for specifications with pure method calls, 3-20, (2014), Cham
[16] Banerjee, A; Naumann, DA; Rosenberg, S; Vitek, J (ed.), Regional logic for local reasoning about global invariants, No. 5142, 387-411, (2008), New York
[17] Banerjee A, Naumann DA, Rosenberg S (2013) Local reasoning for global invariants, part i: region logic. J ACM 60(3):18:1-18:56 · Zbl 1281.68154
[18] Brotherston J (2007) Formalised inductive reasoning in the logic of bunched implications. In: Proceedings of the 14th international conference on static analysis, SAS’07. Springer, Berlin, pp 87-103 · Zbl 1211.68081
[19] Cook B, Haase C, Ouaknine J, Parkinson M, Worrell J (2011) Tractable reasoning in a fragment of separation logic. In: CONCUR 2011-Concurrency theory: 22nd international conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings. Springer, Berlin, pp 235-249 · Zbl 1300.03017
[20] Chalin, P; Kiniry, JR; Leavens, GT; Poll, E, Beyond assertions: advanced specification and verification with JML and ESC/java2, No. 4111, 342-363, (2006), Berlin
[21] Cheon, Y; Leavens, GT; Sitaraman, M; Edwards, S, Model variables: cleanly supporting abstraction in design by contract, Softw Pract Exp, 35, 583-599, (2005) · doi:10.1002/spe.649
[22] Moura, L; Bjørner, N, Z3: an efficient SMT solver, No. 4963, 337-340, (2008), Berlin
[23] Distefano D, O’Hearn PW, Yang H (2006) A local shape analysis based on separation logic. In Proceedings of the 12th International conference on tools and algorithms for the construction and analysis of systems, TACAS’06. Springer, Berlin, pp 287-302 · Zbl 1180.68112
[24] Ernst G, Pfhler J, Schellhorn G,Haneberg D, Reif W (2014) Kiv: overview and verifythis competition. Int J Softw Tools Technol Transf 1-18
[25] Ford RL, Leino KRM (2017) Dafny reference manual (draft). https://github.com/Microsoft/dafny/blob/master/Docs/DafnyRef/out/DafnyRef.pdf
[26] Guttag, JV; Horning, JJ; Wing, JJ, The larch family of specification languages, IEEE Softw, 2, 24-36, (1985) · doi:10.1109/MS.1985.231756
[27] Hobor A, Villard J (2012) The ramifications of sharing in data structures. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13. ACM, New York, pp 523-536 · Zbl 1301.68180
[28] Ishtiaq SS, O’Hearn PW (2001) BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’01. ACM, New York, pp 14-26 · Zbl 1323.68077
[29] Jones, C.B.: Systematic software development using VDM. International Series in Computer Science, Prentice-Hall Inc, Englewood Cliffs (1986) · Zbl 0584.68008
[30] Jacobs B, Smans J, Piessens F (2010) The verifast program verifier: a tutorial
[31] Kassios, IT; Sekerinski, E (ed.); Misra, J (ed.); Nipkow, T (ed.), Dynamic frames: support for framing, dependencies and sharing without restrictions, No. 4085, 268-283, (2006), Berlin
[32] Kassios, IT, The dynamic frames theory, Form Asp Comput, 23, 267-288, (2011) · Zbl 1252.68192 · doi:10.1007/s00165-010-0152-5
[33] Leavens GT, Baker AL, Ruby C (2001) Preliminary design of JML: a behavioral interface specification language for Java. Technical Report 98-06q, Iowa State University, Department of Computer Science, December 2001. This is an obsolete version
[34] Leavens, GT; Baker, AL; Ruby, C, Preliminary design of JML: a behavioral interface specification language for Java, ACM SIGSOFT Softw Eng Notes, 31, 1-38, (2006) · doi:10.1145/1127878.1127884
[35] Leino KRM (1995) Toward reliable modular programs. Ph.D. thesis, California Institute of Technology. Available as Technical Report Caltech-CS-TR-95-03
[36] Leino, KRM, Data groups: specifying the modification of extended state, 144-153, (1998), New York
[37] Leino KRM (2008) Specification and verification of object-oriented software. Lecture notes from Marktoberdorf Internation Summer School. http://research.microsoft.com/en-us/um/people/leino/papers/krml190.pdf
[38] Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Logic for programming, artificial intelligence, and reasoning, 16th international conference, LPAR-16 (Lecture Notes in Computer Science), vol 6355. Springer, pp 348-370 · Zbl 1253.68095
[39] Leino, KRM; Müller, P; Castagna, G (ed.), A basis for verifying multi-threaded programs, No. 5502, 378-393, (2009), Berlin · Zbl 1234.68078
[40] Leino KRM, Monahan R (2010) Dafny meets the verification benchmarks challenge. In: Proceedings of the third international conference on verified software: theories, tools, experiments (Lecture Notes in Computer Science), vol 6217. Springer, Berlin, pp 112-126
[41] Leino, KRM; Nelson, G, Data abstraction and information hiding, ACM Trans Program Lang Syst, 24, 491-553, (2002) · doi:10.1145/570886.570888
[42] Leino KRM, Poetzsch-Heffter A, Zhou Y (2002) Using data groups to specify and check side effects. In: Proceedings of the ACM SIGPLAN 2002 Conference on programming language design and implementation (PLDI’02) (ACM SIGPLAN Notices), vol 37(5). ACM, New York, pp 246-257
[43] Müller, P; Poetzsch-Heffter, A; Leavens, GT, Modular invariants for layered object structures, Sci Comput Program, 62, 253-286, (2006) · Zbl 1100.68539 · doi:10.1016/j.scico.2006.03.001
[44] Mostowski W, Ulbrich M (2015) Dynamic dispatch for method contracts through abstract predicates. In: Proceedings of the 14th international conference on modularity, MODULARITY 2015. ACM, New York, pp 109-116
[45] Müller, P.: Modular specification and verification of object-oriented programs (Lecture Notes in Computer Science), vol. 2262. Springer, Berlin (2002) · Zbl 0998.68034 · doi:10.1007/3-540-45651-1
[46] Noble J, Vitek J, Potter J (1998) Flexible alias protection. In: Jul E (ed) ECOOP ’98—Object-oriented programming, 12th European conference, Brussels, Belgium (Lecture Notes in Computer Science), vol 1445. Springer, pp 158-185
[47] O’Hearn P, Reynolds J, Yang H (2001) Local reasoning about programs that alter data structures. In: Proceedings of CSL’01 (Lecture Notes in Computer Science), vol 2142. Springer, Berlin, pp 1-19 · Zbl 0999.68045
[48] O’Hearn PW, Yang H, Reynolds JC (2004) Separation and information hiding. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’04. ACM, New York, pp 268-280 · Zbl 1325.68069
[49] O’Hearn PW, Yang H, Reynolds JC (2009) Separation and information hiding. ACM Trans Program Lang Syst 31(3):11:1-11:50
[50] Parkinson MJ (2005) Local reasoning for Java. Technical Report 654, University of Cambridge Computer Laboratory, November 2005. The author’s Ph.D. dissertation
[51] Parkinson, M; Bierman, G; Palsberg, J (ed.); Abadi, M (ed.), Separation logic and abstraction, 247-258, (2005), New York · Zbl 1369.68151
[52] Parkinson, M; Bierman, G; Wadler, P (ed.), Separation logic, abstraction and inheritance, 75-86, (2008), New York · Zbl 1295.68091
[53] Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Log Methods Comput Sci 8(3), (2012) · Zbl 1256.03036
[54] Rosenberg, S; Banerjee, A; Naumann, DA, Decision procedures for region logic, 379-395, (2012), Berlin · Zbl 1326.68264 · doi:10.1007/978-3-642-27940-9_25
[55] Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of the seventeenth annual IEEE symposium on logic in computer science. IEEE Computer Society Press, Los Alamitos, pp 55-74
[56] Smans J, Jacobs B, Piessens F (2010) Heap-dependent expressions in separation logic. In: Proceedings of the 12th IFIP WG 6.1 international conference and 30th IFIP WG 6.1 international conference on formal techniques for distributed systems, FMOODS’10/FORTE’10. Springer, Berlin, pp 170-185
[57] Smans J, Jacobs B, Piessens F (2012) Implicit dynamic frames. ACM Trans Program Lang Syst 34(1):2:1-2:58
[58] Smans, J; Jacobs, B; Piessens, F; Schulte, W, Automatic verification of Java programs with dynamic frames, Form Asp Comput, 22, 423-457, (2010) · Zbl 1204.68131 · doi:10.1007/s00165-010-0148-1
[59] Tuerk T (2010) Local reasoning about while-loops. In: International conference on verified software: theories, tools and experiments—theory workshop (VS-Theory
[60] Weiß B (2011) Deductive Verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology
[61] Yang H, O’Hearn PW (2002) A semantic basis for local reasoning. In: Proceedings of the 5th international conference on foundations of software science and computation structures, FoSSaCS ’02. Springer, London, pp 402-416 · Zbl 1077.68705
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.