biblio-sami_intc.bib
@comment{{This file has been generated by bib2bib 1.93}}
@comment{{Command line: bib2bib -ob biblio-sami_intc.bib -c "lipn-category: 'intc'" biblio-sami.bib}}
@comment{{This file has been generated by bib2bib 1.93}}
@comment{{Command line: bib2bib abbrevs.bib Evangelista.bib -c '(year >= 2003) and (year <= 2013)'}}
@comment{{This file has been generated by bib2bib 1.93}}
@comment{{Command line: bib2bib -c "author: 'Evangelista'" biblio.bib}}
@inproceedings{E05,
author = {Sami Evangelista},
title = {{High Level Petri Nets Analysis with Helena}},
booktitle = {{ATPN'2005}},
series = {LNCS},
volume = {3536},
publisher = {Springer},
pages = {455--464},
year = {2005},
paper = {doc/ICATPN-2005.pdf},
slides = {doc/ICATPN-2005-slides.pdf},
abstract = {This paper presents the high level Petri nets analyzer Helena.
Helena can be used for the on-the-fly verification of state properties, i.e.,
properties that must hold in all the reachable states of the system, and
deadlock freeness. Some features of Helena make it particularly efficient
in terms of memory management. Structural abstractions techniques,
mainly transitions agglomerations, are used to tackle the state explosion
problem. Benchmarks are presented which compare our tool to Maria.
Helena is developed in portable Ada and is freely available under the
conditions of the GNU General Public License.},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EKPPR03,
author = {Sami Evangelista and Claude Kaiser and Jean-Fran\c{c}ois Pradat-Peyre and
Pierre Rousseau},
booktitle = {{AEU'2003}},
series = {LNCS},
publisher = {Springer},
volume = {2655},
title = {{Quasar: a New Tool for Analysing Concurrent Programs}},
year = {2003},
pages = {168--181},
paper = {doc/AEU-2003.pdf},
abstract = {Concurrency introduces a high degree of combinatory which
may be the source of subtle mistakes. We present a new tool, Quasar,
which is based on ASIS and which uses fully the concept of patterns. The
analysis of a concurrent Ada program by our tool proceeds in four steps:
automatic extraction of the concurrent part of the program; translation
of the simplified program into a formal model using predefined patterns
that are combined by substitution and merging constructors; analysis of
the model both by structural techniques and model-checking techniques;
reporting deadlock or starvation results. We demonstrate the usefulness
of Quasar by analyzing several variations of a non trivial concurrent
program.},
tags = {tool,petri nets},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EPPP07,
author = {Sami Evangelista and Christophe Pajault and Jean-Fran\c{c}ois Pradat-Peyre},
title = {{A Simple Positive Flows Computation Algorithm for a Large Subclass of Colored
Nets}},
booktitle = {{FORTE'2007}},
year = {2007},
pages = {177--195},
series = {LNCS},
publisher = {Springer},
volume = {4574},
paper = {doc/FORTE-2007.pdf},
abstract = {Positive flows provide very useful informations that can be
used to perform efficient analysis of a model. Although algorithms computing
(a generative family of) positive flows in ordinary Petri nets are
well known, computing a generative family of positive flows in colored
net remains an open problem. We propose in this paper a pragmatic approach
that allows us to define an algorithm that computes a generative
family of particular but useful positive flows in a large subclass of colored
nets: the simple well-formed nets.},
tags = {petri nets},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EP07,
author = {Sami Evangelista and Christophe Pajault},
title = {{Some Solutions to the Ignoring Problem}},
booktitle = {{SPIN'2007}},
year = {2007},
pages = {76--94},
series = {LNCS},
publisher = {Springer},
volume = {4595},
paper = {doc/SPIN-2007.pdf},
slides = {doc/SPIN-2007-slides.pdf},
abstract = {
The ignoring problem refers to the fact that some actions may be infinitely
postponed by a state space search algorithm that makes use of partial order
reduction (POR). The prevention of this phenomenon is mandatory if one wants to
verify more elaborate properties than the deadlock freeness, e.g., safety or
liveness properties. We present in this work some solutions to this problem. In
order to assess the quality of our propositions, we included them in our model
checker Helena. We report the result of some experiments which show that our
algorithms yield better reductions than state of the art algorithms like those
implemented in the Spin tool.},
tags = {por},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EKPPPR05,
author = {Sami Evangelista and Claude Kaiser and Christophe Pajault and
Jean-Fran\c{c}ois Pradat-Peyre and Pierre Rousseau},
title = {{Dynamic Tasks Verification with Quasar}},
booktitle = {{AEU'2005}},
year = {2005},
pages = {91--104},
series = {LNCS},
publisher = {Springer},
volume = {3555},
paper = {doc/AEU-2005.pdf},
abstract = {The inclusion of dynamic tasks modelisation in QUASAR, a tool for
automatic analysis of concurrent programs, extends its applicative usefulness.
However this extension leads to large size models whose processing has to face
combinatory explosion of modeling states. This paper presents briefly Ada
dynamic tasks semantic and dependences and then it explains the choice of an
efficient generic modeling pattern. This implies to consider the naming, the
hierarchy, the master retrieval, the termination of dynamic tasks and their
synchronization dependences successively. The adequacy of both this modeling
and the QUASAR techniques is highlighted by the analysis of two non-trivial Ada
programs. The large reduction factor between the initial and final state
numbers of these program models shows that the state explosion can be limited,
making automatic validation of dynamic concurrent programs feasible.},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EKPPR03-2,
author = {Sami Evangelista and Claude Kaiser and Jean-Fran\c{c}ois Pradat-Peyre and
Pierre Rousseau},
title = {{Verifying linear time temporal logic properties of concurrent Ada programs
with quasar}},
booktitle = {{SIGADA'2003}},
year = {2003},
pages = {17--24},
publisher = {ACM},
paper = {doc/SIGADA-2003.pdf},
slides = {doc/SIGADA-2003-slides.pdf},
abstract = {In this paper we present an original and useful way for specifying
and verifying temporal properties of concurrent programs with our tool
named Quasar. Quasar is based on ASIS and uses formal methods (model
checking). Properties that can be checked are either general, like
deadlock or fairness, or more context specific, referring to tasks
states or to value of variables; properties are then expressed in
temporal logic. In order to simplify the expression of these
properties, we define some templates that can be instantiated with
specific items of the programs. We demonstrate the usefulness of these
templates by verifying subtle variations of the Peterson
algorithm. Thus, although Quasar uses up-to-date formal methods it
remains accessible to a large class of practitioners.},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{E08,
author = {Sami Evangelista},
title = {{Dynamic Delayed Duplicate Detection for External Memory Model Checking}},
booktitle = {{SPIN'2008}},
year = {2008},
pages = {77--94},
series = {LNCS},
publisher = {Springer},
volume = {5156},
paper = {doc/SPIN-2008.pdf},
slides = {doc/SPIN-2008-slides.pdf},
abstract = {
Duplicate detection is an expensive operation of disk-based
model checkers. It consists of comparing some potentially new states, the
candidate states, to previous visited states. We propose a new approach
to this technique called dynamic delayed duplicate detection. This one
exploits some typical properties of states spaces, and adapts itself to
the structure of the state space to dynamically decide when duplicate
detection must be conducted. We implemented this method in a new
algorithm and found out that it greatly cuts down the cost of duplicate
detection. On some classes of models, it performs significantly better
than some previously published algorithms},
tags = {external},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EK09-3,
author = {Sami Evangelista and Lars M. Kristensen},
title = {{Dynamic State Space Partitioning for External Memory Model Checking}},
booktitle = {{FMICS'2009}},
paper = {doc/FMICS-2009.pdf},
slides = {doc/FMICS-2009-slides.pdf},
year = {2009},
pages = {70--85},
series = {LNCS},
publisher = {Springer},
volume = {5825},
abstract = {We describe a dynamic partitioning scheme usable by model
checking techniques that divide the state space into partitions, such as
most external memory and distributed model checking algorithms. The
goal of the scheme is to reduce the number of transitions that link states
belonging to different partitions, and thereby limit the amount of disk
access and network communication. We report on several experiments
made with our verification platform ASAP that implements the dynamic
partitioning scheme proposed in this paper.},
tags = {external,distributed},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EHPP05,
author = {Sami Evangelista and Serge Haddad and Jean-Fran\c{c}ois Pradat-Peyre},
booktitle = {{ATVA'2005}},
title = {{Syntactical Colored Petri Nets Reductions}},
year = {2005},
publisher = {Springer},
series = {LNCS},
volume = {3707},
pages = {202--216},
paper = {doc/ATVA-2005.pdf},
slides = {doc/ATVA-2005-slides.pdf},
abstract = {In this paper, we develop a syntactical version of elaborated reductions
for high-level Petri nets. These reductions simplify the model by merging
some sequential transitions into an atomic one. Their conditions combine local
structural ones (e.g. related to the actions of a thread) and global algebraic
ones (e.g. related to the threads synchronization). We show that these
conditions are performed in a syntactical way, when a syntax of the color
mappings is given. We show also how our method outperforms previous ones on a
recent case study with regard both to the reduction ratio and the
automatization of their application.},
tags = {petri nets,reduction},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EHPP04,
author = {Sami Evangelista and Serge Haddad and Jean-Fran\c{c}ois Pradat-Peyre},
booktitle = {{WODES'2004}},
pages = {355--360},
title = {{New Coloured Reductions for Software Validation}},
year = {2004},
paper = {doc/WODES-2004.pdf},
abstract = {Structural model abstraction is a powerful technique for reducing the
complexity of a state based enumeration analysis.We present in this paper
accurate reductions for high-level Petri nets based on new ordinary Petri nets
reductions. These reductions involve only structural and algebraical
conditions. They preserve the liveness of the net and any LTL formula that does
not observe the reduced transitions of the net. The mixed use of structural and
algebraical conditions signicantly enlarges their application area. Furthermore
the specication of the transformation is parametric with respect to the
cardinalities of coloured domains.},
tags = {reduction,petri nets},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EPP06,
author = {Sami Evangelista and Jean-Francois Pradat-Peyre},
title = {{On the Computation of Stubborn Sets of Colored Petri Nets}},
year = {2006},
publisher = {Springer},
series = {LNCS},
booktitle = {{ATPN'2006}},
volume = {4024},
pages = {146--165},
paper = {doc/ICATPN-2006.pdf},
slides = {doc/ICATPN-2006-slides.pdf},
summary = {Introduces a symbolic algorithm to compute stubborn sets of colored Petri
nets. Not as efficient as if it was applied on the unfolded net but does not
require an unfolding of the net. The algorithm is implemented in Helena
\cite{E05}.},
abstract = {Valmari's Stubborn Sets method is a member of the so-called
partial order methods. These techniques are usually based on a selective
search algorithm: at each state processed during the search, a stubborn
set is calculated and only the enabled transitions of this set are used to
generate the successors of the state. The computation of stubborn sets
requires to detect dependencies between transitions in terms of conflict
and causality. In colored Petri nets these dependencies are difficult to
detect because of the color mappings present on the arcs: conflicts and
causality connections depend on the structure of the net but also on
these mappings. Thus, tools that implement this technique usually unfold
the net before exploring the state space, an operation that is often
untractable in practice. We present in this work an alternative method
which avoids the cost of unfolding the net. To allow this, we use a
syntactically restricted class of colored nets. Note that this class still
enables wide modeling facilities since it is the one used in our model checker
Helena which has been designed to support the verification of software
specifications. The algorithm presented has been implemented and several
experiments which show the benefits of our approach are reported.
For several models we obtain a reduction close or even equal to the one
obtained after an unfolding of the net. We were also able to efficiently
reduce the state spaces of several models obtained by an automatic translation
of concurrent software.},
tags = {por,petri nets},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{EPP05,
author = {Sami Evangelista and Jean-Fran\c{c}ois Pradat-Peyre},
title = {{Memory Efficient State Space Storage in Explicit Software Model Checking}},
year = {2005},
publisher = {Springer},
series = {LNCS},
booktitle = {{SPIN'2005}},
volume = {3639},
pages = {43--57},
paper = {doc/SPIN-2005.pdf},
slides = {doc/SPIN-2005-slides.pdf},
abstract = {The limited amount of memory is the major bottleneck in
model checking tools based on an explicit states enumeration. In this
context, techniques allowing an efficient representation of the states are
precious. We present in this paper a novel approach which enables to
store the state space in a compact way. Though it belongs to the family
of explicit storage methods, we qualify it as semi-explicit since all states
are not explicitly represented in the state space. Our experiments report
a memory reduction ratio up to 95% with only a tripling of the computing
time in the worst case.},
tags = {reduction},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{WEK09,
author = {Michael Westergaard and Sami Evangelista and Lars M. Kristensen},
title = {{ASAP: An Extensible Platform for State Space Analysis}},
booktitle = {ATPN'2009},
publisher = {Springer},
series = {LNCS},
year = {2009},
volume = {5606},
pages = {303--312},
paper = {doc/ICATPN-2009.pdf},
slides = {doc/ICATPN-2009-slides.pptx},
abstract = {The ASCoVeCo State space Analysis Platform (ASAP) is
a tool for performing explicit state space analysis of coloured Petri nets
(CPNs) and other formalisms. ASAP supports a wide range of state space
reduction techniques and is intended to be easy to extend and to use,
making it a suitable tool for students, researchers, and industrial users
that would like to analyze protocols and/or experiment with different
algorithms. This paper presents ASAP from these two perspectives.},
tags = {tool},
lipn-category = {intc},
lipn-time = {ant}
}
@inproceedings{CDEHKP10,
author = {Christine Choppy and Anna Dedova and Sami Evangelista and Silien Hong and Kais
Klai and Laure Petrucci},
title = {{The NEO Protocol for Large-Scale Distributed Database Systems: Modelling and
Initial Verification}},
booktitle = {{ATPN'2010}},
series = {LNCS},
publisher = {Springer},
year = {2010},
volume = {6128},
pages = {145--164},
abstract = {This paper presents the modelling process and first analysis results
carried out within the NEOPPOD project. A protocol, NEO, has been
designed in order to manage very large distributed databases such as
those used for banking and e-government applications, and thus to
handle sensitive data. Security of data is therefore a critical
issue that must be ensured before the software can be released on
the market.
Our project aims at verifying essential properties of the protocol
so as to guarantee such properties are satisfied. The model was
designed by reverse-engineering from the source code, and then
initial verification was performed. This modelling work requires
choices of adequate abstraction levels both at the modelling and
verification stages. In particular, the overall system is so large
that the model should be carefully built in order to make
verification possible without getting too far from the actual
protocol implementation.},
paper = {doc/ICATPN-2010.pdf},
slides = {doc/ICATPN-2010-slides.pdf},
lipn-category = {intc}
}
@inproceedings{EPY11,
author = {Sami Evangelista and Laure Petrucci and Samir Youcef},
title = {{Parallel Nested Depth-First Searches for LTL Model Checking}},
booktitle = {{ATVA'2011}},
series = {LNCS},
publisher = {Springer},
year = {2011},
volume = {6996},
pages = {381--396},
abstract = {Even though the well-known nested-depth first search algorithm for
LTL model checking provides good performance, it cannot benefit from the re-
cent advent of multi-core computers. This paper proposes a new version of this
algorithm, adapted to multi-core architectures with a shared memory. It can ex-
hibit good speed-ups as supported by a series of experiments.},
paper = {doc/ATVA-2011.pdf},
slides = {doc/ATVA-2011-slides.pdf},
tags = {parallel,ltl},
lipn-category = {intc}
}
@inproceedings{ACE11,
author = {Leila Abidi and Christophe C{\'e}rin and Sami Evangelista},
title = {{A Petri-Net Model for the Publish-Subscribe Paradigm and
Its Application for the Verification of the BonjourGrid Middleware}},
booktitle = {SCC'2011},
publisher = {IEEE},
year = {2011},
pages = {496--503},
abstract = {In this article we focus on the modelization of
the BonjourGrid protocol which is based on the Publish-
Subscribe (Pub-Sub) paradigm, a paradigm for asynchronous
communication that is useful for implementing some approaches
in distributed programming. The aim of this paper
is to isolate the generic mechanisms of construction for the
publish-subscribe approach then to model and verify, based on
those mechanisms, the BonjourGrid protocol that allows the
coordination of multiple instances of desktop grid middleware.
We produce models using colored Petri nets in order to describe
a specific modeling approach for the Pub-Sub paradigm. Such
models are important, first, to formally verify the adequacy
of BonjourGrid in the coordination of resources in desktop
grids - for example by proving the absence of a deadlock in
the BonjourGrid protocol, and second, to offer a 'composition'
mechanism for integrating any protocol based on the Pub-Sub
paradigm. These ideas are illustrated along the BonjourGrid
case study and they constitute a methodology of building Pub-
Sub systems.},
paper = {doc/SCC-2011.pdf},
slides = {doc/SCC-2011-slides.pdf},
lipn-category = {intc}
}
@inproceedings{EK12,
author = {Sami Evangelista and Lars M. Kristensen},
title = {{Hybrid On-the-Fly Model Checking with the Sweep-line Method}},
booktitle = {{ATPN'2012}},
series = {LNCS},
publisher = {Springer},
year = {2012},
volume = {7347},
pages = {248--267},
abstract = {The sweep-line method allows explicit state model checkers to delete
states from memory on-the-fly during state space
exploration thereby lowering the memory demands of
the verification procedure. The sweep-line method
is based on a least progress-first search order that
prohibits the immediate use of standard on-the-fly
LTL model checking algorithms that rely on a
depth-first search order. This paper proposes and
experimentally evaluates an algorithm for LTL model
checking compatible with the search order prescribed
by the sweep-line method.},
paper = {doc/ICATPN-2012.pdf},
slides = {doc/ICATPN-2012-slides.pdf},
lipn-category = {intc}
}
@inproceedings{EK12-2,
author = {Sami Evangelista and Lars M. Kristensen},
title = {{Combining the Sweep-Line Method with the use of
an External-memory Priority Queue}},
booktitle = {{SPIN'2012}},
series = {LNCS},
publisher = {Springer},
year = {2012},
volume = {7385},
pages = {43--61},
abstract = {The sweep-line method is an explicit-state model checking technique
that uses a notion of progress to delete states from
internal memory during state space exploration and
thereby reduce peak memory usage. The sweep-line
algorithm relies on the use of a priority queue
where the progress value assigned to a state
determines the priority of the state. In earlier
implementations of the sweep-line method the
progress priority queue is kept in internal memory
together with the current layer of states being
explored. In this paper we investigate a scheme
where the current layer is stored in internal memory
while the priority queue is stored in external
memory. From the perspective of the sweep-line
method, we show that this combination can yield a
significant reduction in peak memory usage compared
to a pure internal memory implementation. On an
average of 60 example instances, this combination
reduced peak memory usage by a factor of 25 at the
cost of an increase in execution time by a factor of
2.5. From the perspective of external memory state
space exploration, we demonstrate experimentally
that the state deletion performed by the sweep-line
method may reduce the I/O overhead induced by
duplicate detection compared to a pure external
memory state space exploration method.},
paper = {doc/SPIN-2012.pdf},
slides = {doc/SPIN-2012-slides.pdf},
lipn-category = {intc}
}
@inproceedings{ELPP12,
author = {Sami Evangelista and Alfons Laarman and Laure Petrucci and Jaco Van De Pol},
title = {{Improved Multi-Core Nested Depth-First Search}},
booktitle = {{ATVA'2012}},
series = {LNCS},
publisher = {Springer},
year = {2012},
volume = {7561},
pages = {269--283},
abstract = {This paper presents CNDFS, a tight integration of two earlier
multi-core nested depth-first search (NDFS) algorithms for LTL model
checking. CNDFS combines the different strengths and avoids some
weaknesses of its predecessors. We compare CNDFS to an earlier
ad-hoc combination of those two algorithms and show several benefits:
It has shorter and simpler code and a simpler correctness proof.
It exhibits more stable performance and scalability, while at
the same time reducing memory requirements.
The algorithm has been implemented in the multi-core backend of the
LTSmin model checker, which is now benchmarked for the first time on
a 48~core machine (previously 16). The experiments demonstrate better
scalability than other parallel LTL model checking algorithms, but we also
investigate apparent bottlenecks. Finally, we noticed that
the multi-core NDFS algorithms produce shorter counterexamples,
surprisingly often shorter than their BFS-based counterparts.},
paper = {doc/ATVA-2012.pdf},
slides = {doc/ATVA-2012-slides.pdf},
tags = {parallel,ltl},
lipn-category = {intc}
}