Bibliography

# [Brotherston&Kanovich10] J. Brotherston and M. Kanovich. Undecidability of propositional separation logic and its neighbours. In 25th Annual IEEE} Symposium on Logic in Computer Science, LICS 2010, pages 137--146, Edinburgh, UK, July 2010.

# [Dawar&Gardner&Ghelli04] A. Dawar, P. Gardner and G. Ghelli. Adjunct elimination through games in static ambient logic. FSTTCS’04, pages 211-223, vol. 3328, LNCS, Springer, 2004.

# [Galmiche&Larchey06] D. Galmiche and D. Larchey-Wending. Expressivity properties of Boolean BI through relational models. FSTTCS'06, pages 358—369, Vol. 4337 of LNCS, 2006.

# [Abramsky 97] S. Abramsky. Semantics of interaction: an introduction to game semantics. In ''Semantics and Logics of Computation,'' pp. 1-32. Cambridge University Press, 1997.

# [Abramsky 97] S. Abramsky. Semantics of interaction: an introduction to game semantics. In ''Semantics and Logics of Computation,'' pp 1-32. Cambridge University Press, 1997.

# [Antonopoulos & Dawar 09] T. Antonopoulos and A. Dawar. Separating Graph Logic from MSO. In ''FOSSACS'09,'' LNCS 5504, pp. 63-77, Springer 2009.

# [Aucher et al 09] G. Aucher and Ph. Balbiani and L. Fariñas del Cerro and A. Herzig. Global and Local Graph Modifiers. ''ENTCS 231,'' 293-307, 2009.

# [Balbiani & Condotta 02] Ph. Balbiani and J.F. Condotta. Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In ''FroCoS'02,'' LNAI 2309, 162--173, Springer 2002.

# [Balbiani et al 10] Tableaux for public announcement logics. ''Journal of Logic and Computation, Special Issue on Tableaux and Analytic Proof Methods,'' vol. 20 (1) 55-76, 2010.

# [Abramsky 97] S. Abramsky. Semantics of interaction: an introduction to game semantics. In ''Semantics and Logics of Computation,'' pp 1--32. Cambridge University Press, 1997.

# [Antonopoulos & Dawar 09] T. Antonopoulos and A. Dawar. Separating Graph Logic from MSO. In ''FOSSACS'09, LNCS 5504,'' pp. 63--77, Springer 2009.

# [Aucher et al 09] G. Aucher and Ph. Balbiani and L. Fariñas del Cerro and A. Herzig. Global and Local Graph Modifiers. ''ENTCS'' 231:293--307, 2009.

# [Abramsky 97] S. Abramsky. ''Semantics of interaction: an introduction to game semantics.'' In Semantics and Logics of Computation, pp 1--32. Cambridge University Press, 1997.

# [Abramsky 97] S. Abramsky. 'Semantics of interaction: an introduction to game semantics.' In Semantics and Logics of Computation, pp 1--32. Cambridge University Press, 1997.

# [Bansal & Brochenin & Lozes 09] K. Bansal and R. Brochenin and E. Lozes. Beyond Shapes: Lists with Ordered Data. In FOSSACS'09, LNCS 5504, pp. 425--439, Springer 2009.

# [Berard et al 01] B. Bérard and M. Bidoit and A. Finkel and F. Laroussinie and A. Petit and L. Petrucci and Ph. Schnoebelen. Systems and Software Verification, Model-Checking Techniques and Tools, Springer, 2001.

# [Berdine & Calcagno & OHearn 04] J. Berdine, C. Calcagno, and P. O'Hearn. A decidable fragment of separation logic. In FSTTCS'04, LNCS 3328, pp. 97--109, Springer, 2004..

# [Berdine & Calcagno & OHearn 05] J. Berdine and C. Calcagno and P. W. O'Hearn. Symbolic execution with separation logic. In APLAS'05, pages 52--68, vol. 3780 of LNCS, 2005.

