Julia Sapiña

Julia Sapiña

Assistant Professor·Researcher in Computer Science

Departament de Sistemes Informàtics i Computació (DSIC)
ELP · VRAIN · Universitat Politècnica de València
Camí de Vera s/n, 46022 València, Spain

GitHub
Journal articles
13
Conference papers
15
Tools released
12
Sexenios
2

About

I'm a researcher in Computer Science working with the Extensions of Logic Programming (ELP) research group, part of the Valencian Research Institute for Artificial Intelligence (VRAIN) at the Universitat Politècnica de València.

After my degree in 2012, I joined the ELP, where I have had the pleasure of working with great researchers such as María Alpuente, Demis Ballis, Francisco Frechina, and Santiago Escobar.

In December 2017, I successfully defended my Ph.D. dissertation, focused on the formal development of rewriting-based techniques for (Maude) program analysis and debugging.

During my postdoctoral stage, I also had the opportunity to collaborate with Francisco Durán, from the Universidad de Málaga (UMA); José Meseguer, from the University of Illinois at Urbana-Champaign (UIUC); and Kyungmin Bae, from Pohang University of Science and Technology (POSTECH). You can take a look at our joint work in the Publications section of this page.

I currently work as an Assistant Professor at the Department of Computer Systems and Computation (DSIC), Universitat Politècnica de València, and hold two six-year research periods (sexenios de investigación) granted by ANECA, covering 2014–2019 and 2020–2025.

Research Interests

Maude Rewriting Logic Narrowing Unification Generalization Theorem Proving Formal Methods for Security Protocol Analysis and Verification Intruder Models Privacy

Publications

Journal Papers

  • [j13]

    DM-Check: Verifying invariants of concurrent systems by deductive model checking.

    K. Bae, S. Escobar, R. López-Rueda, J. Meseguer, J. Sapiña.

    Journal of Logical and Algebraic Methods in Programming (JLAMP), vol. 149, pp. 101107. Elsevier, 2026. PDF

  • [j12]

    Safety enforcement via programmable strategies in Maude.

    M. Alpuente, D. Ballis, S. Escobar, D. Galán, J. Sapiña.

    Journal of Logical and Algebraic Methods in Programming (JLAMP), vol. 132, pp. 100849. Elsevier, 2023. PDF

  • [j11]

    An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis.

    R. López-Rueda, S. Escobar, J. Sapiña.

    Journal of Logical and Algebraic Methods in Programming (JLAMP), vol. 135, pp. 100895. Elsevier, 2023. PDF

  • [j10]

    Order-sorted equational generalization algorithm revisited.

    M. Alpuente, S. Escobar, J. Meseguer, J. Sapiña.

    Annals of Mathematics and Artificial Intelligence, vol. 90, pp. 499–522. Springer, 2022. PDF

  • [j9]

    Optimization of rewrite theories by equational partial evaluation.

    M. Alpuente, D. Ballis, S. Escobar, J. Sapiña.

    Journal of Logical and Algebraic Methods in Programming (JLAMP), vol. 124, pp. 100729. Elsevier, 2022. PDF

  • [j8]

    Symbolic Specialization of Rewriting Logic Theories with Presto.

    M. Alpuente, D. Ballis, S. Escobar, J. Sapiña.

    Theory and Practice of Logic Programming (TPLP), vol. 22, pp. 444–495. Cambridge University Press, 2022. PDF

  • [j7]

    Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME System.

    M. Alpuente, D. Ballis, J. Sapiña.

    Mathematics in Computer Science, vol. 14, pp. 591–606. Springer, 2020. PDF

  • [j6]

    Static Correction of Maude Programs with Assertions.

    M. Alpuente, D. Ballis, and J. Sapiña.

    Journal of Systems and Software (JSS), vol. 153, pp. 64–85. Elsevier, 2019. PDF

  • [j5]

    Symbolic Analysis of Maude Theories with Narval.

    M. Alpuente, D. Ballis, S. Escobar, and J. Sapiña.

    Theory and Practice of Logic Programming (TPLP), vol. 19, issue 5–6, pp. 874–890. Cambridge University Press, 2019. PDF

  • [j4]

    Inspecting Maude Variants with GLINTS.

    M. Alpuente, A. Cuenca-Ortega, S. Escobar, and J. Sapiña.

    Theory and Practice of Logic Programming (TPLP), vol. 17, issue 5–6, pp. 689–707. Cambridge University Press, 2017. PDF

  • [j3]

    Debugging Maude Programs via Runtime Assertion Checking and Trace Slicing.

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    Journal of Logical and Algebraic Methods in Programming (JLAMP), Special Issue on Automated Verification of Programs and Web Systems, vol. 85, issue 5, pp. 707–736. Elsevier, 2016. PDF

  • [j2]

    Assertion-based Analysis via Slicing with ABETS.

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    Theory and Practice of Logic Programming (TPLP), vol. 16, issue 5–6, pp. 515–532. Cambridge University Press, 2016. PDF

  • [j1]

    Exploring Conditional Rewriting Logic Computations.

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    Journal of Symbolic Computation (JSC), Special Issue on Symbolic Computation in Software Science, vol. 69, pp. 3–39. Elsevier, 2015. PDF

