Papers
 

2007

Pedro de la Cámara, María del Mar Gallardo, Pedro Merino
Model Extraction for ARINC 653 based Avionics Software
to be presented at the 14th International Workshop on Model Checking Software (SPIN07),
Berlin, Germany, July 1-3


María del Mar Gallardo, Christophe Joubert, Pedro Merino, David Sanán
C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs
to be presented at the 14th International Workshop on Model Checking Software (SPIN07),
Berlin, Germany, July 1-3

María del Mar Gallardo, Pedro Merino, David Sanán
Extending CADP for Analising C Code
to be presented at the Fifth International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS'07)

María del Mar Gallardo, Christophe Joubert, Pedro Merino
On-the-Fly Data Flow Analysis based on Verification Technology
proceedings of the 6th International Workshop on Compiler Optimizations Meets Compiler Verification, COCV 2007, pp. 36-51, Braga, Portugal 2007

2006

María del Mar Gallardo, Jesús Martínez, Pedro Merino, Ernesto Pimentel
On the Evolution of Reliability Methods for Critical Systems
Journal of Integrated Design & Process Science, vol. 10 (4) pp. 55-68, December 2006

María del Mar Gallardo, Christophe Joubert, Pedro Merino
Implementing Influence Analysis using Parameterised Boolean Equation Systems
Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

María del Mar Gallardo, Jesús Martínez, Pedro Merino, Ernesto Pimentel
On the Evolution of Reliability Methods for Critical Software
Proceedings of the Ninth World Conference on Integrated Design & Process Technology

María Alpuente, María del Mar Gallardo, Ernesto Pimentel, Alicia Villanueva
Verifying Real-Time Properties of tccp Programs
Journal of Universal Computer Science, vol. 12, issue 11, 1551-1573, Dec. 2006

María del Mar Gallardo, Jesús Martínez, Pedro Merino, Pablo Núñez, Ernesto Pimentel
PiXL: Applying XML Standards to Support the Integration of  Analysis Tools for Protocols
Science of Computer Programming Journal, Volume 65, Issue 1, 57-69 (March 2007)

Pedro de la Cámara, María del Mar Gallardo, Pedro Merino
Abstract Matching for Software Model Checking
13th International Workshop on Model Checking of Software (SPIN06)
March 30 -- April 1, 2006, Vienna, Austria
Lecture Notes in Computer Science 3925, pp. 182-200

María del Mar Gallardo, Pedro Merino, David Sanán
Towards Model Checking C Code with OPEN/CAESAR
Fourth International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS'06)
May 23-24, 2006 - Paphos, Cyprus

María del Mar Gallardo, Jesús Martínez, Pedro Merino, Pablo Núñez, Ernesto Pimentel
PiXL: Applying XML Standards to Support the Integration of  Analysis Tools
Fourth International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS'06)
May 23-24, 2006 - Paphos, Cyprus

2005

Pedro de la Cámara, María del Mar Gallardo, Pedro Merino, David Sanán
Model Checking Software with well-defined APIs: The Socket case
Proceedings of the Tenth International Workshop on Formal Methods for Industrial Critical Systems (FMICS05)
pp.17-26, Editors T. Margaria & M. Massink, Sponsored by ACM SIGSOFT
This paper has received the
EASST Best Paper Award
September 2005, Lisbon
A summary of this paper has appeared in
The EASST Newsletter Volume 11 (December 2005)

Mariemma Yagüe, María del Mar Gallardo, Antonio Maña
Semantic Access Control Model: A Formal Specification
10th European Symposium on Research in Computer Security
LNCS 3679, Computer Security- ESORICS 2005, pp. 24-43.
2005
September 2005, Milan

María Alpuente, María del Mar Gallardo, Ernesto Pimentel, Alicia Villanueva

A Semantic Framework for the Abstract Model Checking of tccp programs

Theoretical Computer Science, Volume 346, Issue 1, 23 November 2005, Pages 58-95
http://authors.elsevier.com/sd/article/S0304397505004755

M. M. Gallardo, P.Merino, J. Martínez
Model Checking Active Network with SPIN
Computer Communication(2005) 28: 609-622

