Research by Marisa Navarro

Member of  LoRea group

My research interests are:        

• Graph Transformation and Logics for Graphical Structures
• Temporal Logical Systems and Resolution.
• Modularity and Verification. Learning.
• Functional and Logic Programming. 
• Formal Specification and Semantics of Programming Languages. 

Projects

I am now involved in the projects:

"Modelos y Métodos basados en Grafos para la Computación en gran escala (GRAMM)"

Entidad Financiadora: MINECO (Ref. TIN2017-86727-C2-2-R)

Duración:  3 años (1/1/2018-31/12/2020)

Investigador principal del proyecto coordinado:  Fernando Orejas Valdés (Univ. Politécnica Cataluña) y del subproyecto 2: Paqui Lucio Carrasco

Investigadores participantes de la UPV-EHU: 4

"Modelos y Métodos Computacionales para Datos Masivos Estructurados (COMMAS)"

Entidad Financiadora: MINECO (Ref. TIN2013-46181-C2-2-R)

Duración:  4 años (1/1/2014-31/12/2017)

Investigador principal del proyecto coordinado:  Fernando Orejas Valdés (Univ. Politécnica Cataluña) y del subproyecto 2: Paqui Lucio Carrasco

Investigadores participantes de la UPV-EHU: 6

"Logic and Reasoning (LoRea)"

Entidad financiadora: UPV-EHU (Ref. GIU15/30)

Duración:  3 años (1/12/2015 - 30/11/2018)

Investigador responsable:  Paqui Lucio Carrasco 

Número de investigadores participantes:  6

"Basque Advanced Informatics Laboratory (BAILab)"

Entidad financiadora: UPV-EHU (Ref. UFI11/45)

Duración:  5 años (1/1/2012 - 31/12/2016)

Investigador responsable:  Agustín Arruabarrena Santos

Número de investigadores participantes:  87 (de 5 grupos de investigación de la UPV/EHU)

Conferences, Journals and Book Chapters 

• "Institutions for Navigational Logics for Graphical Structures"

           Fernando Orejas, Elvira Pino, Marisa Navarro, Leen Lambers.

           Theoretical Computer Science. Volume 741, pp. 19-24, September 2018.

            (DOI: 10.1016/j.tcs.2018.02.031)

• "Towards a Navigational Logic for Graphical Structures"

           Leen Lambers, Marisa Navarro, Fernando Orejas, Elvira Pino.

           In: Reiko Heckel, Gabriele Taentzer (eds) Graph Transformation, Specifications, and Nets: In Memory of Hartmut Ehrig.

           Publicado en Springer Lecture Notes in Computer Science 10800, pp 124-141, 2018.

          (DOI: 10.1007/978-3-319-75396-6_7;  Print ISBN: 978-3-319-75395-9 Online ISBN: 978-3-319-75396-6)

• "A Logic of Graph Conditions Extended with Paths"

           Marisa Navarro, Fernando Orejas, Elvira Pino, Leen Lambers.

           - Presentación en GCM 2016 (7th Int. Workshop on Graph Computation Models, Vienna, Austria, 4 July 2016).

             Pre-Proccedings: http://gcm2016.inf.uni-due.de/pre-proceedings.html          

           - Presentación en PROLE 2016 (XVI Jornadas sobre Programación y Lenguajes, Salamanca, 13-16 September 2016)

• Editora de las actas formales de PROLE 2015 en EPTCS (Electronic Proceedings in Theoretical Computer Science):

  EPTCS 200. Proceedings XV Jornadas sobre Programación y Lenguajes Santander, Spain, 15-17th September 2015.

  Edited by: Marisa Navarro.

  Published: 19th December 2015.

  (DOI: 10.4204/EPTCS.200;  ISSN: 2075-2180)

   

• "On graphical logics for reasoning about graph properties"

          Leen Lambers, Marisa Navarro, Fernando Orejas, Elvira Pino.
           Presentación en Dagstuhl Seminar on Verification of Evolving Graph Structures, Report 15451, p.16.

           Fecha de presentación: 4/11/2015.

