[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 |