M. M. Gallardo, P.Merino, J. Martínez, E.Pimentel
Abstracting UML behavioral diagrams for verification
Chapter of the book
"Software Evolution with UML and XML"
Edited by Idea Group Publisher

María Alpuente, María del Mar Gallardo, Ernesto Pimentel, Alicia Villanueva
Verifying Real-Time Properties of tccp Programs
V Jornadas de Programación y Lenguajes to be held in Granada in September 2005

María Alpuente, María del Mar Gallardo, Ernesto Pimentel, Alicia Villanueva

A Semantic Framework for the Abstract Model Checking of tccp programs

(four paged summary)
V Jornadas de Programación y Lenguajes to be held in Granada in September 2005

2004

M. M. Gallardo, P.Merino, J. Martínez, G. Rodríguez
Integration of Reliability and Performance Analyses for Active Network Services
Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 04)
Linz, Austria
Electronic Notes on Theoretical Computer Science, 133:217-236

María Alpuente, María del Mar Gallardo, Ernesto Pimentel, Alicia Villanueva
Abstract Model Checking of tccp programs
Proceedings of the 2nd Workshop on Quantitative Aspects of Programming Languages (QAPL 2004)
.
Electronic Notes in Theoretical Computer Science, 112:16-30

M. M. Gallardo, P.Merino, E.Pimentel
A Generalized Semantics of Promela for Abstract Model Checking
Formal Aspects of Computing (2004) 16: 166-193

María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel
aSPIN: A Tool for Abstract Model Checking
International Journal on Software Tools for Technology Transfer (STTT)
SSN: 1433-2779 (Paper) 1433-2787 (Online)

Issue: Volume 5, Numbers 2-3

Date: March 2004

Pages: 165 - 184

María del Mar Gallardo, Alejandro Carmona, Jesús Martínez y Pedro Merino
Un Marco de Trabajo para la Construcción de Herramientas de Model Checking
 
IV Jornadas de Programación y Lenguajes. Málaga 11-12 de Noviembre de 2004   

M. M. Gallardo, M. Hornos,  P.Merino, J. Martínez
Integration of Interval Logic Specifications into the Model Checking SPIN
XII Jornadas de Concurrencia y Sistemas Distribuidos (2004)

2003

Applying Data Abstraction to XML Formal Designs
by María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel
 4th International Conference on Software Engineering, Artificial Intelligence, Networking, and
