|
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
|
|
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) .
|