# [Berdine & Calcagno & OHearn 05] J. Berdine, C. Calcagno, and P. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO'05, LNCS 4111, pp. 115--137, Springer, 2005.

# [Berdine et al 06] J. Berdine, B. Cook, D. Distefano, and P. O'Hearn. Automatic termination proof for programs with shape-shifting heaps. In CAV'06, LNCS 4144, pp. 386--400, 2006.

# [Biri & Galmiche 03] N. Biri and D. Galmiche. A Separation Logic for Resource Distribution --extended abstract--. In FST&TCS'03, pages 23--37, vol. 2914 of LNCS, 2003.

# [Biri & Galmiche 07] N. Biri and D. Galmiche. Models and Separation Logics for Resource Trees. Journal of Logic and Computation, 17(4):687--726, 2007.

# [Blackburn & de Rijke & Venema 01] P. Blackburn, M. de Rijke, Y. Venema. Modal logic, Cambridge University Press, New York, NY, USA, 2001.

# [Abramsky 97] S. Abramsky. Semantics of interaction: an introduction to game semantics. In Semantics and Logics of Computation, pp 1--32. Cambridge University Press, 1997.

# [Antonopoulos & Dawar 09] T. Antonopoulos and A. Dawar. Separating Graph Logic from MSO. In FOSSACS'09, LNCS 5504, pp. 63--77, Springer 2009.

# [Aucher et al 09] G. Aucher and Ph. Balbiani and L. Fariñas del Cerro and A. Herzig. Global and Local Graph Modifiers. ENTCS 231: 293-307, 2009.

# [Balbiani & Condotta 02] Ph. Balbiani and J.F. Condotta. Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In FroCoS'02, LNAI 2309, pp. 162--173, Springer 2002.

# [Balbiani et al 08] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi, and T. De Lima. "knowable" as "known after an announcement". To appear, 2008.

# [Balbiani et al 10] Tableaux for public announcement logics. Journal of Logic and Computation, Special Issue on Tableaux and Analytic Proof Methods, Vol. 20, n. 1, p. 55-76, 2010.

# [Balbiani & Cheikh & Feuillade 09] Ph. Balbiani, F. Cheikh, G. Feuillade. Algorithms and Complexity of Automata Synthesis by Asynchronous Orchestration With Applications to Web Services Composition. ENTCS 229(3): 3-18 (2009).

# [Balbiani & Echahed & Herzig 10] A modal Logic for Termgraph Rewriting. International Conference on Graph Transformation (ICGT 2010), Twente, LNCS 6372, p. 59-74, 2010.

# [Baltag & Moss 04] A. Baltag and L. Moss. Logics for epistemic programs. Synthese, 139(2):165–224, 2004.

# [Baltag & Smets 08] A. Baltag and S. Smets. Probabilistic dynamic belief revision. Synthese 165 (2): 179-202 (2008)

# [Demri&Lazic09] S. Demri and R. Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), 2009.

# [Distefano&Katoen&Rensink04] D. Distefano and J. P. Katoen and A. Rensink. Who is pointing when to whom? FST\&TCS’04, pages 250—262, vol. 3328, LNCS, Springer, 2004.

# [Distefano&OHearn&Yang06] D. Distefano, P. O’Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS'06, LNCS 3920, pp. 287--302, Springer, 2006.

# [Doods08] From Separation Logic to Hyperedge Replacement and Back. 4th Int. Conference on Graph Transformation,ICGT08, Leicester, UK, september 2008.

# [Engberg&Winskel90] U. Engberg and G. Winskel. Petri nets as models of linear logic. In CAAP'90, LNCS 431, pp. 147--161, Springer, 1990.

# [Faggian&Hyland02] C. Faggian and M. Hyland. Designs, disputes and strategies. 16th Int. Workshop on Computer Science Logic, CSL 2002, LNCS 2471, pages 442--457, September 2002.