Conference Papers

  • [c15]

    NuITP: An Inductive Theorem Prover for Equational Program Verification.

    F. J. Durán, S. Escobar, J. Meseguer, J. Sapiña.

    In Proc. of the 26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024), 2024. PDF

  • [c14]

    Verifying Invariants by Deductive Model Checking.

    K. Bae, S. Escobar, R. López-Rueda, J. Meseguer, J. Sapiña.

    In Proc. of the 15th International Workshop on Rewriting Logic and its Applications (WRLA 2024), 2024. PDF

  • [c13]

    Optimizing Maude Programs via Program Specialization.

    M. Alpuente, D. Ballis, S. Escobar, J. Meseguer, J. Sapiña.

    In Proc. of Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, 2023. PDF

  • [c12]

    Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints.

    S. Escobar, R. López-Rueda, J. Sapiña.

    In Proc. of the 9th ACM International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2023), 2023. PDF

  • [c11]

    Variant-Based Equational Anti-unification.

    M. Alpuente, D. Ballis, S. Escobar, J. Sapiña.

    In Proc. of the 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2022), 2022. PDF

  • [c10]

    Protocol Analysis with Time and Space.

    D. Aparicio-Sánchez, S. Escobar, C. Meadows, J. Meseguer, J. Sapiña.

    In Proc. of Protocols, Strands, and Logic, 2021. PDF

  • [c9]

    An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA.

    D. Aparicio-Sánchez, S. Escobar, R. Gutiérrez, J. Sapiña.

    In Proc. of the 25th European Symposium on Research in Computer Security (ESORICS 2020), 2020. PDF

  • [c8]

    Protocol Analysis with Time.

    D. Aparicio-Sánchez, S. Escobar, C. Meadows, J. Meseguer, J. Sapiña.

    In Proc. of the 21st International Conference on Cryptology in India (INDOCRYPT 2020), 2020. PDF

  • [c7]

    Variant-based Equational Unification under Constructor Symbols.

    D. Aparicio-Sánchez, S. Escobar, J. Sapiña.

    In Proc. of the 36th International Conference on Logic Programming (ICLP 2020), 2020. PDF

  • [c6]

    Most General Variant Unifiers.

    S. Escobar and J. Sapiña.

    Technical Communications of the 35th International Conference on Logic Programming (ICLP 2019), 2019. PDF

  • [c5]

    Inferring Safe Maude Programs with ÁTAME.

    M. Alpuente, D. Ballis, and J. Sapiña.

    In Proc. of the 6th International Congress on Mathematical Software (ICMS 2018), 2018. PDF

  • [c4]

    Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis.

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    In Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer (LRC 2015), LNCS vol. 9200, pp. 72–96. Springer-Verlag, 2015. PDF

  • [c3]

    Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way).

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    In Specification, Algebra, and Software: A Festschrift Symposium in Honor of Kokichi Futatsugi (SAS 2014), LNCS vol. 8373, pp. 229–255. Springer-Verlag, 2014. PDF

  • [c2]

    Parametric Exploration of Rewriting Logic Computations.

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    In Proc. of the 5th International Symposium on Symbolic Computation in Software Science (SCSS 2013), EPiC vol. 15, pp. 4–18. EasyChair, 2013. PDF

  • [c1]

    Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJulienne.

    M. Alpuente, D. Ballis, F. Frechina, and J. Sapiña.

    In Proc. of the 22nd European Symposium on Programming (ESOP 2013), LNCS vol. 7792, pp. 121–124. Springer-Verlag, 2013. PDF