• "Satisfiability of Constraint Specifications on XML Documents"

   Marisa Navarro, Fernando Orejas, Elvira Pino.

  - Presentación en las Jornadas sobre Programación y Lenguajes PROLE 2015, Santander, 16/9/2015 y

    en el Festschrift Symposium in Honor of José Meseguer, Urbana, IIlinois, USA, 23-25/9/2015.

  - Publicado en el libro "Logic, Rewriting, and Concurrency" by Springer Verlag in Lecture Notes in Computer Science 9200, pp 539-561, 2015.

  (DOI: 10.1007/978-3-319-23165-5_25; Print ISBN: 978-3-319-23164-8; Online ISBN: 978-3-319-23165-5).

   

• "SpecSatisfiabilityTool: A tool for testing the satisfiability of specifications on XML documents"

   Javier Albors, Marisa Navarro.
   XIV Jornadas sobre Programación y Lenguajes, Cádiz, Spain (September 16-19, 2014).

   Publicado en EPTCS (Electronic Proceedings in Theoretical Computer Science) nº 173, pp 27-40, 2015.

   http://arxiv.org/html/1501.01693    (DOI: 10.4204/EPTCS.173.3)

   

• "A refutation procedure for proving satisfiability of constraint specifications on XML documents"

            Marisa Navarro, Fernando Orejas.
            Presentado en SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science. Gammarth, La Marsa, Tunisia (December 7-8, 2014).
            Publicado en EasyChair Proceedings in Computing (EPiC) Series, nº 30, pp 47-61, 2014.

            http://www.easychair.org/publications/?page=862275542   (ISSN: 2040-557X)

• "Invariant-Free Clausal Temporal Resolution"

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, F. Orejas.

Journal of Automated Reasoning. Volume 50, issue 1, pp. 1-49, January 2013.

(DOI: 10.1007/s10817-011-9241-2)     [Electronic Edition]

• "Semantics of Structured Normal Logic Programs”

E. Pasarella, F. Orejas, E. Pino, M. Navarro.

The Journal of Logic and Algebraic Programming. Volume 81, issue 5, pp 559-584, July 2012

http://dx.doi.org/10.1016/j.jlap.2012.03.001

• "Proving Satisfiability of Constraint Specifications on XML Documents"

M. Navarro, F. Orejas. 

Actas de las X Jornadas sobre Programación y Lenguajes PROLE’2010 (Valencia, September 2010), 

published by Editorial Garceta.

• "Translating propositional extended conjunctions of Horn clauses into Boolean Circuits"

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro. 

Theoretical Computer Science. Volume 411, Issues 16-18, pp. 1723-1733 (2010).

• "Dual Systems of Tableaux and Sequents for PLTL"

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, F. Orejas. 

The Journal of Logic and Algebraic Programming. Volume 78, issue 8 (November 2009), pp 701-722.

http://dx.doi.org/10.1016/j.jlap.2009.05.001

• "Invariant-Free Clausal Temporal Resolution"

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, F. Orejas. 

Contributed Talk in Workshop on Modal Fixpoint Logics, Amsterdam, March 25-27, 2008.

Technical Report UPV-EHU-LSI-TR-11-2008.

• "Systematic Semantic Tableaux for PLTL"

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro. 

Actas de las VII Jornadas sobre Programación y Lenguajes PROLE’2007 (Zaragoza, September 2007), 

published by Thomson Paraninfo, pp. 1-10, 2007  (ISBN: 978-84-9732-599-8)

Published as Revised Selected Paper in E.N.T.C.S. 206, pp. 59-73, 2008.

• "A Cut-Free and Invariant-Free Sequent Calculus for PLTL"

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, Fernando Orejas. 

Presentation in CSL 2007 ( Computer Science Logic: 21 International Workshop, 16th Annual Conference of the EACSL),

Lausanne, Switzerland, September 11-15, 2007.

• "A Transformational Semantics of Static Embedded Implications"

Edelmira Pasarella, Fernando Orejas, Elvira Pino, Marisa Navarro. 

Presentation in LOPSTR'05 (International Symposium on Logic-based Program Synthesis and Transformation), London, UK, September 7 - 9, 2005.