# [Fermüller03] C. Fermüller. Parallel dialogue games and hypersequents for intermediate logics. Int. Conference on Analytic Tableaux and Related Methods, TABLEAUX 2003, LNAI 2796, pages 48--64, Rome, Italy, 2003.

# [Finkel&Lozes&Sangnier07] A. Finkel, E. Lozes, and A. Sangnier. Towards model checking pointer systems. In Benedikt Lowe, editor, Proceedings of the International Conference on Infinity in Logic and Computation (ILC'07)}, Cape Town, South Africa, November 2007.

# [Finkel&Schnoebelen01] A. Finkel and Ph. Schnoebelen.Well-structured transitions systems everywhere! TCS, 256(1--2):63--92, 2001.

# [Finkel&Lozes&Sangnier09] A. Finkel, E. Lozes and A. Sangnier. Towards Model Checking Pointer Systems. In ILC'07, LNAI 5489, pp. 56-82. Springer, 2009.

# [Galmiche&Larchey06] D. Galmiche and D. Larchey-Wending. Expressivity properties of Boolean BI through relational models. FST&TCS'06, pages 358—369, Vol. 4337 of LNCS, 2006.

# [Galmiche&Larchey99] D. Galmiche and D. Larchey-Wendling. Structural Sharing and Efficient Proof-search in Propositional Intuitionistic Logic. In ASIAN'99, LNCS 1742, pp. 101--112, Springer, 1999.

# [Galmiche&Mery02] D. Galmiche and D. Méry. Connection-based proof search in propositional BI logic. in CADE-18, pages 111-128, vol. 2392 of LNCS, 2002.

# [Galmiche&Mery05] D. Galmiche and D. Méry. Characterizing provability in BI's Pointer Logic through Resource Graphs. In LPAR'05, pages 459—473, vol. 3835 of LNCS, 2005

# [Galmiche&Mery05a] D. Galmiche and D. Méry. Resource graphs and countermodels in resource logics. In ENTCS, 125(3):117--135, 2005.

# [Galmiche&Mery09] D. Galmiche and D. Méry. Tableaux and resource graphs for separation logic. Journal of Logic and Computation, 20:1, pp 189 – 231, 2010.

# [Galmiche&Mery&Pym02] D. Galmiche and D. Méry and D. Pym. Resource tableaux (extended abstract). In CSL'02, pages 183—199, vol. 2471 of LNCS, 2002.

# [Galmiche&Mery&Pym05] D. Galmiche, D. Méry, and D. Pym. The semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science, 15(6):1033--1088, 2005.

# [Galmiche&Salhi08] D. Galmiche and Y. Salhi. Calculi for an intuitionistic hybrid modal logic. In Int Workshop on Intuitionistic Modal Logic and Applications, IMLA'08, 2008.

# [Galmiche&Salhi10a] D. Galmiche and Y. Salhi. A Family of Gôdel Hybrid Logics. Journal of Applied Logic 8, p. 371—385. 2010

# [Galmiche&Salhi10b] D. Galmiche and Y. Salhi. Label-free Proof Systems for Intuitionistic Modal Logic IS5. Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16, LNAI 6355, p. 255—271, Dakar, Senegal, June 2010.

# [Gasquet&Said08] O. Gasquet and B. Said. Efficient graph rewriting system using local event-driven pattern matching. To appear, 2008.

# [Girard95] J.Y. Girard. Proof nets: the parallel syntax for proof theory. In Logic and Algebra, M. Dekker, 1995.

# [Gradel&Kolaitis&Vardi97] E. Gradel, Ph. Kolaitis, M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53--69, 1997.

# [Halpern-etal01] J. Halpern and R. Harper and N. Immerman and Ph. Kolaitis and M. Vardi and V. Vianu. On the Unusual Effectiveness of Logic in Computer Science. Bulletin of Symbolic Logic 7(2):213--236, 2001.

# [Hirschkoff&Lozes&Sangiorgi02] D. Hirschkoff, E. Lozes and D. Sangiorgi. Separability, expressiveness and decidability of the Ambient Logic. In Procs. of Logics In Computer Science, pages 423-432, 2002.

