Parlog Programs Nontermination Analysis. - María-del-Mar Gallardo; José M. Troya (GULP, 1993)

Granularity Analysis of Concurrent Logic Languages based on Abstract Interpretation. - María-del-Mar Gallardo; José M. Troya (GULP-PRODE (1), 1994)

Studying the Cost of Logic Languages in an Abstract Interpretation Framework for Granularity Analysis. - María-del-Mar Gallardo; José M. Troya (LOPSTR, 1995)

A Framework for Automatic Construction of Abstract Promela Models. - María-del-Mar Gallardo; Pedro Merino 001 (SPIN, 1999)

Verifying Distributed Systems with Model Checking and Static Analysis. - María-del-Mar Gallardo; Pedro Merino 001 (ICDCS Workshop on Distributed System Validation and Verification, 2000)

Using XML to implement abstraction for Model Checking. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Estefanía Rosales (SAC, 2002)

Refinement of LTL Formulas for Abstract Model Checking. - María-del-Mar Gallardo; Pedro Merino 001; Ernesto Pimentel 001 (SAS, 2002)

alpha SPIN: Extending SPIN with Abstraction. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Ernesto Pimentel 001 (SPIN, 2002)

An extension of the ns simulator for active network research. - Guillermo Rodríguez; Pedro Merino 001; María-del-Mar Gallardo (Comput. Commun., 2002)

A Tool for Abstraction in Model Checking. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Ernesto Pimentel 001 (FMICS, 2002)

Comparing Under and Over-Approximations of LTL Properties for Model Checking. - María-del-Mar Gallardo; Pedro Merino 001; Ernesto Pimentel 001 (WFLP, 2002)

Debugging UML Designs with Model Checking. - María-del-Mar Gallardo; Pedro Merino 001; Ernesto Pimentel 001 (J. Object Technol., 2002)

Abstract Model Checking and Refinement of Temporal Logic in aSPIN. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Ernesto Pimentel 001 (ACSD, 2003)

Applying Data Abstraction to XML Formal Designs. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Ernesto Pimentel 001 (SNPD, 2003)

Abstract Model Checking of tccp programs. - María Alpuente; María-del-Mar Gallardo; Ernesto Pimentel 001; Alicia Villanueva (QAPL, 2004)

Integration of Reliability and Performance Analyses for Active Network Services. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Guillermo Rodríguez (FMICS, 2004)

A generalized semantics of PROMELA for abstract model checking. - María-del-Mar Gallardo; Pedro Merino 001; Ernesto Pimentel 001 (Formal Aspects Comput., 2004)

aSPIN: A tool for abstract model checking. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Ernesto Pimentel 001 (Int. J. Softw. Tools Technol. Transf., 2004)

Semantic Access Control Model: A Formal Specification. - Mariemma Inmaculada Yagüe del Valle; María-del-Mar Gallardo; Antonio Mana (ESORICS, 2005)

Model checking software with well-defined APIs: the socket case. - Pedro de la Cámara; María-del-Mar Gallardo; Pedro Merino 001; David Sanán (FMICS, 2005)

Model checking active networks with SPIN. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001 (Comput. Commun., 2005)

A semantic framework for the abstract model checking of tccp programs. - María Alpuente; María-del-Mar Gallardo; Ernesto Pimentel 001; Alicia Villanueva (Theor. Comput. Sci., 2005)

Implementing Influence Analysis Using Parameterised Boolean Equation Systems. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001 (ISoLA, 2006)

Abstract Matching for Software Model Checking. - Pedro de la Cámara; María-del-Mar Gallardo; Pedro Merino 001 (SPIN, 2006)

Towards Model Checking C Code with OPEN/CÆSAR. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (MSVVEIS, 2006)

Static Analysis using Parameterised Boolean Equation Systems - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001 (CoRR, 2006)

On the Evolution of reliability Methods for Critical Software. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Ernesto Pimentel 001 (Trans. SDPS, 2006)

Verifying Real-Time Properties of tccp Programs. - María Alpuente; María-del-Mar Gallardo; Ernesto Pimentel 001; Alicia Villanueva (J. Univers. Comput. Sci., 2006)

On-the-fly model checking for C programs with extended CADP in FMICS-jETI. - María-del-Mar Gallardo; Pedro Merino 001; Christophe Joubert; David Sanán (ICECCS, 2007)

Model Extraction for ARINC 653 Based Avionics Software. - Pedro de la Cámara; María-del-Mar Gallardo; Pedro Merino 001 (SPIN, 2007)