* authoring in alphabetical order

Informal Publications

  • [i4]

    Rewriting Logic Techniques for Program Analysis and Optimization.

    J. Sapiña.

    1st Doctoral Consortium of SISTEDES 2014 Conferences, 2014. PDF

  • [i3]

    Rewriting Logic Techniques for Program Analysis and Optimization.

    J. Sapiña.

    1st Doctoral School Meeting of Ph.D. Students of the Universitat Politècnica de València, 2014. (Scientific Poster) PDF

  • [i2]

    Slicing Slices. An Incremental Backward Trace Slicing Methodology for RWL Computations.

    J. Sapiña.

    Master's Thesis in Software Engineering, Formal Methods and Information Systems, Universitat Politècnica de València, 2013.

  • [i1]

    A Conditional Slicing Tool for Maude.

    J. Sapiña.

    Final Year Project in Computer Science Engineering, Universitat Politècnica de València, 2012. PDF

Software & Tools

NuITP

2023

Interactive theorem prover that helps users construct, check, and manage proofs of properties of Maude specifications through a guided, step-by-step deduction process.

CVTool

2020

Protocol transformation for Maude-NPA that safely discards certain cryptographic properties, bringing within reach protocols whose algebraic properties are inexpressible or whose state space is otherwise unmanageable.

CR-MGVU

2020

Brings constructor symbols into variant-based equational unification, so the procedure stops as soon as it can and stops returning the surplus unifiers that the constructor-agnostic version computes.

Presto

2020

Symbolic partial evaluator that specializes Maude rewrite theories with respect to a given goal, producing optimized programs while preserving their observable behavior.

MGVU

2019

Narrowing-based unification algorithm that computes most general variant unifiers, improving on the original variant-based algorithm both in execution time and in the number of unifiers returned, with experiments for exclusive-or and Abelian group theories.

Narval

2019

Stepper for variant-based narrowing that allows users to symbolically explore, one step at a time, the reachable states and unifiers of a Maude theory modulo its equational axioms.

Atame

2018

Infers safety assertions for Maude programs and automatically repairs the fragments of code that violate them, helping ensure correctness without manual intervention.

Abets

2016

Combines runtime assertion checking with trace slicing to isolate the fragments of a Maude computation responsible for an assertion violation, easing error diagnosis.

Anima

2014

Interactive tool for inspecting Maude executions one rewrite at a time; it also performs forward trace slicing, complementing the backward slicing carried out by iJulienne.

iJulienne

2013

Backward trace-slicing tool that reduces a rewriting sequence to the fragments relevant to a piece of data of interest, filtering out irrelevant computation steps to ease debugging.

Mau-Dev

2013

Developer-oriented extension of the official Maude release adding debugging and tracing utilities on top of the standard interpreter.

Maude for Windows

2013

Compilation guide and ready-to-use binaries that make it possible to build and run Maude natively on Windows, which the official releases do not directly target.

Background

Research Stays

  • Sep 2020 – Dec 2021

    Universidad Complutense de Madrid

    Hosted by Prof. Narciso Martí-Oliet

  • Sep – Nov 2015

    Università degli Studi di Siena

    Hosted by Prof. Moreno Falaschi

Fellowships

  • 2019 – 2021

    APOSTD Postdoctoral Fellowship

    Generalitat Valenciana (GVA)

  • 2013 – 2017

    FPI-UPV Predoctoral Fellowship

    Universitat Politècnica de València

Education & Courses