# [Hirschkoff&Lozes&Sangiorgi03] D. Hirschkoff, E. Lozes and D. Sangiorgi. Minimality results for the spatial logics. In Procs. of FSTTCS’03, pages 252-264, vol. 2914 of LNCS, 2003.

# [Ishtiaq&Ohearn01] S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In POPL'01, pages 14—26, 2001.

# [Jensen-etal97] J. Jensen and M. Jorgensen and N. Klarlund and M. Schwartzbach. Automatic Verification of Pointer Programs using Monadic Second-order Logic. In PLDI'97, pages 226--236, 1997.

# [Larchey07] D. Larchey-Wendling. Graph-based decision for Goedel-Dummett logics. Journal of Automated Reasoning, 38:201--225, 2007.

# [Larchey&Mery&Galmiche01] D. Larchey-Wendling and D. Méry and D. Galmiche. STRIP: Structural Sharing for Efficient Proof-search. In IJCAR'01, pages 696--700, vol. 2083 of LNCS, 2001.

# [Larchey&Galmiche09] D. Larchey-Wendling and D. Galmiche. Exploring the Relation between Intuitionistic BI and Classical BI: An unexpected Embedding. Mathematical Structures in Computer Science, vol. 19, pp 435 - 500, 2009

# [Larchey&Galmiche10] D. Larchey-Wendling and D. Galmiche. The Undecidability of Boolean BI through Phase Semantics. In 25th Annual {IEEE} Symposium on Logic in Computer Science, LICS 2010, p. 147-156, Edinburgh, UK, July 2010.

# [Larchey08] D. Larchey-Wendling. Kripke Models of Boolean BI and Invertible resources. Domains IX International Workshop, Brighton, UK, 2008.

# [Larchey10] D. Larchey-Wendling. An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics. Mathematical Foundations of Programming Semantics, MFPS 2010, ENTCS 265, p. 369 - 387, 2010.

# [LevAmi&Sagiv00] T. Lev-Ami and M. Sagiv. TVLA: A System for Implementing Static Analyses. In SAS'00, pages 280--301, 2000.

# [Lisitsa&Potapov05] A. Lisitsa and I. Potapov. Temporal logic with predicate lambda-abstraction. In TIME'05, 147--155, IEEE, 2005.

# [Loding&Rohde03] Ch. Loding and Ph. Rohde. Model Checking and Satisfiability for Sabotage Modal Logic. In FST&TCS'03, pages 302—313, vol. 2914 of LNCS, 2003.

# [Lozes04] E. Lozes. Separation logic preserves the expressive power of classical logic. In 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE'04), 2004.

# [Magill-etal07] S. Magill, J. Berdine, E. Clarke, B. Cook. Arithmetic strengthening for shape analysis. In SAS'07, LNCS 4634, pp. 419--436. Springer, 2007.

# [McCusker&Pym07] A Games Model of Bunched Implications. In CSL '07, LNCS 4646, pp 573-588, 2007.

# [Nelson&Oppen80] G. Nelson and D. Oppen.Fast decision procedures based on congruence closure. Journal of ACM, 27(2):356--364, 1980.

# [Neven&Schwentick&Vianu04] F. Neven and T. Schwentick and V. Vianu. Finite State Machines for Strings Over Infinite Alphabets. TOCL 5(3) :403—435, 2004.

# [OHearn&Pym99] P.W. O'Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215--244, 1999.

# [OHearn&Reynolds&Yang01] P. O'Hearn, J. Reynolds, H.Yang. Local reasoning about programs that alter data structures. In CSL'01, LNCS 2142, pp. 1--19, Springer, 2001.

# [OHearn&Pym&Yang04] P. O'Hearn and H. Yang and D. Pym. Possible worlds and resources: The semantics of BI. In Theoretical Computer Science, 315(1):257--305, 2004.

