@article{OrejasPinoNavarroetal.2018,
  author    = {Orejas, Fernando and Pino, Elvira and Navarro, Marisa and Lambers, Leen},
  title     = {Institutions for navigational logics for graphical structures},
  series = {Theoretical computer science},
  volume    = {741},
  journal   = {Theoretical computer science},
  publisher = {Elsevier},
  address   = {Amsterdam},
  issn      = {0304-3975},
  doi       = {10.1016/j.tcs.2018.02.031},
  pages     = {19 -- 24},
  year      = {2018},
  abstract  = {We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex.},
  language  = {en}
}
@article{NavarroOrejasPinoetal.2021,
  author    = {Navarro, Marisa and Orejas, Fernando and Pino, Elvira and Lambers, Leen},
  title     = {A navigational logic for reasoning about graph properties},
  series = {Journal of logical and algebraic methods in programming},
  volume    = {118},
  journal   = {Journal of logical and algebraic methods in programming},
  publisher = {Elsevier Science},
  address   = {Amsterdam [u.a.]},
  issn      = {2352-2208},
  doi       = {10.1016/j.jlamp.2020.100616},
  pages     = {33},
  year      = {2021},
  abstract  = {Graphs play an important role in many areas of Computer Science. In particular, our work is motivated by model-driven software development and by graph databases. For this reason, it is very important to have the means to express and to reason about the properties that a given graph may satisfy. With this aim, in this paper we present a visual logic that allows us to describe graph properties, including navigational properties, i.e., properties about the paths in a graph. The logic is equipped with a deductive tableau method that we have proved to be sound and complete.},
  language  = {en}
}