C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001; David Sanán (SPIN, 2007)

Extending CADP for Analyzing C Code. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (MSVVEIS, 2007)

An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation. - María Alpuente; María-del-Mar Gallardo; Ernesto Pimentel 001; Alicia Villanueva (PROLE, 2007)

On-the-Fly Data Flow Analysis Based on Verification Technology. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001 (COCV@ETAPS, 2007)

PiXL: Applying xml standards to support the integration of analysis tools for protocols. - María-del-Mar Gallardo; Jesús Martínez; Pedro Merino 001; Pablo Núñez; Ernesto Pimentel 001 (Sci. Comput. Program., 2007)

Model Checking C Programs with Dynamic Memory Allocation. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (COMPSAC, 2008)

Web Services for Accessing Explicit State Space Verification Tools. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001; David Sanán (ERCIM News, 2008)

Developing a Decision Support Tool for Dam Management with SPIN. - María-del-Mar Gallardo; Pedro Merino 001; Laura Panizo; Antonio Linares (FMICS, 2009)

Using SCADE for Decision Support in Dam Management. - María-del-Mar Gallardo; Pedro Merino 001; Laura Panizo; Antonio Linares (MSVVEIS, 2009)

Model Checking Dynamic Memory Allocation in Operating Systems. - María-del-Mar Gallardo; Pedro Merino 001; David Sanán (J. Autom. Reason., 2009)

Checking the reliability of socket based communication software. - Pedro de la Cámara; María-del-Mar Gallardo; Pedro Merino 001; David Sanán (Int. J. Softw. Tools Technol. Transf., 2009)

Verification of Dynamic Data Tree with mu-calculus Extended with Separation. - María-del-Mar Gallardo; David Sanán (SEFM, 2010)

A practical use of model checking for synthesis: generating a dam controller for flood management. - María-del-Mar Gallardo; Pedro Merino 001; Laura Panizo; Antonio Linares (Softw. Pract. Exp., 2011)

Verification support for ARINC-653-based avionics software. - Pedro de la Cámara; J. Raúl Castro; María-del-Mar Gallardo; Pedro Merino 001 (Softw. Test. Verification Reliab., 2011)