• "Classifying the problem of Learning Extended Horn Clauses"
  J. Gaintzarain, M. Hermo, M. Navarro.
  Actas de las V Jornadas sobre Programación y Lenguajes PROLE 2005 (Simposio 10 del I Congreso Español de Informática - CEDI 2005)
  Published by Thomson Paraninfo, pp. 205-210, 2005  (ISBN: 84-9732-438-2)

• "Goals in the Propositional Horn^ Language are Monotone Boolean Circuits"

J. Gaintzarain, M. Hermo, M. Navarro.

Presentation in MFCS 2005, August 29 - September 2, Gdansk, Poland.

Published by Springer Verlag in Lecture Notes in Computer Science  3618, (2005) pp. 376-386. ©Springer-Verlag LNCS.

• “On Learning Conjunctions of Horn^ Clauses”

J. Gaintzarain, M. Hermo, M. Navarro.

Contributed paper in `CIE 2005: New Computational Paradigms´, Amsterdam, June 8-12, 2005.

•  "From Modular Horn Programs to Flat Ones: a Formal Proof for the Propositional Case”.

Navarro, M.

In Proc. ISIICT’2004, April 2004, Amman (Jordan). 

Technical Report UPV-EHU/ LSI/ TR 01-2004.

•  “A Strong Logic Programming View for Static Embedded Implications”

Arruabarrena, R., Lucio, P., Navarro, M.

      In: ‘Foundations of Software Science and Computation Structures’,

      Springer Verlag Lecture Notes in Computer Science  1578, (1999) pp. 56-72. ©Springer-Verlag LNCS.

• "Algebraic Implementation of Abstract Data Types: a Survey of Concepts and New Compositionality Results"

Orejas, F., Navarro, M., Sánchez, A

Mathematical Structures in Computer Science 6, (1996) pp. 33- 67. ©Cambridge University Press.

• "On the Correctness of Modular Systems"

Navarro,  M., Orejas, F., Sánchez, A.

Theoretical Computer Science 140, 1 (March 1995), pp. 139-178. ©Elsevier Science Inc.

• "Implementation and Behavioural Equivalence: a Survey"

            Orejas, F., Navarro, M., Sánchez, A.

      In: ‘Recent Trends in Data Type Specification’ (M. Bidoit, C. Choppy, eds.), 

      Springer Verlag Lecture Notes in Computer Science 655, (1993), pp. 93–125. ©Springer-Verlag LNCS.

• "Contextual rewriting as a sound and complete proof method for conditional LOG-specifications"

Navarro, M., Orejas, F., Remy,  J.L.

Acta Informatica 30, (1993), pp. 147-180. ©Springer-Verlag.

• "Characterizing Confusion"

Navarro,  M., Orejas, F., Sánchez, A.

The Algebraic Specification Column, Bulletin of the EATCS, 49, (Feb. 1993), pp.104–109.

• "On the Correctness of Modular Systems"

Navarro,  M., Orejas, F., Sánchez, A.

AMAST 93, M. Nivat, C. Rattray, T. Rus and G. Scollo (eds) Springer Workshops in Computing (1993), 211-218. ©Springer-Verlag.

• "Term rewriting methods for partial specifications"

Orejas F., Sánchez A., Navarro M., Nivela P., Peña R.

Procc. of  6th Workshop on Specification of Abstract Data Types. Berlin 1988.

• "Parameterized Horn clause specifications: proof theory and correctness"

Navarro, M.; Orejas, F.

Theory and Practice of Software Development-TAPSOFT’87. Springer-Verlag Lecture Notes in Computer Science 249,(1987) pp.202-216.

• "On contextual rewriting"

Navarro, M.; Orejas, F.

Journes LANFOR. Ed. AFCET, pp. 123-135. 1986.

• "A proof-theoretical characterization of persistency for parameterized (conditional) specifications with boolean constraints"

Navarro, M.; Orejas, F.

Procc. of  4th Workshop on Specifications of Abstract Data Types. Burg Warberg (Alemania) 1986.

• "On the equivalence of hierarchical and non-hierarchical rewriting in conditional term rewriting systems"

Navarro, M.; Orejas, F.

Int. Symp. on Symbolic and Algebraic Computation-EUROSAM'84. Springer-Verlag Lecture Notes in Computer Science 174, (1984) pp.74-85.

Back to Marisa Navarro’s Home Page