Parallel/Distributed Computing (SNPD'03)
Lübeck, Germany       October 16-18, 2003

Abstract Model Checking and Refinement of Temporal Logic in aSPIN
by María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel
Third International Conference on Application of Concurrency to System Design
18-20th of June 2003, Guimarães, Portugal

Transforming Specifications to verify Embedded Systems
by María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel
ERCIM News No. 52, January 2003

http://www.ercim.org/publication/Ercim_News/enw52/

M. M. Gallardo, P.Merino, E.Pimentel
Comparing Abstract Semantics for Model Checking
Proc. of III Jornadas de Programación y Lenguajes
12-14 Noviembre de 2003. Alicante. Páginas 167-182

aSPIN: Implementing Model Checking with Data Abstraction
by María del Mar Gallardo, Jesús Martínez, Pedro Merino and Ernesto Pimentel
 Concurrencia y Sistemas Distribuidos. Actas de las XI Jornadas de Concurrencia (2003), pp. 193-206

2002

M. M. Gallardo, P.Merino, E.Pimentel
Comparing Under and Over-Approximations of LTL Properties for Model Checking
In Proc. of the 11h International Workshop on Functional and (Constraint) Logic Programming (June 2002)
Electronic Notes in Theoretical Computer Science vol. 76

M. M. Gallardo, J. Martínez, P. Merino, E. Pimentel
A Tool for Abstraction in Model Checking
In Proc. of the 7th International Workshop on  Formal Methods for Industrial Critical Systems (July 2002)
Electronic Notes in Theoretical Computer Science.
Vol. 66.2

M. M. Gallardo, P.Merino, E.Pimentel
Debugging UML Designs with Model Checking 
in Journal of Object Technology, vol. 1, no. 2, July-August 2002, pages 101-117
http://www.jot.fm/issues/issue_2002_07/article1

G. Rodríguez, P.Merino,  M. M. Gallardo,
An Extension of the ns Simulator for Active Networks Research,
Computer Communications, 25 (3) (2002) pp. 189-197

M. M. Gallardo, P.Merino, E.Pimentel
Refinement of LTL Formulas for Abstract Model Checking
The 9th International Static Analysis Symposium SAS '02 (September 2002)
Lecture notes in Computer Science v. 2477 pp 395-410

M. M. Gallardo, J. Martínez, P. Merino, E. Pimentel
aSPIN: Extending SPIN with Abstraction
 Proc. of the 9th International SPIN Workshop on Model Checking of Software.
Grenoble, France 2002, LNCS 2318, pg 254-258

M. M. Gallardo, J. Martínez, P. Merino, E. Rosales
Using XML to implement Abstraction for Model Checking.
Proc. of the ACM Symposium on Applied Computing, SAC 2002. pp. 1021-1025
Abstract
http://portal.acm.org/citation.cfm?doid=508791.508989

M. M. Gallardo, P.Merino, E.Pimentel,
Verifying Abstract LTL Properties on Concurrent Systems
Proc. of the  6th World Conference on Integrated Design  & Process Technology.
(2002). Abstract

2001

M. M. Gallardo, P.Merino, E.Pimentel,
Abstract Satisfiability of Linear Temporal Logic,
Actas de las Primeras Jornadas sobre Programación y Lenguajes, pages 163-178 (2001)

G. Rodríguez, P.Merino,  M. M. Gallardo,
Modelado y Simulación de Protocolos para Redes Activas,
III  Jornadas de Ingeniería Telemática, Barcelona (2001) 341-348.

M. M. Gallardo, P.Merino
Automatic Abstraction to Improve Model Checking
IX Jornadas de Concurrencia, Sitges (2001) 79-100.

2000

M. M. Gallardo, P.Merino
A Practical Framework to Integrate Abstractions into SDL and MSC based Tools,
5th International Workshop on Formal Methods for Industrial Critical Systems, Berlin (2000)  225-246.

M. M. Gallardo, P.Merino
Verifying Distributed System with Model Checking and Static Analysis
Proceedings of the IEEE ICDCS 2000 Workshop on Distributed System Validation and Verification (2000)

M. M. Gallardo, P.Merino, J.M.Troya
Property Preserving Abstractions of SDL
Jornadas de Concurrencia 2000 (VIII) (2000)

1999

M. M. Gallardo, P.Merino
A Framework for Automatic Construction of Abstract Promela Models,
Theoretical and Practical Aspects of SPIN Model Checking LNCS-1680
(Springer, 1999) 184-199.

 

1997

M. M. Gallardo, P.Merino, J.M.Troya
Relating Abstract Interpretation with Logic Program Verification,
Proc. Post-ILPS97 Int. Workshop on Verification, Model Cheking and Abstract Interpretation, Port Jefferson, EEUU (1997)

 

1996

M. M. Gallardo, J.M.Troya
Studying the Cost of Logic Languages in an Abstract Interpretation Framework for Granularity Analysis
Lecture Notes in Computer Science, 1048, (1996) 91-105.

 

1995

M. M. Gallardo, J.M.Troya
Studying the Cost of Logic Languages in an Abstract Interpretation Framework for Granularity Analysis
 Fifth Int.
Workshop on Logic Program Synthesis and Transformation, Archen, Holanda (1995)

1994

M. M. Gallardo, J.M.Troya
Granularity Analysis of Concurrent Logic Languages Based on Abstract Interpretation
GULP-PRODE'94, Peñíscola, España (1994) 342-357.

1993

M. M. Gallardo, J.M.Troya
Parlog Programs non-termination analysis
Ottavo Convegno sulla Programmazione Logica (GULP'93) (1993) .

1992

M. M. Gallardo, E.Pimentel, J.M.Troya 
Detección de la no terminación de programas Parlog 
Primer Congreso sobre Programación Declarativa. ProDe'92, Madrid (1992) .