@inproceedings{cpp11,
author = {Xiaomu Shi and
Jean-Fran\c{c}ois Monin and
Fr{\'e}d{\'e}ric Tuong and
Fr{\'e}d{\'e}ric Blanqui},
title = {{First Steps towards the Certification of an ARM Simulator
Using Compcert}},
booktitle = {Certified Proofs and Programs - First International Conference},
year = {2011},
month = {December 7-9},
address = {Kenting, Taiwan},
pages = {346-361},
editor = {Jean-Pierre Jouannaud and Zhong Shao},
publisher = {Springer},
series = {LNCS},
volume = {7086},
isbn = {978-3-642-25378-2},
abstract = { The simulation of Systems-on-Chip (SoC) is nowadays a
hot topic because, beyond providing many debugging
facilities, it allows the development of dedicated
software before the hardware is available.
Low-consumption CPUs such as ARM play a central role
in SoC. However, the effectiveness of simulation
depends on the faithfulness of the simulator. To
this effect, we propose here to prove significant
parts of such a simulator, SimSoC. Basically, on
one hand, we develop a Coq formal model of the ARM
architecture while on the other hand, we consider a
version of the simulator including components
written in Compcert-C. Then we prove that the
simulation of ARM operations, according to
Compcert-C formal semantics, conforms to the
expected formal model of ARM. Size issues are
partly dealt with using automatic generation of
significant parts of the Coq model and of SimSoC
from the official textual definition of ARM.
However, this is still a long-term project. We
report here the current stage of our efforts and
discuss in particular the use of Compcert-C in this
framework. }
}
@inproceedings{discotec11,
pdf = {discotec11.pdf},
author = {Yuxin Deng and St\'{e}phane Grumbach and Jean-Fran\c{c}ois Monin},
title = {{A Framework for Verifying Data-Centric Protocols}},
booktitle = {FMOODS/FORTE 2011},
address = {Reykjavik, Iceland},
year = 2011,
editor = {Bruni, R. and Dingel, J.},
volume = {6722},
pages = {106-120},
series = {LNCS},
month = {June 6-9},
publisher = {Springer},
abstract = { Data centric languages, such as recursive rule based
languages, have been proposed to program distributed
applications over networks. They simplify greatly
the code, which is orders of magnitude shorter, much
more declarative, while still admitting efficient
distributed execution. We show that they also
provide a promising approach to the verification of
distributed protocols, thanks to their data centric
orientation, which allows to explicitly handle
global structures, such as the topology of the
network, routing tables, trees, etc, as well as
their properties. We consider a framework using an
original formalization in the Coq proof assistant of
a distributed computation model based on message
passing with either synchronous or asynchronous
behavior. The declarative rules of the Netlog
language for specifying distributed protocols, as
well as the virtual machines for evaluating these
rules, are encoded in Coq as well. We consider as a
case study tree protocols, and show how this
framework enables us to formally verify them in both
the asynchronous and synchronous setting. }
}
@techreport{bfs-RR-Inria11,
pdf = {netlogcoq-rr.pdf},
author = {Yuxin Deng and St\'{e}phane Grumbach and Jean-Fran\c{c}ois Monin},
title = {{Verifying Declarative Netlog Protocols with Coq: a First Experiment}},
institution = {INRIA},
year = 2011,
type = {Research Report},
pages = {25},
number = 7511,
abstract = {
Declarative languages, such as recursive rule based languages, have
been proposed to program distributed applications over networks. It
has been shown that they simplify greatly the code, while still
offering efficient distributed execution. In this report, we show
that moreover they provide a promising approach to the verification
of distributed protocols. We consider the Netlog language and use
the Coq proof assistant. We first formalize the distributed
computation model based on message passing with either synchronous
or asynchronous behavior. We then see how the declarative rules of
the protocols can be simply encoded in Coq and we develop the
machine embedded on each node of the network which evaluates the
rules. This framework enables us to formally verify distributed
protocols, as shown on a concrete case study, a spanning tree
construction in both the asynchronous and synchronous setting.
}
}
@inproceedings{rapido11,
pdf = {rapido11.pdf},
author = {Blanqui, Fr\'ed\'eric and Helmstetter, Claude and
Joloboff, Vania and Monin, Jean-Fran\c{c}ois and Shi, Xiaomu},
title = {Designing a {CPU} model: from a pseudo-formal document to
fast code},
booktitle = {Proceedings of the 3rd Workshop on
Rapid Simulation and Performance Evaluation: Methods and Tools},
address = {Heraklion, Greece},
month = {January},
year = 2011,
note = {Best Paper Award},
abstract = {
For validating low level embedded software, engineers use simulators
that take the real binary as input. Like the real hardware, these
full-system simulators are organized as a set of components. The main
component is the CPU simulator (ISS), because it is the usual
bottleneck for the simulation speed, and its development is a long
and repetitive task. Previous work showed that an ISS can
be generated from an Architecture Description Language (ADL). In
the work reported in this paper, we generate a CPU simulator
directly from the pseudo-formal descriptions of the reference
manual. For each instruction, we extract the information describing
its behavior, its binary encoding, and its assembly syntax. Next,
after automatically applying many optimizations on the extracted
information, we generate a SystemC/TLM ISS. We also
generate tests for the decoder and a formal specification in
Coq. Experiments show that the generated ISS is as fast and stable
as our previous hand-written ISS.
}
}
@inproceedings{monin10_inversion,
pdf = {coq2.pdf},
hal_id = {inria-00489412},
url = {http://hal.inria.fr/inria-00489412/en/},
title = { {P}roof {T}rick: {S}mall {I}nversions},
author = {{M}onin, {J}ean-{F}ran{\c{c}}ois},
abstract = {{W}e show how an inductive hypothesis can be inverted
with small proof terms, using just dependent
elimination with a diagonal predicate. {T}he
technique works without any auxiliary type such as
{T}rue, {F}alse, eq. {I}t can also be used to
discriminate, in some sense, the constructors of an
inductive type of sort {P}rop in {C}oq.},
language = {{A}nglais},
affiliation = {{FORMES} - {LIAMA} - {INRIA} - {T}singhua
{U}niversity / {B}eijing - {LIAMA} -
{U}niversit{\'e} {J}oseph {F}ourier - {UJF} -
{U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I}
},
booktitle = {{S}econd {C}oq {W}orkshop },
address = {{E}dinburgh {R}oyaume-{U}ni },
organization = {{Y}ves {B}ertot },
editor = {{Y}ves {B}ertot },
audience = {internationale },
day = {09},
month = {July},
year = {2010},
urlpdf = {http://hal.inria.fr/inria-00489412/PDF/paper_1.pdf}
}
@misc{simsoc_cert10,
pdf = {simsoc-cert-work-in-progress.pdf},
author = {Blanqui, F. AND Helmstetter, C. AND Joloboff, V. AND Monin, J.-F. AND Shi, X.},
title = {{SimSoC-Cert: a Certified Simulator for Systems on Chip}},
howpublished = {Draft},
month = {September},
year = {2010},
abstract = {The design and debugging of Systems-on-Chip using a
hardware implementation is difficult and requires
heavy material. Simulation is an interesting
alternative approach, which is both more flexible
and less expensive. SimSoC is a fast
instruction set simulator for various ARM, PowerPC,
and RISC-based architectures. However, speed
involves tricky short-comings and design decisions,
resulting in a complex software product. This makes
the accuracy of the simulator a non-trivial
question: there is a strong need to strengthen the
confidence that simulations results match the
expected accuracy. We therefore decided to
certify SimSoC, that is, to formally prove in
Coq the correctness of a significant part of this
software. The present paper reports our first
efforts in this direction, targeting the ARMv6
architecture. }
}
@misc{coqnetlog_RR,
pdf = {netlog_in_coq.pdf},
title = {{Towards Verifying Declarative Netlog Protocols with Coq}},
author = {Deng, Yuxin AND Grumbach, Stephane AND Monin, Jean-Fran\c{c}ois},
howpublished = {Draft},
pages = {20},
month = {June},
year = {2010},
url = {http://hal.inria.fr/inria-00506093/en/},
abstract = {
Declarative languages, such as recursive rule based languages, have
been proposed to program distributed applications over networks. It
has been shown that they simplify greatly the code,
while still offering efficient
distributed execution. In this paper, we show that moreover they
provide a promising approach to the verification of distributed
protocols. We choose the Netlog language
and use the Coq proof assistant. We first formalize
the distributed computation model
based on message passing with either synchronous or asynchronous behavior.
We then see how the declarative rules of the
protocols can be simply encoded in Coq. Finally, we develop
the machine embedded on each node of the network which evaluates the
rules. This framework enables us to formally verify distributed
declarative protocols, as sketched on a concrete example, a
breadth-first search tree construction in a distributed network.
}
}
@inproceedings{dengmonin09tase,
pdf = {tase09-leader.pdf},
author = {Yuxin Deng and Jean-francois Monin},
title = {{Verifying self-stabilizing population protocols with Coq}},
booktitle = {3rd IEEE International Symposium on Theoretical Aspects of Software Engineering},
year = 2009,
editor = {Jifeng HE and Michael Hinchey and Xirong Ma},
address = {Tianjin, China},
month = {July},
abstract = { Population protocols are an elegant model recently
introduced for distributed algorithms running in
large and unreliable networks of tiny mobile
agents. Correctness proofs of such protocols involve
subtle arguments on infinite sequences of events. We
propose a general formalization of self-stabilizing
population protocols with the Coq proof
assistant. It is used in reasoning about a concrete
protocol for leader election in complete graphs. The
protocol is formally proved to be correct for
networks of arbitrarily large size. To this end we
develop an appropriate theory of infinite sequences,
including results for reasoning on abstractions. In
addition, we provide a constructive correctness
proof for a leader election protocol in directed
rings. An advantage of using a constructive setting
is that we get more informative proofs on the
scenarios that converge to the desired
configurations. }
}
@misc{monin08_universalis,
author = {Jean-Fran\c{c}ois Monin},
title = {Programmation},
howpublished = {Encyclop{\ae}dia Universalis, Corpus},
year = 2008
}
@unpublished{CML06:_balwords,
author = {Judica{\"e}l Courant and Jean-Fran\c{c}ois Monin and Yassine Lakhnech},
title = {Proof pearl: elementary inductive and integer-based
proofs about balanced words},
note = {draft},
ps = {http://www-verimag.imag.fr/~monin/Publis/balwords06.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/balwords06.pdf},
abstract = {Inductive characterizations of words containing the same
number of 'a' and 'b' can easily be given. However, formally
proving the completeness of some of them turns out to be
trickier than one may expect. We discuss and compare two Coq
developments relating such balanced words to their inductive
characterizations. One is based on auxiliary inductive
structures and elementary arguments. The other one is based on
a discrete variant of the intermediate value theorem.},
year = 2006
}
@incollection{monin06:_iste,
author = {Jean-Fran\c{c}ois Monin and Philippe Chavin},
title = {{Coq}},
booktitle = {{Software Specification Methods, An Overview Using a Case Study}},
publisher = {Herm\`es Science},
url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=100},
abstract = {This chapter is an attempt to provide a formal
specification which is as faithful as possible to the informal
one and consistent. The features of Coq are powerful enough to
make the specification both very abstract and executable. We
\emph{construct} mathematical structures or functions whenever
possible, instead of specifying them with axioms. If the
axiomatic way turns out better, we look for structures
satisfying the axioms we need. },
year = 2006,
editor = {H. Habrias and M. Frappier},
series = {ISTE},
chapter = 16,
isbn = {1905209347},
month = apr
}
@incollection{monincourant07:_tfp,
author = {Jean-Fran\c{c}ois Monin and Judica{\"e}l Courant},
title = {{Proving Termination Using Dependent Types: the Case of Xor-Terms}},
editor = {H. Nilsson},
booktitle = {{Trends in Functional Programming 7}},
pages = {1-18},
chapter = 1,
publisher = {Intellect},
address = {Bristol, UK / Chicago, USA},
year = 2007,
ps = {http://www-verimag.imag.fr/~monin/Publis/tfp06.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/tfp06.pdf},
abstract = {We study a normalization function in
an algebra of terms quotiented by an associative,
commutative and involutive operator (logical xor).
This study is motivated by the formal verification of
cryptographic systems,
where a normalization function for xor-terms
turns out to play a key role.
Such a function is easy to define using general recursion.
However, as it is to be used in a type theoretic proof assistant,
we also need a proof termination of this function.
Instead of using a clever mixture of various rewriting orderings,
we follow an approach involving the power of
Type Theory with dependent types.
The results are to be applied in the proof
of the security API described in~\cite{courantmonin06wits}.},
month = apr
}
@inproceedings{courantmonin06wits,
author = {Judica{\"e}l Courant and Jean-Fran\c{c}ois Monin},
title = {Defending the bank with a proof assistant},
booktitle = {{WITS 2006}},
note = {In {WITS} proceedings},
year = 2006,
ps = {http://www-verimag.imag.fr/~monin/Publis/wits06.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/wits06.pdf},
abstract = {We show how the proof-assistant Coq helped us formally
verify the security of an API. As far as we know, this is the
first mathematical proof of security of an API. The API we
verified is a fixed version of Bond's modelization of IBM's Common
Cryptographic Architecture. We explain the methodology we
followed, sketch our proof and explain the points the formal
verification raised.},
address = {Vienna},
month = mar
}
@book{livre-mf-trad,
author = {J-F. Monin},
title = {Understanding Formal Methods},
publisher = {Springer Verlag},
note = {Foreword by G. Huet, ISBN 1-85233-247-6},
year = 2002,
abstract = {
This book is intended to help the student or the engineer who wants
an introduction to formal techniques, as well as the practitioner
who wishes to broaden her or his knowledge of this subject. It
mainly aims at providing a synthetic view of the logical foundations
of such techniques, with an emphasis on intuitive ideas, so that it
can also be considered as a practical complement to classical
introductory manuals to logic, which generally focus more detail on
specific subjects (e.g.\ first-order logic), and to books dedicated
to particular formal methods.}
}
@inproceedings{join_calcul_TT,
author = {J-F. Monin},
title = {Formalisation of the Join-Calculus in Type Theory},
booktitle = {International Worshop on Formal Methods and Security},
year = 2004,
month = may,
editor = {P-L. Curien and Song Fangmin},
address = {Nankin},
abstract = {
Towards verifying mobile code, we choose to formalize an
appropriate elementary model of concurrency in type theory (more
precisely: the calculus of inductive constructions, CIC,
implemented in the Coq proof assistant).
The chosen process calculus is the Join-Calculus (JC) of Fournet,
Gonthier and Levy. The latter can be seen as a variant of the
pi-calculus of Milner, Parrow and Walker, with better locality
properties. We use Coq for encoding a structural operational
semantics of JC based on the reflexive chemical abstract machines
model. Our formalisation uses the full power of inductive
constructions and dependent types available in the underlying
theory of Coq, in order to capture the reflexive features of JC.
}
}
@incollection{tphols04,
author = {J-F. Monin},
title = {{Proof pearl: From concrete to functional unparsing}},
booktitle = {{Theorem Proving in Higher Order Logics
(17th International Conference on TPHOLs 2004)}},
pages = {217--224},
publisher = {Springer Verlag},
month = {September},
address = {Park City, Utah, USA},
year = 2004,
editor = {K. Slind and A. Bunker and G. Gopalakrishnan},
volume = 3223,
series = {LNCS},
ps = {http://www-verimag.imag.fr/~monin/Publis/tphols04.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/tphols04.pdf},
abstract = {We provide a proof that the elegant trick of Olivier
Danvy for expressing printf-like functions without dependent types
is correct, where formats are encoded by functional expressions in
continuation-passing style. Our proof is formalized in the
Calculus of Inductive Constructions. We stress a methodological
point: when one proves equalities between functions, a common
temptation is to introduce a comprehension axiom and then to prove
that the considered functions are extensionally equal. Rather
than weakening the result (and adding an axiom), we prefer to
strenghten the inductive argumentation in order to stick to the
intensional equality.}
}
@inproceedings{courantmonin06jfla,
author = {Judica{\"e}l Courant and Jean-Fran\c{c}ois Monin},
title = {Faire garder la banque par un {C}oq},
booktitle = {Actes des dix-septi{\`{e}}mes journ{\'{e}}es francophones des langages applicatifs},
year = 2006,
month = jan,
pages = {25 -- 39},
ps = {http://www-verimag.imag.fr/~monin/Publis/jfla06.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/jfla06.pdf},
abstract = {Nous d\'ecrivons comment Coq nous a permis de d\'emontrer
math\'ematiquement et formellement la s\'ecurit\'e d'une interface
de programmation de s\'ecurit\'e. \`A notre connaissance il s'agit
de la premi\`ere d\'emonstration math\'ematique de s\'ecurit\'e
d'une interface de programmation. Nous pr\'esentons bri\`evement
notre d\'emonstration et expliquons les difficult\'es
rencontr\'ees lors du processus de formalisation.}
}
@article{fmsd-abr03,
author = {B.~B\'erard and L. Fribourg and F.~Klay and J-F.~Monin},
title = {A compared study of two correctness proofs for
the standardized algorithm of {ABR} conformance},
journal = {{Formal Methods in System Design}},
year = 2003,
volume = 22,
month = jan,
pages = {59--86},
ps = {http://www-verimag.imag.fr/~monin/Publis/fmsd-bfkm03.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/fmsd-bfkm03.pdf},
abstract = {The ABR conformance protocol is a real-time program that
controls data ow rates on ATM networks. A crucial part of this
protocol is the dynamical computation of the expected rate of
data cells. We present here a modelling of the corresponding
program with its environment, using the notion of (parametric)
timed automata. A fundamental property of the service provided
by the protocol to the user is expressed in this framework and
proved by two di erent methods. The rst proof relies on
inductive invariants, and was originally veri ed using theorem-
proving assistant Coq. The second proof is based on reachability
analysis, and was obtained using model-checker HyTech. We
explain and compare these two proofs in the uni ed framework of
timed automata.}
}
@article{fmsd-abr00,
author = {J-F.~Monin},
title = {Proving the Correctness of
the Standardized Algorithm for {ABR} conformance},
journal = {{Formal Methods in System Design}},
year = 2000,
volume = 17,
month = dec,
pages = {221--243},
ps = {http://www-verimag.imag.fr/~monin/Publis/fmsd-abr00.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/fmsd-abr00.pdf},
abstract = {Conformance control for ATM cells is based on a
real-time reactive algorithm which delivers a value depending on
inputs from the network. This value must always fit with a well
defined theoretical value. We present here the correctness proof
of the algorithm standardized for the ATM transfer capability
called ABR. The proof turned out to produce a key argument
during the standardization process of ABR.}
}
@incollection{Monin-Klay-abr-99,
author = {J-F. Monin and F. Klay},
title = {{Correctness Proof of the Standardized Algorithm for
ABR Conformance}},
booktitle = {{FM'99 -- Formal Methods}},
publisher = {Springer Verlag},
ps = {http://www-verimag.imag.fr/~monin/Publis/fm99-abr.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/fm99-abr.pdf},
abstract = {Conformance control for ATM cells is based on a
real-time reactive algorithm which delivers a value
depending on inputs from the network. This value must
always agree with a well defined theoretical value. We
present here the correctness proof of the algorithm
standardized for the ATM transfer capability called ABR.
The proof turned out a key argument during the
standardization process of ABR.},
year = 1999,
editor = {Jeannette Wing and Jim Woodcock and Jim Davies},
volume = 1708,
pages = {662--681},
series = {LNCS}
}
@incollection{jfm-abr-98,
author = {J-F. Monin},
title = {{Proving a real time algorithm for ATM in Coq}},
booktitle = {{Types for Proofs and Programs}},
publisher = {Springer Verlag},
ps = {http://www-verimag.imag.fr/~monin/Publis/types97.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/types97.pdf},
abstract = {This paper presents the techniques used for proving, in
the framework of type theory, the correctness of an
algorithm recently standardized at ITU-T that handles
time explicitly. The structure of the proof and its
formalization in Coq are described, as well as the main
tools which have been developed: an abstract model of
``real-time'' that makes no assumption on the nature of
time and a way to actually find proofs employing
transitivity, using only logical definitions and an
existing tactic.},
year = 1998,
editor = {E. Gimenez and C. Paulin-Mohring},
volume = 1512,
pages = {277--293},
series = {LNCS}
}
@incollection{facit-invoice,
author = {P. Chavin and J-F. Monin},
editor = {Marc Frappier and Henri Habrias},
booktitle = {Software Specification Methods},
title = {{An Abstract and constructive specification in Coq}},
chapter = 13,
publisher = {Springer Verlag},
year = 2000,
series = {FACIT}
}
@article{jfm-scp-96,
author = {J-F. Monin},
title = {{Exceptions considered harmless}},
journal = {{Science of Computer Programming}},
ps = {http://www-verimag.imag.fr/~monin/Publis/scp96.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/scp96.pdf},
abstract = {Program extraction is a well known technique for
developing correct functional programs from a
constructive proof of their specification. This paper
shows how to deal with exceptions in such a framework.
We propose a modular (and impredicative) formalization
in the calculus of constructions and we illustrate the
technique on three examples.},
year = 1996,
volume = 26,
pages = {179--196}
}
@incollection{jfm-mpc-95,
author = {J-F. Monin},
title = {{Extracting Programs with Exceptions
in an Impredicative Type System}},
booktitle = {{Mathematics of Program Construction}},
publisher = {Springer Verlag},
ps = {http://www-verimag.imag.fr/~monin/Publis/mpc95.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/mpc95.pdf},
abstract = {This paper is about exceptions handling using classical
techniques of program extraction. We propose an
impredicative formalization in the calculus of
constructions and we illustrate the technique on two
examples. The first one, though simple, allows us to
experiment various techniques. The second one is an
adaptation of a bigger algorithm previously developed in
Coq by J. Rouyer, namely first order unification. Only
small changes were needed in order to get a more
efficient program from the original one.},
year = 1995,
editor = {B. M{\"o}ller},
volume = 947,
series = {LNCS}
}
@article{JMG-ieee-88,
author = {C. Jard and J-F. Monin and R. Groz},
title = {Development of {V}eda, a {P}rototyping {T}ool for
{D}istributed {A}lgorithms},
journal = {IEEE Transactions on Software Engineering},
volume = 14,
number = 3,
pages = {339--352},
month = mar,
year = 1988,
keywords = {Parallel Programming},
abstract = { The development of a simulator, called Veda, is
described. Veda is a software tool to help designers in
protocol modeling and validation. It is oriented towards the
rapid prototyping of distributed algorithms. Algorithms are
described using an ISO (International Organisation for
Standardization) formal description technique, called
Estelle. The development of Veda and its internal structure is
presented, emphasizing the use of Prolog as a software
engineering tool. Typical uses of Veda are discussed.}
}
@inproceedings{JaGrMo-86,
author = {C. Jard and R. Groz and J-F. Monin},
title = {V\'eda: a {}Software {S}imulator for the {V}alidation of
{P}rotocol {S}pecifications},
editor = {L. Csaba and K. Tarnay and T. Szentivanyi},
booktitle = {COMNET'85, Computer Network Usage: Recent Experiences},
year = 1986,
publisher = {North Holland},
address = {Budapest}
}
@inproceedings{JaMoGr-86,
author = {C. Jard and J-F. Monin and R. Groz },
title = {Experience in implementing {X250} (a {CCITT} Subset of
{Estelle})},
booktitle = {IFIP Workshop V on Protocol Specification Testing
and Verification},
publisher = {North Holland},
year = 1986,
editor = {M. Diaz}
}
@inproceedings{jfm-plilp-88,
author = {J-F. Monin},
title = {A Compiler Written in {P}rolog: the {V}\'eda Experience},
booktitle = {Programming Languages Implementation and Logic Programming},
publisher = {Springer Verlag},
year = 1989,
editor = {Deransart and Lorho and Maluszynski},
number = 348,
series = {LNCS},
address = {Orl\'eans}
}
@inproceedings{glmphrcl-89,
author = {R. Groz and M. Litime and J-F. Monin and M. Phalippou
and C. Herv\'e and P. Riou and P. Cousin and J. Le
Compagnon},
title = {Elements of a {C.A.S.E.} Environment for Defining and
Generating Test Suites},
booktitle = {Int. Work. on Prot. Test Syst},
year = 1989,
address = {Berlin}
}
@inproceedings{jfm-iclp-91,
author = {J-F. Monin},
title = {Real-size Compiler Writing Using {P}rolog with
Arrows},
pages = {188--201},
booktitle = {Proceedings of the Eighth International Conference on
Logic Programming},
abstract = {Since the seminal paper of Colmerauer (1975) on
metamorphosis grammars, Prolog has been recognised as a
potentially interesting language for writing compilers.
However very few real size compilers have been written
in Prolog until now. We describe here such an
experiment, called Veda, carried out at CNET since 1984,
in which an Estelle compiler-simulator for protocol
checking was successfully developed. We sketch the (to
our knowledge original) techniques which were introduced
in Veda for enhancing performances up to a usable level,
while keeping clarity, flexibility and declarativity in
the programming style. One of them, based on
``arrows'', has applications in a class of problems
independant from compilation.},
year = 1991,
editor = {Koichi Furukawa},
publisher = {The MIT Press},
address = {Paris, France}
}
@inproceedings{GdJfm-fme-93,
author = {G. Doumenc and J-F. Monin},
title = {The Parallel Abstract Machine : A Common Execution
Model for {FDT}s},
booktitle = {FME'93 : Industrial-Strength Formal Methods},
publisher = {Springer Verlag},
abstract = {We introduce a new execution model for implementing FDTs
based on the reactive approach. In this model, called
the {\em PAM}, systems are divided into several reactive
entities communicating by an activation mechanism. This
paper introduces the {\em PAM} approach and shows how
different communication mechanisms such as asynchronous
fifo in {\em ESTELLE} or multiple rendez-vous in {\em
LOTOS} can be implemented. It then presents the analysis
of an implementation of a transport protocol (CCITT T70).},
year = 1993,
volume = 670,
series = {LNCS}
}
@inproceedings{jfm-prol-84,
author = {J-F. Monin},
title = {\'Ecriture d'un compilateur r\'eel en {P}rolog},
booktitle = {S\'eminaire sur la programmation en logique},
year = 1984,
editor = {S. Bourgault and M. Dincbas},
address = {Plestin}
}
@inproceedings{aya-estelle,
author = {J-M. Ayache and R. Groz and C. Jard and J-F. Monin},
title = {Des outils pour {Estelle} : du prototype au poste industriel},
booktitle = {Journ\'ees francophones pour l'informatique},
year = 1987,
month = jan,
note = {Li\`ege}
}
@inproceedings{ZhMo-cfip-88,
author = {W. Zhang and J-F. Monin},
title = {R\'esultats et exp\'eriences sur un environnement de
simulation pour l'\'evaluation de performances \`a
partir d'{Estelle}},
booktitle = {Colloque Francophone sur l'Ing\'enierie des Protocoles},
year = 1988,
editor = {R. Castanet and O. Rafiq},
address = {Bordeaux}
}
@incollection{jfm-c3-85,
author = {J-F. Monin},
title = {Terminaison distribu\'ee et groupes commutatifs},
booktitle = {Parall\'elisme, communication et synchronisation},
publisher = {\'editions du CNRS},
year = 1985,
editor = {J-P. Verjus and G. Roucairol}
}
@book{condillac,
author = {M. Condillac},
title = {Prolog, fondements et applications},
publisher = {Dunod},
year = 1986,
note = {r\'edacteur de deux chapitres}
}
@book{livref,
editor = {F. du Castel},
title = {{L}es {t\'el\'ecommunications}},
publisher = {Roger Levrault Int.},
year = 1993,
note = {contribution au chapitre informatique}
}
@article{BCM-95,
author = {P. Bellot and J.-P. Cottin and
J-F. Monin},
title = {{D\'eveloppement et validation de logiciels.
M\'ethodes formelles}},
journal = {{Techniques de l'Ing\'enieur}},
year = 1995,
number = 12,
pages = {1--12}
}
@inbook{ofta-97,
author = {J-F. Monin and J. Sifakis},
title = {Application des techniques formelles au logiciel},
chapter = {II, El\'ements de classification des m\'ethodes formelles},
publisher = {OFTA},
year = 1997,
volume = 20,
series = {Arago}
}
@phdthesis{jfm-these,
author = {J-F. Monin},
title = {Programmation en logique et compilation de
protocoles : le simulateur V\'eda},
school = {Universit\'e de Rennes I},
type = {Th\`ese d'universit\'e},
year = 1989,
month = jan
}
@phdthesis{jfm-hdr,
author = {J-F. Monin},
title = {Contribution aux m\'ethodes formelles pour le logiciel},
school = {Universit\'e de Paris Sud},
type = {M\'emoire d'habilitation \`a diriger des recherches},
ps = {http://www-verimag.imag.fr/~monin/Publis/hdr.ps},
pdf = {http://www-verimag.imag.fr/~monin/Publis/hdr.pdf},
year = 2002,
month = apr
}
This file was generated by bibtex2html 1.95.