# [Oppen80] D. Oppen. Reasoning about recursively defined data structures. Journal of ACM, 27(3):403--411, 1980.

# [Pnueli77] A. Pnueli. The temporal logic of programs. FOCS'77, pages 46—57, 1977, IEEE.

# [Pym02] D. Pym. The semantics and proof theory of the logic of bunched implications. Kluwer Academic Publishers, 2002.

# [Pym&Tofts06] D. Pym and C. Tofts. A calculus and logic of resources and processes. Formal Aspects of Computing, 18:495--517, 2006.

# [Pym&Tofts07] D. Pym and C. Tofts. Systems modelling via resources and processes: Philosophy, calculus, semantics, and logic. ENTCS, 172:545--587, 2007.

# [Reynolds00] J. Reynolds, Intuitionistic Reasoning about Shared Mutable Data Structures. In J. Davies, D. Roscoe, and J. Woodcock, editors, Millennial Perspectives in Computer Science, pages 303--321, Houndsmill, Hampshire, 2000. Palgrave.

# [Reynolds02] J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, pages 55--74, IEEE, 2002.

# [Rugina04] R. Rugina. Quantitative shape analysis. In SAS'04, LNCS 3148, pp. 228--245, Springer, 2004.

# [Sagiv&Reps&Wilhelm02] M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, 24(3):217--298, 2002.

# [van Benthem&Liu07] J. van Benthem and F. Liu. Dynamic logic of preference upgrade. Journal of Applied Non-Classical Logics, 17:157--182, 2007.

# [van Benthem&vanEijk&Kooi06] J. van Benthem, J. van Eijck B. Kooi. Logics of communication and change. Information and Computation, 204:1620--1662, 2006.

# [van Ditmarsch&van der Hoek&Kooi07] H.P. van Ditmarsch, W. van der Hoek & B.P. Kooi, Dynamic Epistemic Logic. Synthese Library volume 337. Springer, 2007.

# [van Ditmarsch&Herzig07] Belief revision and dynamic logic. Journal of Applied Non-Classical Logics, Vol. 17 , n. 2, 2007.

# [van Ditmarsch&Herzig&deLima10] From Situation Calculus to Dynamic Logic. Journal of Logic and Computation, 2010 (to appear).

# [Vardi&Wolper94] M. Vardi and P. Wolper. Reasoning about Infinite Computations. Information and Computation 115:1--37, 1994.

# [Weber04] T. Weber. Towards mechanized program verification with separation logic. In CSL'04, LNCS 3210, pp. 250--264, Springer, 2004.

# [Yahav et al03] E. Yahav and Th. Reps and M. Sagiv and R. Wilhelm. Verifying temporal heap properties specified via evolution logic. ESOP’03, pages 204—222, vol. 2618, LNCS, Springer, 2003.

# [Yavuz-Kahveci&Bultan02] T. Yavuz-Kahveci and T. Bultan. Automated verification of concurrent linked lists with counters. In SAS'02, LNCS 2477, pp. 69--84. Springer, 2002.

# [Zhang&Sipma&Manna04] T. Zhang, H. Sipma, and Z. Manna. Decision procedures for recursive data structures with integer constraints. In IJCAR'04, LNCS 3097, pp. 152--167, Springer, 2004.

# [Biri&Galmiche03] N. Biri and D. Galmiche. A Separation Logic for Resource Distribution --extended abstract--. In FST&TCS'03, pages 23--37, vol. 2914 of LNCS, 2003.

# [Biri&Galmiche07] N. Biri and D. Galmiche. Models and Separation Logics for Resource Trees. Journal of Logic and Computation, 17(4):687--726, 2007.

# [Blackburn&deRijke&Venema01] P. Blackburn, M. de Rijke, Y. Venema. Modal logic, Cambridge University Press, New York, NY, USA, 2001.

# [Bojanczyketal09] M. Bojanczyk and A. Muscholl and Th. Schwentick and L. Segoufin. Two-variable Logic on Data Trees and XML Reasoning. JACM 56(3), 2009.