Preface of Prole 2012. - María-del-Mar Gallardo (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

A model-extraction approach to verifying concurrent C programs with CADP. - María-del-Mar Gallardo; Christophe Joubert; Pedro Merino 001; David Sanán (Sci. Comput. Program., 2012)

An extension of Java PathFinder for hybrid systems. - Laura Panizo; María-del-Mar Gallardo (ACM SIGSOFT Softw. Eng. Notes, 2012)

Verification of complex dynamic data tree with mu-calculus. - María-del-Mar Gallardo; David Sanán (Autom. Softw. Eng., 2013)

Modeling Hybrid Systems in Hy-tccp. - Damián Adalid; María-del-Mar Gallardo; Laura Titolo (CoRR, 2014)

Modeling Hybrid Systems in the Concurrent Constraint Paradigm. - Damián Adalid; María-del-Mar Gallardo; Laura Titolo (PROLE, 2014)

Using SPIN for automated debugging of infinite executions of Java programs. - Damián Adalid; Alberto Salmerón; María-del-Mar Gallardo; Pedro Merino 001 (J. Syst. Softw., 2014)

Extending model checkers for hybrid system verification: the case study of SPIN. - María-del-Mar Gallardo; Laura Panizo (Softw. Test. Verification Reliab., 2014)

Abstract Analysis of Universal Properties for tccp. - Marco Comini; María-del-Mar Gallardo; Laura Titolo; Alicia Villanueva (LOPSTR, 2015)

Runtime Verification of Expected Energy Consumption in Smartphones. - Ana Rosario Espada; María-del-Mar Gallardo; Alberto Salmerón; Pedro Merino 001 (SPIN, 2015)

Using Model Checking to Generate Test Cases for Android Applications. - Ana Rosario Espada; María-del-Mar Gallardo; Alberto Salmerón; Pedro Merino 001 (MBT, 2015)

River Basin Management with Spin. - María-del-Mar Gallardo; Pedro Merino 001; Laura Panizo; Alberto Salmerón (SPIN, 2016)

Adding Correctness Checking to Test Automation Platform. - Alberto Salmerón; Leticia Lavado; María-del-Mar Gallardo; Pedro Merino Gómez (ISSRE Workshops, 2017)

Guided test case generation for mobile apps in the TRIANGLE project: work in progress. - Laura Panizo; Alberto Salmerón; María-del-Mar Gallardo; Pedro Merino 001 (SPIN, 2017)

A Simulation Tool for tccp Programs. - María-del-Mar Gallardo; Leticia Lavado; Laura Panizo (WLP / WFLP, 2017)

A program analysis framework for tccp based on abstract interpretation. - Marco Comini; María-del-Mar Gallardo; Laura Titolo; Alicia Villanueva (Formal Aspects Comput., 2017)

A constraint-based language for modelling intelligent environments. - María-del-Mar Gallardo; Leticia Lavado; Laura Panizo; Laura Titolo (J. Reliab. Intell. Environ., 2017)

A characterisation of verification tools for software defined networks. - Leticia Lavado; Laura Panizo; María-del-Mar Gallardo; Pedro Merino 001 (J. Reliab. Intell. Environ., 2017)

Performance Analysis of Spotify® for Android with Model-Based Testing. - Ana Rosario Espada; María-del-Mar Gallardo; Alberto Salmerón; Pedro Merino 001 (Mob. Inf. Syst., 2017)

Integrating river basin DSSs with model checking. - María-del-Mar Gallardo; Pedro Merino 001; Laura Panizo; Alberto Salmerón (Int. J. Softw. Tools Technol. Transf., 2018)

How Formal Methods Can Contribute to 5G Networks. - María-del-Mar Gallardo; Francisco Luque-Schempp; Pedro Merino Gómez; Laura Panizo (From Software Engineering to Formal Methods and Tools, and Back, 2019)

Trace Analysis Using an Event-Driven Interval Temporal Logic. - María-del-Mar Gallardo; Laura Panizo (LOPSTR, 2019)

Teaching Formal Methods: From Software in the Small to Software in the Large. - María-del-Mar Gallardo; Laura Panizo (FMTea, 2019)

A formal approach to automatically analyse extra-functional properties in mobile applications. - Ana Rosario Espada; María-del-Mar Gallardo; Alberto Salmerón; Laura Panizo; Pedro Merino 001 (Softw. Test. Verification Reliab., 2019)

Introduction to the Special Issue devoted to SPIN 2018. - María-del-Mar Gallardo; Pedro Merino 001 (Int. J. Softw. Tools Technol. Transf., 2020)

Modeling and verification of the Multi-connection Tactile Internet Protocol. - Delia Rico; María-del-Mar Gallardo; Pedro Merino 001 (Q2SWinet, 2021)

A denotational semantics for PROMELA addressing arbitrary jumps. - Marco Comini; María-del-Mar Gallardo; Alicia Villanueva (CoRR, 2021)

Toward Zero Touch Configuration of 5G Non-Public Networks for Time Sensitive Networking. - Francisco Luque-Schempp; Laura Panizo; María-del-Mar Gallardo; Pedro Merino 001; Javier Rivas (IEEE Netw., 2022)

The Role of Abstraction in Model Checking. - María-del-Mar Gallardo; Pedro Merino 001; Laura Panizo (Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, 2023)

AutomAdapt: Zero Touch Configuration of 5G QoS Flows Extended for Time-Sensitive Networking. - Francisco Luque-Schempp; Laura Panizo; María-del-Mar Gallardo; Pedro Merino 001 (IEEE Access, 2023)

STAn: analysis of data traces using an event-driven interval temporal logic. - Laura Panizo; María-del-Mar Gallardo (Autom. Softw. Eng., 2023)

Verification of a multi-connectivity protocol for Tactile Internet applications. - Delia Rico; María-del-Mar Gallardo; Pedro Merino 001 (Comput. Commun., 2023)

Flextory: Flexible Software Factory of IoT Data Consumers. - Rafael López-Gómez; Laura Panizo; María-del-Mar Gallardo (Sensors, 2024)

Runtime monitoring of 5G network slicing using STAn. - Laura Panizo; María-del-Mar Gallardo; Francisco Luque-Schempp; Pedro Merino 001 (J. Log. Algebraic Methods Program., 2025)

Corrigendum to "Runtime monitoring of 5G network slicing using STAn" [Journal of Logical and Algebraic Methods in Programming, 145 (2025) 101059]. - Laura Panizo; María-del-Mar Gallardo; Francisco Luque-Schempp; Pedro Merino 001 (J. Log. Algebraic Methods Program., 2025)