Research by Marisa Navarro

Member of  LoRea group

My research interests are:        

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

Projects

I am now involved in the project:

"Métodos formales y algoritmos para el diseño de sistemas (FORMALISM)"

Entidad Financiadora: CICYT (Ref. TIN2007-66523)

Duración:  5 años + 1 año prórroga (2008/20013)

Investigador principal:  Fernando Orejas Valdés (Univ. Politécnica Cataluña)

Número de investigadores participantes:  29

Three previous proyects I was involved in:

"Logic and Reasoning"

Entidad financiadora: UPV-EHU (Ref. GIU07/35)

Duración:  3 años (12-05-2008  a 11-05-2011)

Investigador responsable:  Francisca Lucio Carrasco  

Número de investigadores participantes:  5

Participación como investigador del Subproyecto 03, en el proyecto coordinado:

“Métodos basados en Grafos para el Modelado, Análisis y Realización de Sistemas de gran tamaño (GRAMMARS)” 

Entidad Financiadora: CICYT (Ref. TIN2004-07925-C03-03). Años: 2005, 2006 y 2007

Investigador responsable del proyecto coordinado:  Fernando Orejas Valdés (Univ. Politécnica Cataluña)

Participación como investigador responsable del Subproyecto 03, en el proyecto coordinado:

"Modelización, Análisis y Verificación de Sistemas Heterogéneos (MAVERISH)"

Entidad Financiadora: CICYT (Ref. TIC2001-2476-C03-03). Años: 2002, 2003 y 2004

Investigador responsable del proyecto coordinado:  Fernando Orejas Valdés (Univ. Politécnica Cataluña)

Conferences, Journals and Book Chapters 

• "Semantics of Structured Normal Logic Programs”

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

To appear (in 2012) in Journal of Logic and Algebraic Programming.

• "Invariant-Free Clausal Temporal Resolution"

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

To appear (in 2012) in Journal of Automated Reasoning (Online from December 2th, 2011)

doi: 10.1007/s10817-011-9241-2

[Electronic Edition]

• "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 and M. Navarro. 

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

• "Dual Systems of Tableaux and Sequents for PLTL"

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

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, and 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 and 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 and 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