# [Bouajjani-etal05] A. Bouajjani and P. Habermehl and P. Moro and T. Vojnar. Verifying programs with dynamic 1-selector-linked structured in regular model-checking. In TACAS'05, pages 13--29, vol. 3440 of LNCS, 2005.

# [Bouajjani-etal06] A. Bouajjani, P. Habermehl, A. Rogalewicz, T. Vojnar. Abstract Regular Tree Model Checking. Electr. Notes Theor. Comput. Sci. 149(1): 37-48, 2006.

# [Bozga&Iosif&Lakhnech04] M. Bozga and R. Iosif and Y. Lakhnech. On logics of aliasing. In SAS'04, pages 344--360, vol. 3148 of LNCS, 2004.

# [Brochenin&Demri&Lozes07] R. Brochenin and S. Demri and E. Lozes. Reasoning about sequences of memory states. LFCS’07, LNCS 4514, pp. 100--114, Springer, 2007.

# [Brochenin&Demri&Lozes08] R. Brochenin and S. Demri and E. Lozes. On the almighty wand. In CSL'08, LNCS 5213, pages 322--337, Springer, 2008.

# [Brochenin&Demri&Lozes09] R. Brochenin, S. Demri and E. Lozes. Reasoning about sequences of memory states. Annals of Pure and Applied Logics 161(3): 305--323, 2009.

# [Brotherston&Kanovich10] J. Brotherston and M. Kanovich. Undecidability of propositional separation logic and its neighbours. In 25th Annual IEEE} Symposium on Logic in Computer Science, LICS 2010, pages 137--146, Edinburgh, UK, July 2010.

# [Burkart et al01] O. Burkart and D. Caucal and F. Moller and B. Steffen. Verification of infinite structures. In Handbook of Process Algebra, pages 545—623, Elsevier, 2001.

# [Caires&Cardelli03] L. Caires and L. Cardelli. A Spatial logic for concurrency (part I). Information and Computation 186(2) :194—235, 2003.

# [Caires&Lozes06] L. Caires and E. Lozes. Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency.Theoretical Computer Science 358(2--3):293--314, 2006.

# [Caires&Vieira06] L. Caires and H. T. Vieira. Extensionality of Spatial Observations in Distributed Systems. In EXPRESS'06, ENTCS, 2006.

# [Calcagno&Yang&OHearn01] C. Calcagno and H. Yang and P. O'Hearn. Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In FST&TCS'01, pages 108--119, vol. 2245 of LNCS, 2001.

# [Calcagno&Yang&OHearn01b] C. Calcagno, H. Yang, and P. O'Hearn. Computability and complexity results for a spatial assertion language. In APLAS'01, pages 289--300, 2001.

# [Calcagno&Gardner&Hague05] C. Calcagno and Ph. Gardner and M. Hague. From separation logic to first-order logic. In FOSSACS'05, pages 395--409, vol. 3441 of LNCS, 2005.

# [Calcagno&Gardner&Zarfaty05] C. Calcagno and Ph. Gardner and U. Zarfaty. Context Logic and Tree Update. In the 32nd Annual Symposium on Principles of Programming Languages, POPL'05, pages 259—270, 2005.

# [Calcagno&Gardner&Zarfaty07] C. Calcagno and Ph. Gardner and U. Zarfaty. Context Logic as Modal Logic: Completeness and Parametric Inexpressivity. In 34th Annual Symposium on Principles of Programming Languages, POPL'07, 2007.

# [Cardelli&Gordon00] L. Cardelli and A. D. Gordon. Mobile Ambients, Theoretical Computer Science 240(1):177--213, 2000.

# [Cardelli&Ghelli04] L. Cardelli and G. Ghelli. TQL: A Query Language for Semistructured Data Based on the Ambient Logic. Mathematical structures in Computer Science 14(3) : 285—327, 2004.

