×

Separation logics and modalities: a survey. (English) Zbl 1398.03151

Summary: Like modal logic, temporal logic, and description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we propose a selection of landmark results about decidability, complexity and expressive power.

MSC:

03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences
03B44 Temporal logic
03B45 Modal logic (including the logic of norms)
03D15 Complexity of computation (including implicit computational complexity)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., & Väänänen, J. (2011). From IF to BI: A tale of dependence and separation. CoRR, abs/1102.1388.
[2] Allen, J. (1983). Maintaining knowledge about temporal intervals. Communications of the ACM,26(11), 832-843. · Zbl 0519.68079
[3] Antonopoulos, T. (2010). Expressive power of query languages (Unpublished doctoral dissertation), University of Cambridge, UK.
[4] Antonopoulos, T., & Dawar, A. (2009). Separating graph logic from MSO. In L. de Alfaro (Ed.), Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (pp. 63-77). Berlin: Springer. · Zbl 1234.03022
[5] Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M. & Ouaknine, J. (2014). Foundations for decision problems in separation logic with general inductive predicates. In A. Muschol (Ed.), Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, proceedings (pp. 411-425). Berlin: Springer. · Zbl 1406.03046
[6] Areces, C., Blackburn, P., & Marx, M. (2001). Hybrid logics: Characterization, interpolation and complexity. The Journal of Symbolic Logic,66, 977-1010. · Zbl 0984.03018
[7] Aucher, G., Balbiani, P., Fariñas del Cerro, L., & Herzig, A. (2009). Global and Local Graph Modifiers. Electronic Notes in Theoretical Computer Science,231, 293–307.
[8] Baader, F., Calvanese, D., McGuinness, D., Nardi, D., & Patel-Schneider, P. (Eds.). (2003). The description logic handbook: Theory, implementation and applications. Cambridge: Cambridge University Press. · Zbl 1058.68107
[9] Balbiani, P., & Tinchev, T. (2014). Decidability and computability in PRSPDL. In R. Gor, B.P. Kooi & A. Kurucz (Eds.), Advances in Modal Logic 10, invited and contributed papers from the Tenth Conference on Advances in Modal Logic, held in Groningen, The Netherlands, August 5-8, 2014. (pp. 16-33). London: College Publications.
[10] Bansal, K., Brochenin, R., & Lozes, E. (2009). Beyond shapes: Lists with ordered data. In L. de Alfaro (Ed.), Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (pp. 425–439). Berlin: Springer. · Zbl 1234.68083
[11] Barrett, C., & Tinelli, C. (in press). Satisfiability modulo theories. In E. Clarke, T. Henzinger, & Veith, H. (Eds.), Handbook of model checking. Berlin: Springer. · Zbl 1392.68379
[12] Ben-Ari, M., Halpern, J., & Pnueli, A. (1982). Deterministic propositional dynamic logic: Finite models, complexity, and completeness. Journal of Computer and System Sciences,25, 402-417. · Zbl 0512.03013
[13] Benevides, M., de Freitas, R., & Viana, J. (2011). Propositional dynamic logic with storing, recovering and parallel composition. Electronic Notes in Theoretical Computer Science,269, 95-107. · Zbl 1347.03059
[14] Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., & Schnoebelen, P., (2001). Systems and software verification, model-checking techniques and tools. Berlin: Springer. · Zbl 1002.68029
[15] Berdine, J., Calcagno, C. & O’Hearn, P. (2004). A decidable fragment of separation logic. In K. Lodaya, & M. Mahajan (Eds.), FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, proceedings. (pp. 97-109) Berlin: Springer. · Zbl 1117.03337
[16] Berdine, J., Calcagno, C. & O’Hearn, P. (2005). Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W. P. de Roever (Eds.), Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, revised lectures (pp. 115-137) Berlin: Springer.
[17] Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic. Cambridge: Cambridge University Press. · Zbl 0988.03006
[18] Blackburn, P., van Benthem, J., & Wolter, F. (Eds.). (2006). Handbook of modal logic (Vol. 3). Philadelphia, PA: Elsevier. · Zbl 1114.03001
[19] Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., & Segoufin, L. (2011). Two-variable logic on data words. ACM Transactions on Computational Logic,12, 27. · Zbl 1352.03041
[20] Bojańczyk, M., & Lasota, S. (2010). An extension of data automata that captures XPath. In J.-P. Jouannaud & M. Escardó (Eds.), Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, UK (pp. 243-252). Washington, DC: IEEE Computer Society.
[21] Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., & David, C. (2006). Two-variable logic on words with data. In P. G. Kolaitis, R. Alur, & M. Veanes (Eds.), 21st IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, proceedings(pp. 7-16). Washington, DC: IEEE Computer Society.
[22] Börger, E., Grädel, E., & Gurevich, Y. (1997). The classical decision problem. Berlin: Springer.
[23] Bornat, R., Calcagno, C., O’Hearn, P., & Parkinson, M. (2005). Permission accounting in separation logic. In J. Palsberg & M. Abadi (Eds.), Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 (pp. 259-270). New York, NY: ACM Press. · Zbl 1369.68130
[24] Botincan, M., Parkinson, M., & Schulte, W. (2009). Separation logic verification of C programs with an SMT solver. Electronic Notes in Theoretical Computer Science,254, 5-23.
[25] Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2009). A logic-based framework for reasoning about composite data structures. In M. Bravetti & G. Zavattaro (Eds.), CONCUR 2009 - Concurrency Theory, 20th International Conference, Bologna, Italy, September 1-4, 2009. Proceedings (pp. 178-195). Berlin: Springer. · Zbl 1254.68146
[26] Bouyer, P. (2002). A logical characterization of data languages. Information Processing Letters,84, 75-85. · Zbl 1042.68544
[27] Bresolin, D., Della Monica, D., Goranko, V., Montanari, A. & Sciavicco, G. (2010). Metric propositional neighborhood logics: Expressiveness, decidability, and undecidability. In H. Coelho, R. Studer, & Wooldridge, M. (Eds.), ECAI 2010-19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, proceedings (pp. 695-700). Amsterdam: IOS Press. · Zbl 1211.68397
[28] Brochenin, R. (2013). Separation logic: Expressiveness, complexity, temporal extension. (Unpublished doctoral dissertation). École Normale Supérieure de Cachan, France.
[29] Brochenin, R., Demri, S., & Lozes, E. (2008). On the almighty wand. In M. K. S. Martini (Ed.), Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings (pp. 322-338). Berlin: Springer. · Zbl 1157.03010
[30] Brochenin, R., Demri, S., & Lozes, E. (2009). Reasoning about sequences of memory states. Annals of Pure and Applied Logic,161, 305-323. · Zbl 1225.68068
[31] Brochenin, R., Demri, S., & Lozes, E. (2012). On the almighty wand. Information and Computation,211, 106-137. · Zbl 1262.03051
[32] Brotherston, J. (2012). Bunched logics displayed. Studia Logica,100, 1223-1254. · Zbl 1282.03011
[33] Brotherston, J., Fuhs, C., Gorogiannis, N., & Navarro Perez, J. (2014). A decision procedure for satisfiability in separation logic with inductive predicates. In T. A. Henzinger, & D. Miller (Eds.), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14-18, 2014 (Paper No. 25). New York, NY: ACM Press. · Zbl 1401.68111
[34] Brotherston, J., & Kanovich, M. (2010). Undecidability of propositional separation logic and its neighbours. In J. P. Jouannaud & M. Escardó (Eds.), Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, UK (pp. 130-139). Washington, DC: IEEE Computer Society. · Zbl 1295.68166
[35] Brotherston, J., & Kanovich, M. (2014). Undecidability of propositional separation logic and its neighbours. Journal of the ACM,61, 14. · Zbl 1295.68166
[36] Brotherston, J., & Villard, J. (2014). Parametric completeness for separation theories. In S. Jagannathan & P. Sewell (Eds.), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 (pp. 453-464). New York NY: ACM Press. · Zbl 1284.68112
[37] Burstall, R. (1972). Some techniques for proving correctness of programs which alter data structures. Machine Intelligence,7, 23-50. · Zbl 0259.68009
[38] Calcagno, C., & Distefano, D. (2011). Infer: An automatic program verifier for memory safety of C programs. In M. G. Bobaru, K. Havelund, G. J. Holzmann, & R. Joshi (Eds.), NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (pp. 459-465). Berlin: Springer.
[39] Calcagno, C., Distefano, D., O’Hearn, P., & Yang, H. (2009). Compositional shape analysis by means of bi-abduction. In Z. Shao & B. C. Pierce (Eds.), Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009 (pp. 289-300). New York NY: ACM Press. · Zbl 1315.68085
[40] Calcagno, C., Gardner, P. & Hague, M. (2005). From separation logic to first-order logic. In V. Sassone (Ed.), Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, proceedings (pp. 395-409). Berlin: Springer. · Zbl 1119.03022
[41] Calcagno, C., Gardner, P., & Zarfaty, U. (2007). Context logic as modal logic: completeness and parametric inexpressivity. In M. Hofmann & M. Felleisen (Eds.), Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007 (pp. 123-134). New York NY: ACM Press. · Zbl 1295.68079
[42] Calcagno, C., O’Hearn, P., & Yang, H. (2001). Computability and complexity results for a spatial assertion language for data structures In R. Hariharan, M. Mukund & V. Vinay (Eds.), FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 21st Conference, Bangalore, India, December 13-15, 2001, proceedings (pp. 108-119). Berlin: Springer. · Zbl 1052.68590
[43] Calcagno, C., O’Hearn, P., & Yang, H. (2007). Local action and abstract separation logic. In M. Abadi, L. Ong, & J. Marcinkowski (Eds.), 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, proceedings (pp. 366-378). Washington DC: IEEE Computer Society.
[44] Calvanese, D., & Giacomo, G. D. (2005). Expressive description logics. In F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi & P.F. Patel-Schneider (Eds.), The description logic handbook: theory, implementation, and applications (pp. 178-218). Cambridge: Cambridge University Press.
[45] Cardelli, L., & Gordon, A. (2000). Anytime, anywhere: modal logics for mobile ambients. In M. N. Wegman & T. W. Reps (Eds.), POPL 2000, proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000 (pp. 365-377). New York, NY: ACM Press. · Zbl 1323.68405
[46] Charatonik, W., Kieroński, E., & Mazowiecki, F. (2014). Decidability of weak logics with deterministic transitive closure. In T. A. Henzinger, & D. Miller (Eds.), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14-18, 2014 (Paper No. 29). New York, NY: ACM Press. · Zbl 1394.03015
[47] Clarke, E., Grumberg, O., & Peled, D. (2000). Model checking. Cambridge, MA: MIT Press.
[48] Cook, B., Haase, C., Parkinson, M., & Worrell, J. (2011). Tractable reasoning in a fragment of separation logic. In J.-P. Katoen & B. König (Eds.), CONCUR 2011 - Concurrency Theory - 22nd International Conference, Aachen, Germany, September 6-9, 2011. Proceedings (pp. 235-249). Berlin: Springer. · Zbl 1300.03017
[49] Cooper, D. (1972). Theorem proving in arithmetic without multiplication. Machine Learning,7, 91-99. · Zbl 0258.68046
[50] Copeland, J. (2002). The genesis of possible worlds semantics. Journal of Philosophical Logic,31, 99-137. · Zbl 1006.03003
[51] Courtault, J.-R., & Galmiche, D. (2013). A modal BI logic for dynamic resource properties. In S. N. Artëmov & A. Nerode (Eds.), Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6-8, 2013. Proceedings (pp. 134-148). Berlin: Springer. · Zbl 1437.03116
[52] David, C. (2009). Analyse de XML avec données non-bornées (Unpublished doctoral dissertation). Paris Diderot University, France.
[53] Dawar, A., Gardner, P., & Ghelli, G. (2004). Adjunct elimination through games in static ambient logic. In K. Lodaya & M. Mahajan (Eds.), FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, proceedings (pp. 211-223). Berlin: Springer. · Zbl 1117.03338
[54] Dawar, A., Gardner, P., & Ghelli, G. (2007). Expressiveness and complexity of graph logic. Information and Computation,205, 263-310. · Zbl 1114.03028
[55] de Moura, L. & Björner, N. (2008). Z3: An efficient SMT solver. In C. R. Ramakrishnan & J. Rehof (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (pp. 337-340). Berlin: Springer.
[56] de Rijke, M. (1992). The modal logic of inequality. The Journal of Symbolic Logic,57, 566-584. · Zbl 0788.03019
[57] Demri, S. (2005). A reduction from DLP to PDL. Journal of Logic and Computation,15, 767-785. · Zbl 1092.03016
[58] Demri, S., & Deters, M. (2014). Expressive completeness of separation logic with two variables and no separating conjunction. In T. A. Henzinger, & D. Miller (Eds.), Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14-18, 2014 (Paper No. 37). New York, NY: ACM Press. · Zbl 1394.03054
[59] Demri, S., & Deters, M. (in press). Two-variable separation logic and its inner circle. ACM Transactions on Computational Logic. · Zbl 1354.03036
[60] Demri, S., & D’Souza, D. (2007). An automata-theoretic approach to constraint LTL. Information and Computation,205, 380-415. · Zbl 1113.03015
[61] Demri, S., Galmiche, D., Larchey-Wendling, D. & Mery, D. (2014). Separation Logic with One Quantified Variable. In E. A. Hirsch, S. O. Kuznetsov, J.-E. Pin, & N. K. Vereshchagin (Eds.), Computer Science – Theory and Applications – 9th International Computer Science Symposium in Russia, CSR 2014, Moscow, Russia, June 7–11, 2014. Proceedings (Vol. 8476 pp. 125-138). Berlin: Springer. · Zbl 1408.68036
[62] Demri, S. & Lazić, R. (2009). LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic,10, 16. · Zbl 1351.68158
[63] de Rijke, M. (1992). The modal logic of inequality. The Journal of Symbolic Logic, 57. 566-584. · Zbl 0788.03019
[64] Distefano, D., Katoen, J.-P. & Rensink, A. (2004). Who is pointing when to whom? On the automated verification of linked list structures. In K. Lodaya & M. Mahajan (Eds.), FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, proceedings (pp. 250-262). Berlin: Springer. · Zbl 1117.68427
[65] Distefano, D., O’Hearn, P., & Yang, H. (2006). A Local Shape Analysis Based on Separation Logic. In H. Hermanns & J. Palsberg (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-April 2, 2006, proceedings (pp. 287-302). Berlin: Springer.
[66] Enea, C., Saveluc, V., & Sighireanu, M. (2013). Compositional Invariant Checking for Overlaid and Nested Linked Lists. In M. Felleisen & P. Gardner (Eds.), Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16–24, 2013 (pp. 129–148). Proceedings Berlin: Springer. · Zbl 1381.68051
[67] Etessami, K., Vardi, M., & Wilke, T. (1997). First-Order Logic with Two variables and Unary Temporal logics. In M. Y. Vardi & G. W. J. Tiuryn (Eds.), Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29-July 2, 1997 Washington (pp. 228-235). DC: IEEE Computer Society. · Zbl 1096.03013
[68] Figueira, D. (2010). Reasoning on words and trees with data. Thesis (PhD). École Normale Supérieure de Cachan, France.
[69] Figueira, D., & Segoufin, L. (2009). Future-looking logics on data words and trees. In R. Královic & D. Niwinski (Eds.), Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009 (pp. 331–343). Proceedings Berlin: Springer. · Zbl 1250.03050
[70] Fine, K. (1975). Some connections between elementary and modal logic. In S. Kanger (Ed.), Proceedings of the 3rd Scandinavian Logic Symposium (pp. 15-31). Amsterdam North Holland. · Zbl 0316.02021
[71] Fitting, M. (1983). Proof methods for modal and intuitionistic logics. Dordrecht: D. Reidel. · Zbl 0523.03013
[72] Floyd, R. (1967). Assigning Meanings to Programs. Proceedings of Symposia in Applied Mathematics,19, 19-32. · Zbl 0189.50204
[73] Gabbay, D. (1981). Expressive Functional Completeness in Tense Logic. In U. Mönnich (Ed.), Aspects of Philosophical Logic (pp. 91-117). Dordrecht: D. Reidel. · Zbl 0523.03017
[74] Gabbay, D., Hodkinson, I., & Reynolds, M. (1994). Temporal Logic: Mathematical Foundations and Computational Aspects, (Vol. 1). Oxford: Oxford University Press. · Zbl 0921.03023
[75] Gabbay, D., Kurucz, A., Wolter, F., & Zakharyaschev, M. (2003). Many-dimensional modal logics: Theory and practice. Cambridge: Cambridge University Press. · Zbl 1051.03001
[76] Galmiche, D., & Méry, D. (2010). Tableaux and Resource Graphs for Separation Logic. Journal of Logic and Computation,20, 189–231. · Zbl 1193.03061
[77] Gardner, P., & Zarfaty, U. (2007). An Introduction to Context Logic. In D. Leivant & R. J. G. B. de Queiroz (Eds.), Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2-5, 2007, proceedings (pp. 189-202). Berlin: Springer. · Zbl 1213.03039
[78] Göller, S. (2007). On the Complexity of Reasoning About Dynamic Policies. In J. Duparc & T. A. Henzinger (Eds.), Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, proceedings (pp. 358-373). Berlin: Springer. · Zbl 1179.03037
[79] Goranko, V., & Passy, S. (1992). Using the universal modality: Gains and questions. Journal of Logic and Computation,2, 5-30. · Zbl 0774.03003
[80] Gordon, M. (2014). Hoare Logic [Lecture notes]. Retrieved from http://www.cl.cam.ac.uk/mjcg/HoareLogic/.
[81] Grädel, E., Kolaitis, P., & Vardi, M. (1997). On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic,3, 53-69. · Zbl 0873.03009
[82] Grädel, E., Otto, M., & Rosen, E. (1999). Undecidability Results on Two-Variable Logics. Archive for Mathematical Logic,38, 313–354. · Zbl 0927.03015
[83] Haase, C., Ishtiaq, S., Ouaknine, J., & Parkinson, M., (2013). SeLoger: A Tool for Graph-Based Reasoning in Separation Logic. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013 (pp. 790–795). Proceedings Berlin: Springer.
[84] Harel, D., Kozen, D., & Tiuryn, J. (2000). Dynamic Logic. Cambridge, MA: MIT Press. · Zbl 0976.68108
[85] Hella, L., & Kuustisto, A. (2014). One-dimensional fragment of first-order logic. In R. Goré, B. P. Kooi & A. Kurucz (Eds.), Advances in Modal Logic 10, invited and contributed papers from the Tenth Conference on Advances in Modal Logic, held in Groningen, The Netherlands, August 5-8, 2014 (pp. 274-293). London: College Publications.
[86] Hella, L., Luosto, K., Sano, K., & Virtema, J. (2014). The expressive power of modal independence logic. In R. Goré, B. P. Kooi & A. Kurucz (Eds.), Advances in Modal Logic 10, invited and contributed papers from the Tenth Conference on Advances in Modal Logic, held in Groningen, The Netherlands, August 5-8, 2014 (pp. 294-312). London: College Publications. · Zbl 1385.03018
[87] Hemaspaandra, E. (1996). The price of Universality. Notre Dame Journal of Formal Logic,37, 173-203. · Zbl 0865.03032
[88] Hennessy, M., & Milner, R. (1980). On observing nondeterminism and concurrency. In J. W. Bakker & J. van Leeuwen (Eds.), Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, July 14-18, 1980, proceedings (pp. 299-309). Berlin: Springer. · Zbl 0441.68018
[89] Herzig, A. (2013). A Simple Separation Logic. In L. Libkin, U. Kohlenbach, & R. J. G. B. de Queiroz (Eds.), Logic, Language, Information, and Computation - 20th International Workshop, WoLLIC 2013, Darmstadt, Germany, August 20-23, 2013. Proceedings (pp. 168-178). Berlin: Springer. · Zbl 1395.03017
[90] Hoare, C. (1969). An axiomatic basis for computer programming. Communications of the ACM,12, 576–580. · Zbl 0179.23105
[91] Hodkinson, I., & Reynolds, M. (2005). Separation - past, present, and future. In S. Artemov, H. Barringer, A. d’Avila, L. Garcez & J. Woods (Eds.), We will show them! Essays in honour of Dov Gabbay on his 60th birthday. London: College Publications. (Vol. 2, pp. 117-142).
[92] Hou, Z., Clouston, R., Goré, R., & Tiu, A. (2014). Proof search for propositional abstract separation logics via labelled sequents. In S. Jagannathan & P. Sewell (Eds.), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 New York (pp. 465–476). NY: ACM Press. · Zbl 1284.68402
[93] Hughes, G., & Cresswell, M. (1968). An introduction to modal logic. York: Methuen. · Zbl 0205.00503
[94] Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., & Yorsh, G. (2004). The boundary between decidability and undecidability for transitive-closure logics. In J. Marcinkowski & A. Tarlecki (Eds.), Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, proceedings (pp. 160-174). Berlin: Springer. · Zbl 1095.03008
[95] Iosif, R., Rogalewicz, A., & Simacek, J. (2013). The Tree Width of Separation Logic with Recursive Definitions. In M. P. Bonacina (Ed.), Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013 (pp. 21-38). Proceedings Berlin: Springer. · Zbl 1329.03068
[96] Ishtiaq, S., & O’Hearn, P. (2001). BI as an Assertion Language for Mutable Data Structures. In C. Hankin & D. Schmidt (Eds.), Conference record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001 New York (pp. 14-26). NY: ACM Press. · Zbl 1323.68077
[97] Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., & Sagiv, M. (2013). Effectively-Propositional Reasoning about Reachability in Linked Data Structures. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (pp. 756-772). Berlin: Springer.
[98] Janin, D. & Walukiewicz, I. (1996). On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In U. Montanari & V. Sassone (Eds.), CONCUR ’96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, proceedings (pp. 263-277). Berlin: Springer.
[99] Jensen, J. (2013a). Enabling Concise and Modular Specifications in Separation Logic. Thesis (PhD). IT University of Copenhagen, Denmark.
[100] Jensen, J. (2013b). Techniques for model construction in separation logic. Retrieved from http://www.itu.dk/research/pls/wiki/index.php/JonasBuhrkalJensen
[101] Kaminski, M., & Francez, N. (1994). Finite-memory automata. Theoretical Computer Science,134, 329–363. · Zbl 0938.68711
[102] Kamp, J. (1968). Tense Logic and the Theory of Linear Order. (Unpublished doctoral dissertation). University of California, Los Angeles, USA.
[103] Kontinen, J., Müller, J., Schnoor, S., & Vollmer, H. (2014). Modal independence logic. In R. Goré, B. P. Koo & A. Kurucz (Eds.), Advances in Modal Logic 10, invited and contributed papers from the Tenth Conference on Advances in Modal Logic, held in Groningen, The Netherlands, August 5-8, 2014 (pp. 353-372). London: College Publications.
[104] Kripke, S. (1959). A completeness theorem in modal logic. The Journal of Symbolic Logic,24, 1-14. · Zbl 0091.00902
[105] Kuncak, V., & Rinard, M. (2004). On spatial conjunction as second-order logic Technical report MIT-CSAIL-TR-2004-067. Cambridge, MA: MIT Computer Science and Artificial Intelligence Laboratory.
[106] Ladner, R. (1977). The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computing,6, 467-480. · Zbl 0373.02025
[107] Larchey-Wendling, D., & Galmiche, D. (2010). The undecidability of boolean BI through Phase Semantics. In J.-P. Jouannaud & M. Escardó (Eds.), Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11–14 July 2010 (pp. 140–149). Edinburgh, UK Washington, DC: IEEE Computer Society. · Zbl 1343.03022
[108] Larchey-Wendling, D., & Galmiche, D. (2013). Nondeterministic Phase Semantics and the Undecidability of Boolean BI. ACM Transactions on Computational Logic,14, 6. · Zbl 1343.03022
[109] Lee, W., & Park, S. (2014). A proof system for separation logic with magic wand. In S. Jagannathan & P. Sewell (Eds.), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 New York (pp. 477–490). NY: ACM Press. · Zbl 1284.68408
[110] Lewis, C. I. (1918). A survey of symbolic logic. Berkeley, CA: University of California Press.
[111] Libkin, L. (2004). Elements of Finite Model Theory. Berlin: Springer. · Zbl 1060.03002
[112] Löding, C., & Rohde, P. (2003). Model Checking and Satisfiability for Sabotage Modal Logic. P. K. Pandya & J. Radhakrishnan (Eds.), FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Mumbai, India, December 15–17, 2003, proceedings (pp. 302-313). Berlin: Springer. · Zbl 1205.68222
[113] Lozes, E. (2004a). Expressivité des Logiques Spatiales. (Unpublished doctoral dissertation). École Normale Supérieure de Lyon, France.
[114] Lozes, E. (2004b, January). Separation logic preserves the expressive power of classical logic. Paper presented at the 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE’04), Venice, Italy.
[115] Lozes, E. (2012). Separation Logic: Expressiveness and Copyless Message-Passing. (Unpublished habilitation dissertation). École Normale Supérieure de Cachan, France.
[116] Lutz, C. (2006). Complexity and succinctness of public announcement logic. In H. Nakashima, M. P. Wellman, G. Weiss, & P. Stone (Eds.), 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8-12, 2006 New York (pp. 137–143). NY: ACM Press.
[117] Lutz, C., Sattler, U., & Wolter, F. (2001). Modal logic and the two-variable fragment. In L. Fribourg (Ed.), Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, proceedings (pp. 247-261). Berlin: Springer. · Zbl 0999.03020
[118] Madhusudan, P., Parlato, G., & Qiu, X. (2011). Decidable logics combining heap structures and data. In T. Ball & M. Sagiv (Eds.), Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011 New York (pp. 611–622). NY: ACM Press. · Zbl 1284.68411
[119] Manna, Z., & Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems. Berlin: Springer. · Zbl 0753.68003
[120] Marcinkowski, J. (2006). On the expressive power of graph logic. In Z. Ésik (Ed.), Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, proceedings (pp. 486-500). Berlin: Springer. · Zbl 1225.03030
[121] Marx, M., & de Rijke, M. (2005). Semantic characterizations of navigational XPath. SIGMOD Record,34(2), 41–46.
[122] Marx, M., & Venema, Y. (1997). Multi-Dimensional Modal Logic. Applied Logic Dordrecht: Kluwer Academic. · Zbl 0942.03029
[123] Minsky, M. (1967). Computation: Finite and Infinite Machines. Upper Saddle River, NJ: Prentice-Hall. · Zbl 0195.02402
[124] Moore, R. C. (1977). Reasoning about knowledge and action. In R. Reddy (Ed.), Proceedings of the 5th International Joint Conference on Artificial Intelligence, Cambridge, MA, US, August 1977 San Francisco (pp. 223–227). San Francisco, CA: William Kaufmann.
[125] Morgan, C. (1976). Methods for automated theorem proving in nonclassical logics. IEEE Transactions on Computers,25, 852-862. · Zbl 0329.68074
[126] Moszkowski, B. (1983). Reasoning about Digital Circuits (Tech. Rep. No. STAN-CS-83-970). Stanford, CA: Department of Computer Science, Stanford University.
[127] Neven, F., Schwentick, T., & Vianu, V. (2004). Finite State Machines for Strings Over Infinite Alphabets. ACM Transactions on Computational Logic,5, 403-435. · Zbl 1367.68175
[128] O’Hearn, P. (2012). A primer on separation logic (and automatic program verification and analysis). In T. Nipkow, O. Grumberg & B. Hauptmann (Eds.), Software Safety and Security: Tools for Analysis and Verification (pp. 286-318). Amsterdam: IOS Press.
[129] O’Hearn, P., & Pym, D. (1999). The logic of bunched implications. Bulletin of Symbolic Logic,5, 215–244. · Zbl 0930.03095
[130] Ohlbach, H., Nonnengart, A., de Rijke, M., & Gabbay, D. (2001). Encoding two-valued non-classical logics in classical logic. In A. Robinson & A. Voronkov (Eds.), Handbook of Automated Reasoning Philadelphia (pp. 1403–1486). Philadelphia, PA: Elsevier. · Zbl 0992.03019
[131] Pérez, J. N., & Rybalchenko, A. (2013). Separation Logic Modulo Theories. In C. Shan (Ed.), Programming Languages and Systems -11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013, Proceedings (pp. 90–106). Berlin: Springer. · Zbl 1426.68058
[132] Piskac, R., Wies, T., & Zufferey, D. (2013). Automating Separation Logic using SMT. In N. Sharygina & H. Veith (Eds.), Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings (pp. 773-789). Berlin: Springer.
[133] Pnueli, A. (1977). The temporal logic of programs. IEEE Computer Society (Ed.), Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October-1 November 1977 (pp. 46-57). Washington, DC: IEEE Computer Society.
[134] Prior, A. (1967). Past, Present and Future. Oxford: Oxford University Press. · Zbl 0169.29802
[135] Pucella, R., Weissman, V. & Walukiewicz, I. (2004). Reasoning about Dynamic Policies. In I. Walukiewicz (Ed.), Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29–April 2, 2004, proceedings (pp. 453-467). Berlin: Springer. · Zbl 1126.03317
[136] Pym, D. (2002). The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Dordrecht: Kluwer Academic. · Zbl 1068.03001
[137] Pym, D., O’Hearn, P., & Yang, H. (2004). Possible worlds and resources: The semantics of BI. Theoretical Computer Science,315, 257-305. · Zbl 1055.03021
[138] Qiu, X. (2013). Automatic techniques for proving correctness of heap-manipulating programs. (Unpublished doctoral dissertation). University of Illinois at Urbana-Champaign, USA.
[139] Qiu, X., Garg, P., Stefanescu, A., & Madhusudan, P. (2013). Natural proofs for structure, data, and separation. In H. J. Boehm & C. Flanagan (Eds.), ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013 New York (pp. 231-242). NY: ACM Press.
[140] Rabin, M. (1969). Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society,41, 1-35. · Zbl 0221.02031
[141] Rabinovich, A. (2014). A proof of Kamp’s theorem. Logical Methods in Computer Science, 10(1:14). · Zbl 1326.03024
[142] Rakamaric, Z., Bruttomesso, R., Hu, A., & Cimatti, A. (2007). Verifying Heap-Manipulating Programs in an SMT Framework. In K. S. Namjoshi, T. Yoneda, T. Higashino & Y. Okamura (Eds.), Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, proceedings (pp. 237-252). Berlin: Springer. · Zbl 1141.68484
[143] Reynolds, J. (2000). Intuitionistic reasoning about shared mutable data structure. In J. Davies & B. Roscoe (Eds.), Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare (pp. 303-321). London: Palgrave Macmillan.
[144] Reynolds, J. (2002). Separation logic: A logic for shared mutable data structures. In S. Abramsky, G. D. Plotkin, & U. Kohlenbach (Eds.), 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, proceedings Washington (pp. 55-74). DC: IEEE Computer Society.
[145] Reynolds, J. (2008). An Overview of Separation Logic. In B. Meyer & J. Woodcock (Eds.), Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, revised selected papers and discussions (pp. 460-469). Berlin: Springer.
[146] Rohde, P. (2004). Moving in a crumbling network: The balanced case. In J. Marcinkowski & A. Tarlecki (Ed.), Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, proceedings (pp. 310-324). Berlin: Springer. · Zbl 1095.03018
[147] Savitch, W. (1970). Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences,4, 177-192. · Zbl 0188.33502
[148] Schmitz, S. (2013). Complexity Hierarchies Beyond Elementary.. CoRR,abs/1312.5686. · Zbl 1347.68162
[149] Schmitz, S., & Zeume, T. (2013). Two-variable logic and two order relations. Logical Methods in Computer Science, 8(1:15).
[150] Segoufin, L., & Toruńczyk, S. (2011). Automata based verification over linearly ordered data domains. T. Schwentick & C. Dürr (Eds.), 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, March 10-12, 2011, Dortmund (pp. 81-92). Wadern: Leibniz-Zentrum für Informatik.
[151] Sighireanu, M., & Cok, D. (in press). Report on SL-COMP 2014. Journal of Satisfiability, Boolean Modeling and Computation.
[152] Spaan, E. (1993). The complexity of propositional tense logics. In M. de Rijke (Ed.), Diamonds and defaults (pp. 287-309). Dordrecht: Kluwer Academic. · Zbl 0831.03005
[153] Straubing, H. (1994). Finite Automata, Formal Logic, and Circuit Complexity. Progress in Theoretical Computer Science Boston, MA: Birkhäuser. · Zbl 0816.68086
[154] Tatsuta, M. & Chin, W.-N. (2014). Completeness of Separation Logic with Inductive Definitions for Program Verification. In D. Giannakopoulou & G. Salaün (Eds.), Software Engineering and Formal Methods - 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014, Proceedings (pp. 20-34). Berlin: Springer.
[155] Tatsuta, M., Chin, W. N., & Ameen, M. A. (2009). Completeness of Pointer Program Verification by Separation Logic. In D. V. Hung & P. Krishnan (Eds.), Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23-27 November 2009 (pp. 179–188). Washington DC: IEEE Computer Society.
[156] Thakur, A., Breck, J., & Reps, T. (2014). Satisfiability modulo abstraction for separation logic with linked lists. In N. Rungta & O. Tkachuk (Eds.), 2014 International Symposium on Model Checking of Software, SPIN 2014, proceedings, San Jose, CA, USA, July 21-23, 2014 (pp. 58–67). New York NY: ACM Press.
[157] Trakhtenbrot, B. (1963). Impossibility of an algorithm for the decision problem in finite classes. AMS Translations, Series,2(23), 1-5. · Zbl 0121.01507
[158] Tuerk, T. (2011). A separation logic fragment for HOL. (Unpublished doctoral dissertation). University of Cambridge, UK.
[159] Vafeiadis, V., & Parkinson, M. (2007). A marriage of rely/guarantee and separation logic. In L. Caires & V. T. Vasconcelos (Eds.), CONCUR 2007 - Concurrency Theory, 18th International Conference, Lisbon, Portugal, September 3-8, 2007, proceedings (pp. 256-271). Berlin: Springer. · Zbl 1151.68556
[160] van Benthem, J. (1976). Correspondence Theory. (Unpublished doctoral dissertation). University of Amsterdam, The Netherlands.
[161] van Benthem, J. (2005). An essay on sabotage and obstruction. In D. Hutter & D. Stephan (Eds.), Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of his 69th Birthday (pp. 268-276). Berlin: Springer. · Zbl 1098.68632
[162] Vardi, M. (1982). The complexity of relational query languages. In H. R. Lewis, B. B. Simons, W. A. Burkhard, & L. H. Landweber (Eds.), Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA (pp. 137-146). New York, NY: ACM Press.
[163] Weber, T. (2004). Towards Mechanized Program Verification with Separation Logic. J. Marcinkowski, & A. Tarlecki (Eds.), Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, proceedings (pp. 250-264). Berlin: Springer. · Zbl 1095.68058
[164] Weis, P. (2011). Expressiveness and succinctness of first-order logic on finite words. (Unpublished doctoral dissertation). University of Massachussetts - Amherst, USA.
[165] Wolper, P. (1983). Temporal logic can be more expressive. Information and Control,56, 72-99. · Zbl 0534.03009
[166] Yahav, E., Reps, T., Sagiv, M. & Wilhelm, R. (2003). Verifying temporal heap properties specified via evolution logic. In P. Degano (Ed.), Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, proceedings (pp. 204-222). Berlin: Springer. · Zbl 1032.68062
[167] Yang, H. (2001). Local Reasoning for Stateful Programs (Unpublished doctoral dissertation). University of Illinois at Urbana-Champaign, USA.
[168] Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, p. (2008). Scalable Shape Analysis for Systems Code. In A. Gupta & S. Malik (Eds.), Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, proceedings (pp. 385-398). Berlin: Springer. · Zbl 1155.68359
[169] Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, M., & Bouajjani, A. (2006). A logic of reachable patterns in linked data-structures. In L. Aceto, & A. Ingólfsdóttir (Eds.), Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006, proceedings (pp. 94-110). Berlin: Springer. · Zbl 1180.68131
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.