# [Cardelli&Gardner&Ghelli02] L. Cardelli, Ph. Gardner, G. Ghelli. A spatial logic for querying graphs. In ICALP'02, LNCS 2380, pp. 597--610, 2002.

# [Conforti&Macedonio&Sassone05a] G. Conforti and D. Macedonio and V. Sassone. Spatial logics for bigraphs. In ICALP'05, pages 766--778, vol. 3580 of LNCS, 2005.

# [Conforti&Macedonio&Sassone05b] G. Conforti and D. Macedonio and V. Sassone. Bigraphical Logics for XML. In Italian Symposium on Advanced Database Systems, SEBD'05, pages 392--399, 2005.

# [Dawar&Gardner&Ghelli04] A. Dawar, P. Gardner and G. Ghelli. Adjunct elimination through games in static ambient logic. FST\&TCS’04, pages 211-223, vol. 3328, LNCS, Springer, 2004.

[Galmiche&Salhi08] D. Galmiche and Y. Salhi. Calculi for an intuitionistic hybrid modal logic. In Int Workshop on Intuitionistic Modal Logic and Applications, IMLA'08, 2008.

# [Balbiani etal.08] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi, and T. De Lima. "knowable" as "known after an announcement". To appear, 2008.

# [Balbiani&Echahed&Herzig10] A modal Logic for Termgraph Rewriting. International Conference on Graph Transformation (ICGT 2010), Twente, LNCS 6372, p. 59-74, 2010.

# [Berdine&Calcagno&OHearn04] J. Berdine, C. Calcagno, and P. O'Hearn. A decidable fragment of separation logic. In FSTTCS'04, LNCS 3328, pp. 97--109, Springer, 2004..

# [Berdine&Calcagno&OHearn05] J. Berdine and C. Calcagno and P. W. O'Hearn. Symbolic execution with separation logic. In APLAS'05, pages 52--68, vol. 3780 of LNCS, 2005.

# [Berdine&Calcagno&OHearn05] J. Berdine, C. Calcagno, and P. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO'05, LNCS 4111, pp. 115--137, Springer, 2005.

# [Berdine-etal06] J. Berdine, B. Cook, D. Distefano, and P. O'Hearn. Automatic termination proof for programs with shape-shifting heaps. In CAV'06, LNCS 4144, pp. 386--400, 2006.

# [Aucher-etal09] G. Aucher and Ph. Balbiani and L. Fariñas del Cerro and A. Herzig. Global and Local Graph Modifiers. ENTCS 231: 293-307, 2009.

# [Balbiani&Condotta02] Ph. Balbiani and J.F. Condotta. Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In FroCoS'02, LNAI 2309, pp. 162--173, Springer 2002.

# [Balbiani etal.10] Tableaux for public announcement logics. Journal of Logic and Computation, Special Issue on Tableaux and Analytic Proof Methods, Vol. 20, n. 1, p. 55-76, 2010.

# [Balbiani&Cheikh&Feuillade09] Ph. Balbiani, F. Cheikh, G. Feuillade. Algorithms and Complexity of Automata Synthesis by Asynchronous Orchestration With Applications to Web Services Composition. ENTCS 229(3): 3-18 (2009).

# [Baltag and Moss04] A. Baltag and L. Moss. Logics for epistemic programs. Synthese, 139(2):165–224, 2004.

# [Baltag&Smets08] A. Baltag and S. Smets. Probabilistic dynamic belief revision. Synthese 165 (2): 179-202 (2008)

# [Bansal&Brochenin&Lozes09] K. Bansal and R. Brochenin and E. Lozes. Beyond Shapes: Lists with Ordered Data. In FOSSACS'09, LNCS 5504, pp. 425--439, Springer 2009.

# [Berard-etal01] B. Bérard and M. Bidoit and A. Finkel and F. Laroussinie and A. Petit and L. Petrucci and Ph. Schnoebelen. Systems and Software Verification, Model-Checking Techniques and Tools, Springer, 2001.