complete-conference.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -q -oc complete-conference.cite -ob complete-conference.bib -c 'topics : "team" and $type="inproceedings" and year>=2004' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{castagna08icfp,
author = {Giuseppe Castagna and Kim Nguyen},
title = {Typed iterators for {XML}},
booktitle = {ICFP},
year = {2008},
pages = {15--26},
ee = {http://doi.acm.org/10.1145/1411204.1411210},
crossref = {icfp08},
bibsource = {DBLP, http://dblp.uni-trier.de},
topics = {team}
}
@inproceedings{jacobs04amast,
author = {Bart Jacobs and Claude March{\'e} and Nicole Rauch},
title = {Formal Verification of a Commercial Smart Card Applet with
Multiple Tools},
crossref = {amast04},
year = 2004,
topics = {team}
}
@inproceedings{barthe05fast,
author = {G. Barthe and T. Rezk and A. Saabas},
title = {{Proof obligations preserving compilation}},
year = 2005,
crossref = {fast05},
pdfurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk//publication/Barthe-Rezk-Saabas.pdf},
pages = {112-126},
topics = {team}
}
@inproceedings{jeannerod17jfla,
author = {Nicolas Jeannerod},
title = {Le coquillage dans le {CoLiS}-mateur: formalisation d'un langage de programmation de type {Shell}},
crossref = {jfla17}
}
@inproceedings{boldo15icfem,
title = {{Formal Verification of Programs Computing the Floating-Point Average}},
author = {Sylvie Boldo},
hal = {https://hal.inria.fr/hal-01174892},
booktitle = {{17th International Conference on Formal Engineering Methods}},
address = {Paris, France},
publisher = {{Springer}},
year = {2015},
month = nov,
pdf = {https://hal.inria.fr/hal-01174892/file/article.pdf},
topics = {team,lri},
type_publi = {irevcomlec},
editor = {Michael Butler and Sylvain Conchon and Fatiha Za\"idi},
volume = {9407},
series = {Lecture Notes in Computer Science},
pages = {17--32}
}
@inproceedings{bol15nsv,
author = {Sylvie Boldo},
title = {Stupid is as Stupid Does: Taking the Square Root of the Square
of a Floating-Point Number},
booktitle = {Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification},
pages = {50--55},
year = {2015},
editor = {Sergiy Bogomolov and Matthieu Martel},
series = {Electronic Notes in Theoretical Computer Science},
address = {Seattle, WA, USA},
month = apr,
hal = {http://hal.inria.fr/hal-01148409},
topics = {team,lri},
type_publi = {irevcomlec},
doi = {http://dx.doi.org/10.1016/j.entcs.2015.10.004},
volume = {317}
}
@inproceedings{boldo14scan,
hal = {https://hal.inria.fr/hal-01088692},
title = {Formal verification of tricky numerical computations},
author = {Sylvie Boldo},
year = 2014,
booktitle = {16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
address = {Würzburg, Germany},
month = sep,
note = {Invited talk},
url = {http://www.scan2014.uni-wuerzburg.de/book_of_abstracts/},
topics = {team,lri},
type_publi = {colloque}
}
@inproceedings{Lelay13,
hal = {http://hal.inria.fr/hal-00880212},
author = {Catherine Lelay},
title = {{A New Formalization of Power Series in Coq}},
booktitle = {5th Coq Workshop},
pages = {1--2},
year = {2013},
address = {Rennes, France},
month = jul,
note = {\url{http://coq.inria.fr/coq-workshop/2013#Lelay}},
topics = {team}
}
@inproceedings{benzaken14esop,
hal = {http://hal.inria.fr/hal-00924156},
author = {V\'eronique Benzaken and \'Evelyne Contejean and Stefania Dumbrava},
title = {A {Coq} Formalization of the Relational Data Model},
crossref = {esop2014},
year = 2014,
month = apr,
editor = {Z. Shao},
booktitle = {European Symposium on Programming, LNCS 8410},
pages = {189-208},
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes}
}
@inproceedings{benzaken08ppdp,
author = {V. Benzaken and G.Castagna and D. Colazzo and C. Miachon},
title = {Pattern by Example: Type-driven Visual Programming of {XML} Queries".},
booktitle = {10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming},
year = 2008,
address = {Valencia, Spain},
month = {July},
publisher = {ACM Press},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {PPDP},
x-proceedings = {yes},
x-international-audience = {yes}
}
@inproceedings{conchon11tacas,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Canonized Rewriting and Ground AC Completion Modulo Shostak Theories}},
crossref = {tacas2011},
year = 2011,
month = apr,
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {TACAS},
url = {http://proval.lri.fr/publications/conchon11tacas.pdf},
hal = {http://hal.inria.fr/hal-00777663},
pages = {45-59},
doi = {10.1007/978-3-642-19835-9_6},
abstract = {http://www.lri.fr/~contejea/publis/2011tacas/abstract.html}
}
@inproceedings{conchon10lpar,
author = {Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala},
title = {{Ground Associative and Commutative Completion Modulo Shostak Theories}},
booktitle = {LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = 2010,
editor = {Andrei Voronkov},
series = {EasyChair Proceedings},
address = {Yogyakarta, Indonesia},
month = oct,
note = {(short paper)},
type_publi = {colloque},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {LPAR}
}
@inproceedings{maneth10vldb,
author = {Sebastian Maneth and
Kim Nguyen},
title = {XPath Whole Query Optimization},
booktitle = {36th International Conference on Very Large Data Bases (VLDB'2010)},
pages = {882--893},
year = 2010,
volume = 3,
number = 1,
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {VLDB}
}
@inproceedings{benzaken11icde,
author = {V\'eronique Benzaken and Jean-Daniel Fekete and Pierre-Luc H\'emery and Wael Khemiri and Ioana Manolescu},
title = {{EdiFlow: data-intensive interactive workflows for visual analytics}},
year = {2011},
booktitle = {{International Conference on Data Engineering (ICDE)}},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {ICDE},
x-proceedings = {yes},
x-international-audience = {yes},
hal = {http://hal.inria.fr/inria-00532552},
crossref = {icde11}
}
@inproceedings{andronick05,
author = {June Andronick and Boutheina Chetali and Paulin-Mohring, Christine},
title = {Formal Verification of Security Properties of Smart Card Embedded Source Code},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {FME},
crossref = {fm05}
}
@inproceedings{andronick06,
author = {June Andronick and Boutheina Chetali},
title = {{An Environment for Securing Smart
Cards Embedded C Code}},
year = {2006},
booktitle = {{International Conference on Research in
Smart Cards (Esmart'06)}},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes}
}
@inproceedings{audebaud06mpc,
author = {Philippe Audebaud and Christine Paulin-Mohring},
title = {Proofs of Randomized Algorithms in {Coq}},
crossref = {mpc2006},
x-equipes = {demons PROVAL EXT},
x-pdf = {http://www.lri.fr/~paulin/ALEA/article.pdf},
url = {http://www.lri.fr/~paulin/ALEA/article.pdf},
x-type = {article},
x-support = {actes},
x-cle-support = {MPC},
topics = {team},
type_publi = {icolcomlec},
year = 2006
}
@inproceedings{Biernacka07wrs,
author = {Malgorzata Biernacka and Dariusz Biernacki},
title = {{Formalizing Constructions of Abstract Machines for Functional Languages in {Coq}}},
booktitle = {{7th International Workshop on Reduction
Strategies in Rewriting and Programming (WRS 2007)}},
year = 2007,
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
address = {Paris, France},
month = jun,
pages = {84--99},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-pdf = {http://www.lsv.ens-cachan.fr/rdp07/WRSproceedings.pdf},
url = {http://www.lsv.ens-cachan.fr/rdp07/WRSproceedings.pdf},
topics = {team, lri}
}
@inproceedings{Biernacki07apges,
author = {Dariusz Biernacki and Jean-Louis Cola\c{c}o and Marc Pouzet},
title = {{Clock-directed Modular Code Generation from Synchronous Block Diagrams}},
booktitle = {{Workshop on Automatic Program Generation for Embedded
Systems (APGES 2007)}},
year = 2007,
address = {Salzburg, Austria},
month = {October},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-pdf = {http://www-fp.dcs.st-and.ac.uk/APGES/OnlineProceedings/11-Pouzet.pdf},
url = {http://www-fp.dcs.st-and.ac.uk/APGES/OnlineProceedings/11-Pouzet.pdf},
topics = {team, lri}
}
@inproceedings{Bol06,
author = {Sylvie Boldo},
title = {Pitfalls of a full floating-point proof: example on the formal proof of the {Veltkamp/Dekker} algorithms},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
pages = {52-66},
x-pdf = {http://www.lri.fr/~sboldo/files/ijcar06.pdf},
url = {http://www.lri.fr/~sboldo/files/ijcar06.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
crossref = {ijcar06}
}
@inproceedings{BolMun06,
author = {Sylvie Boldo and C\'esar Mu{\~n}oz},
title = {Provably Faithful Evaluation of Polynomials},
booktitle = {Proceedings of the 21st Annual ACM Symposium on Applied Computing},
year = {2006},
month = apr,
address = {Dijon, France},
topics = {team},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
volume = 2,
hal = {http://hal.inria.fr/inria-00050232/en/},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {SAC},
pages = {1328-1332}
}
@inproceedings{BoldoFilliatre07,
author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
doi = {10.1109/ARITH.2007.20},
title = {Formal Verification of Floating-Point Programs},
booktitle = {18th IEEE International Symposium on Computer Arithmetic},
pages = {187--194},
x-month = jun,
year = 2007,
x-address = {Montpellier, France},
topics = {team,lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus-floats.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus-floats.pdf},
abstract = {
This paper introduces a methodology to perform formal verification
of floating-point C programs. It extends an existing tool for the
verification of C programs, Caduceus, with new annotations specific
to floating-point arithmetic. The Caduceus first-order logic model
for C programs is extended accordingly. Then verification conditions
expressing the correctness of the programs are obtained in the usual
way and can be discharged interactively with the Coq proof
assistant, using an existing Coq formalization of floating-point
arithmetic. This methodology is already implemented and has been
successfully applied to several short floating-point programs, which
are presented in this paper.}
}
@inproceedings{conchon05jfla,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
title = {Le foncteur sonne toujours deux fois},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla05},
pages = {79--94},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jfla05.ps.gz}
}
@inproceedings{conchon07afm,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St{\'e}phane Lescuyer},
title = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
crossref = {afm07},
abstract = {Ergo is a little engine of proof dedicated to program
verification. It fully supports quantifiers and directly handles
polymorphic sorts. Its core component is CC(X), a new combination
scheme for the theory of uninterpreted symbols parameterized by a
built-in theory X. In order to make a sound integration in a proof
assistant possible, Ergo is capable of generating proof traces
for CC(X). Alternatively, Ergo can also be called interactively
as a simple oracle without further verification. It is currently
used to prove correctness of C and Java programs as part of the Why
platform.},
abstract = {http://www.lri.fr/~contejea/publis/2007afm/abstract.html},
topics = {team,lri},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {AFM},
x-pdf = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
url = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
doi = {10.1145/1345169.1345176},
pages = {55--59}
}
@inproceedings{conchon07smt,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig},
title = {{CC(X)}: Efficiently Combining Equality and Solvable Theories without Canonizers},
booktitle = {SMT 2007: 5th International Workshop on Satisfiability Modulo},
year = 2007,
editor = {Sava Krstic and Albert Oliveras},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT}
}
@inproceedings{conchon08smt,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
and St\'ephane Lescuyer},
title = {{Implementing Polymorphism in SMT solvers}},
booktitle = {SMT 2008: 6th International Workshop on Satisfiability Modulo},
pages = {1--5},
year = 2008,
editor = {Clark Barrett and Leonardo de Moura},
volume = 367,
series = {ACM International Conference Proceedings Series},
topics = {team,lri},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SMT},
x-pdf = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
url = {http://www.lri.fr/~conchon/publis/conchon-smt08.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
isbn = {978-1-60558-440-9},
doi = {10.1145/1512464.1512466},
abstract = {http://www.lri.fr/~contejea/publis/2008smt/abstract.html}
}
@inproceedings{conchon07tfp,
author = {Sylvain Conchon and
Jean-Christophe Filli\^atre and
Julien Signoles},
title = {{Designing a Generic Graph Library using {ML} Functors}},
booktitle = {The Eighth Symposium on Trends in Functional Programming},
editor = {Marco T. Moraz\'an and Henrik Nilsson},
publisher = {Seton Hall University},
volume = {TR-SHU-CS-2007-04-1},
pages = {XII/1--13},
year = 2007,
address = {New York, USA},
month = apr,
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
abstract = {
This paper details the design and implementation of Ocamlgraph, a
highly generic graph library for the programming language Ocaml.
This library features a large set of graph data
structures---directed or undirected, with or without labels on
vertices and edges, as persistent or mutable data structures,
etc.---and a large set of graph algorithms. Algorithms are written
independently from graph data structures, which allows combining
user data structure (resp. algorithm) with Ocamlgraph algorithm
(resp. data structure). Genericity is obtained through massive use
of the Ocaml module system and its functions, the so-called
functors.},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp07.ps},
topics = {team, lri},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-editorial-board = {yes}
}
@inproceedings{conchon08tfp,
author = {Sylvain Conchon and
Jean-Christophe Filli\^atre and
Julien Signoles},
title = {Designing a Generic Graph Library using {ML} Functors},
booktitle = {Trends in Functional Programming (TFP'07)},
month = {April},
year = 2007,
address = {New York City, USA},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {TFP},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{conchon08entcs,
author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St\'ephane Lescuyer},
title = {{CC(X)}: Semantical Combination of Congruence Closure with
Solvable Theories},
booktitle = {Post-proceedings of the 5th International Workshop on
Satisfiability Modulo Theories ({SMT 2007})},
series = {Electronic Notes in Computer Science},
publisher = {Elsevier Science Publishers},
volume = {198(2)},
pages = {51--69},
year = 2008,
abstract = {
We present a generic congruence closure algorithm for deciding
ground formulas in the combination of the theory of equality with
uninterpreted symbols and an arbitrary built-in solvable theory X.
Our algorithm CC(X) is reminiscent of Shostak combination: it
maintains a union-find data-structure modulo X from which maximal
information about implied equalities can be directly used for
congruence closure. CC(X) diverges from Shostak's approach by the use
of semantical values for class representatives instead of canonized
terms. Using semantical values truly reflects the actual
implementation of the decision procedure for X. It also enforces to
entirely rebuild the algorithm since global canonization, which is
at the heart of Shostak combination, is no longer feasible with
semantical values. CC(X) has been implemented in Ocaml and is at
the core of Ergo, a new automated theorem prover dedicated to
program verification.
},
abstract = {http://www.lri.fr/~contejea/publis/2008entcs/abstract.html},
topics = {team},
type_publi = {irevcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-cle-support = {ENTCS},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
doi = {10.1016/j.entcs.2008.04.080}
}
@inproceedings{Conchon08jfla,
author = {Sylvain Conchon and Johannes Kanig and St\'ephane Lescuyer},
title = {{SAT-MICRO : petit mais costaud !}},
year = 2008,
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
x-editorial-board = {yes},
x-international-audience = {no},
x-proceedings = {yes},
crossref = {jfla08},
address = {\'Etretat, France},
publisher = {INRIA},
url = {http://www.lri.fr/~conchon/publis/conchon-jfla08.ps},
abstract = {
Le probl\`eme SAT, qui consiste `a d\'eterminer si une formule bool\'eenne
est satisfaisable, est un des probl\`emes NP-complets les plus
c\'el\`ebres et aussi un des plus \'etudi\'es. Bas\'es initialement sur la
proc\'edure DPLL, les SAT-solvers modernes ont connu des
progr\`es spectaculaires ces dix derni\`eres ann\'ees dans leurs
performances, essentiellement gr\^ace \`a deux optimisations: le retour
en arri\`ere non-chronologique et l'apprentissage par analyse des
clauses conflits. Nous proposons dans cet article une \'etude formelle
du fonctionnement de ces techniques ainsi qu'une r\'ealisation en Ocaml
d'un SAT-solver, baptis\'e SAT-MICRO, int\'egrant ces
optimisations. Le fonctionnement de SAT-MICRO est d\'ecrit par un
ensemble de r\`egles d'inf\'erence et la taille de son code, 70 lignes
au total, permet d'envisager sa certification compl\`ete.}
}
@inproceedings{ConchonFilliatre06wml,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Type-Safe Modular Hash-Consing}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
month = sep,
year = 2006,
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing2.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/hash-consing2.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre07jfla,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Union-Find Persistant}},
year = 2007,
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla07},
pages = {135--149},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
abstract = {
Le probl\`eme des classes disjointes, connu sous le nom de
\emph{union-find}, consiste \`a maintenir dans une structure de
donn\'ees une partition d'un ensemble fini. Cette structure fournit deux
op\'erations : une fonction \emph{find} d\'eterminant la classe d'un
\'el\'ement et une fonction \emph{union} r\'eunissant deux classes. Une
solution optimale et imp\'erative, due \`a Tarjan, est connue depuis
longtemps.
Cependant, le caract\`ere imp\'eratif de cette structure de donn\'ees
devient g\^enant lorsqu'elle est utilis\'ee dans un contexte o\`u
s'effectuent des retours en arri\`ere (\emph{backtracking}). Nous
pr\'esentons dans cet article une version persistante de
\emph{union-find} dont la complexit\'e est comparable \`a celle de la
solution imp\'erative. Pour obtenir cette efficacit\'e, notre solution
utilise massivement des traits imp\'eratifs. C'est pourquoi nous
pr\'esentons \'egalement une preuve formelle de correction, pour
s'assurer notamment du caract\`ere persistant de cette solution.
}
}
@inproceedings{ConchonFilliatre07wml,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{A Persistent Union-Find Data Structure}},
booktitle = {ACM SIGPLAN Workshop on ML},
publisher = {ACM Press},
pages = {37--45},
year = 2007,
address = {Freiburg, Germany},
month = {October},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf-wml07.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/puf-wml07.pdf},
abstract = { The problem of disjoint sets, also known as union-find,
consists in maintaining a partition of a finite set within a data
structure. This structure provides two operations: a function find
returning the class of an element and a function union merging two
classes. An optimal and imperative solution is known since 1975.
However, the imperative nature of this data structure may be a
drawback when it is used in a backtracking algorithm. This paper
details the implementation of a persistent union-find data structure
as efficient as its imperative counterpart. To achieve this result,
our solution makes heavy use of imperative features and thus it is a
significant example of a data structure whose side effects are
safely hidden behind a persistent interface. To strengthen this
last claim, we also detail a formalization using the Coq proof
assistant which shows both the correctness of our solution and its
observational persistence. },
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{Filliatre08wml,
author = {Jean-Christophe Filli\^atre},
title = {{A Functional Implementation of the Garsia--Wachs Algorithm}},
booktitle = {ACM SIGPLAN Workshop on ML},
publisher = {ACM Press},
year = 2008,
address = {Victoria, British Columbia, Canada},
month = {September},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/gw-wml08.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/gw-wml08.pdf},
abstract = { This functional pearl proposes an ML implementation of
the Garsia--Wachs algorithm.
This somewhat obscure algorithm builds a binary tree with minimum
weighted path length from weighted leaf nodes given in symmetric
order. Our solution exhibits the usual benefits of functional
programming (use of immutable data structures, pattern-matching,
polymorphism) and nicely compares to the purely imperative
implementation from \emph{The Art of Computer Programming}.},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{ConchonFilliatre08esop,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
hal = {https://inria.hal.science/hal-04045849},
doi = {10.1007/978-3-540-78739-6_25},
title = {Semi-Persistent Data Structures},
crossref = {esop08},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-url = {https://usr.lmf.cnrs.fr/~jcf/publis/spds-rr.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{contejean04rta,
author = {\'Evelyne Contejean},
title = {{A certified AC matching algorithm}},
booktitle = {15th International Conference on Rewriting Techniques and Applications},
crossref = {rta04},
pages = {70--84},
year = 2004,
type_publi = {icolcomlec},
topics = {team},
doi = {10.1007/978-3-540-25979-4_5},
abstract = {http://www.lri.fr/~contejea/publis/2004rta/abstract.html}
}
@inproceedings{contejean05cade,
author = {\'Evelyne Contejean and Pierre Corbineau},
title = {Reflecting Proofs in First-Order Logic with Equality},
type_publi = {icolcomlec},
topics = {team},
pages = {7--22},
crossref = {cade05},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {CADE},
abstract = {http://www.lri.fr/~contejea/publis/2005cade/abstract.html},
doi = {10.1007/11532231_2}
}
@inproceedings{contejean07frocos,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
title = {Certification of automated termination proofs},
crossref = {frocos07},
pages = {148--162},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {FROCOS},
topics = {team},
doi = {10.1007/978-3-540-74621-8_10},
abstract = {http://www.lri.fr/~contejea/publis/2007frocos/abstract.html}
}
@inproceedings{contejean08wsct,
author = {\'Evelyne Contejean and Xavier Urbain},
title = {{The A3PAT approach}},
booktitle = { Workshop on Certified Termination WScT08},
year = 2008,
address = {Leipzig, Germany},
month = may,
topics = {team},
x-international-audience = {yes},
x-proceedings = {no}
}
@inproceedings{contejean08types,
author = {\'Evelyne Contejean},
title = {{Coccinelle, a Coq library for rewriting}},
booktitle = {Types},
year = 2008,
address = {Torino, Italy},
month = mar,
type_publi = {autre},
x-equipes = {demons PROVAL},
topics = {team},
x-international-audience = {yes},
x-proceedings = {no}
}
@inproceedings{contejean10pepm,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Andrei Paskevich and Olivier Pons and Xavier Urbain},
title = {{A3PAT, an Approach for Certified Automated Termination Proofs}},
crossref = {pepm10},
booktitle = {Partial Evaluation and Program Manipulation},
year = 2010,
month = jan,
pages = {63-72},
topics = {team},
x-equipes = {demons PROVAL},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {PEPM},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
topics = {team},
doi = {10.1145/1706356.1706370},
abstract = {http://www.lri.fr/~contejea/publis/2010pepm/abstract.html}
}
@inproceedings{contejean11rta,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
and Olivier Pons and Xavier Urbain},
crossref = {rta11},
title = {{Automated Certified Proofs with CiME3}},
x-equipes = {demons PROVAL ext},
url = {http://drops.dagstuhl.de/opus/volltexte/2011/3119},
hal = {http://hal.inria.fr/hal-00777669},
urn = {urn:nbn:de:0030-drops-31192},
doi = {10.4230/LIPIcs.RTA.2011.21},
pages = {21--30},
abstract = {http://www.lri.fr/~contejea/publis/2011rta/abstract.html},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {RTA},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
topics = {team}
}
@inproceedings{corbineau04,
author = {Pierre Corbineau},
title = {First-order reasoning in the {Calculus of Inductive Constructions}},
crossref = {types03},
booktitle = {TYPES 2003 : Types for Proofs and Programs},
pages = {162--177},
year = 2004,
editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
volume = 3085,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
topics = {team},
type_publi = {icolcomlec},
ps = {http://www.lri.fr/~corbinea/ftp/publis/types03.ps},
url = {http://www.lri.fr/~corbinea/ftp/publis/types03.ps}
}
@inproceedings{corbineau05jfla,
author = {Pierre Corbineau},
title = {Skip lists et arbres binaires de recherche probabilistes},
topics = {team,colcomlec},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla05},
pages = {99--112}
}
@inproceedings{couchot07ftp,
author = {Jean-Fran\c{c}ois Couchot and Thierry Hubert},
title = {{A Graph-based Strategy for the Selection of Hypotheses}},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {FTP},
booktitle = {FTP 2007 - International Workshop on
First-Order Theorem Proving},
address = {Liverpool, UK},
month = sep,
year = 2007,
pages = {},
x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
url = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
abstract = {In previous works on verifying
C programs by deductive approaches based on SMT provers,
we proposed the heuristic of separation analysis to handle the most
difficult problems.
Nevertheless, this heuristic is not sufficient when applied on
industrial C programs:
it remains some Verification Conditions (VCs) that cannot be decided
by any SMT prover, mainly due to their size.
This work presents a strategy to select relevant hypotheses
in each VC.
The relevance of an hypothesis is the combination of
two separated dependency analysis
obtained by some graph traversals.
The approach is applied on a benchmark issued from
an industrial program verification.
}
}
@inproceedings{couchot07cade,
author = {Jean-Fran\c{c}ois Couchot and St\'ephane Lescuyer},
title = {Handling Polymorphism in Automated Deduction},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {CADE},
pages = {263--278},
booktitle = {21th International Conference on Automated Deduction (CADE-21)},
address = {Bremen, Germany},
month = jul,
year = 2007,
series = {LNCS (LNAI)},
volume = 4603,
x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
url = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
abstract = {Polymorphism has become a common way of designing short and reusable
programs by abstracting generic definitions from type-specific ones.
Such a convenience is valuable in logic as well, because it unburdens
the specifier from writing redundant declarations of logical
symbols.
However,
top shelf automated theorem provers such as
Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To
this end, we present
efficient reductions of polymorphism in both unsorted and many-sorted
first order logics.
For each encoding, we show that the formulas and their encoded
counterparts are logically equivalent in the context of automated
theorem proving. The efficiency keynote is to disturb the prover as
little as possible, especially the internal decision procedures used for
special sorts, e.g. integer linear arithmetic, to which we apply a
special treatment.
The corresponding implementations are presented in the framework of
the Why/Caduceus
toolkit.}
}
@inproceedings{CouchotD07IFM,
author = {Jean-Fran\c{c}ois Couchot and
Fr\'ed\'eric Dadeau},
title = {Guiding the Correction of Parameterized Specifications},
booktitle = {Integrated Formal Methods},
publisher = {Springer},
address = {Oxford, UK},
month = jul,
topics = {team, lri},
series = {Lecture Notes in Computer Science},
volume = 4591,
pages = {176--194},
year = 2007,
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {IFM},
x-pdf = {http://www.lri.fr/~couchot/IMG/pdf/CD07.pdf},
url = {http://www.lri.fr/~couchot/IMG/pdf/CD07.pdf},
abstract = {
Finding inductive invariants is a key issue in many domains such as
program verification, model based testing, etc.
However, few approaches help the designer in the task of writing
a correct and meaningful model, where correction is used for
consistency of the formal specification w.r.t. its inner invariant
properties.
Meaningfulness is obtained by providing many explicit views of the model,
like animation, counter-example extraction, and so on.
We propose to ease the task of writing a correct and meaningful formal
specification
by combining a panel of provers,
a set-theoretical constraint
solver and some model-checkers.}
}
@inproceedings{duran04pepm,
author = {Francisco Dur{\'a}n and Salvador Lucas and Jos{\'e} Meseguer
and Claude March{\'e} and Xavier Urbain},
title = {Proving Termination of Membership Equational Programs},
crossref = {pepm04},
topics = {team},
type_publi = {icolcomlec}
}
@inproceedings{filliatre04icfem,
author = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
title = {Multi-Prover Verification of {C} Programs},
crossref = {icfem04},
year = {2004},
pages = {15--29},
topics = {team},
type_publi = {icolcomlec},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus.ps.gz}
}
@inproceedings{filliatre06jfla,
author = {Jean-Christophe Filli\^atre},
title = {It\'erer avec persistance},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla06},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/enum.ps.gz}
}
@inproceedings{filliatre07cav,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
Verification},
crossref = {cav07},
pages = {173--177},
topics = {team, lri},
hal = {https://hal.inria.fr/inria-00270820v1},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/cav07.pdf},
x-equipes = {demons PROVAL EXT},
x-type = {articlecourt},
x-support = {actes},
x-cle-support = {CAV},
doi = {10.1007/978-3-540-73368-3_21}
}
@inproceedings{Filliatre06wml,
author = {Jean-Christophe Filli\^atre},
title = {{Backtracking iterators}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
month = sep,
year = 2006,
topics = {team, lri},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/enum2.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/enum2.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML}
}
@inproceedings{Filliatre07corde,
author = {Jean-Christophe Filli\^atre},
title = {{Gagner en passant \`a la corde}},
year = 2008,
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
x-editorial-board = {yes},
x-international-audience = {no},
x-proceedings = {yes},
crossref = {jfla08},
address = {\'Etretat, France},
publisher = {INRIA},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/cordes.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/cordes.pdf},
abstract = {
Cet article pr\'esente une r\'ealisation en Ocaml de la structure de
cordes introduite par Boehm, Atkinson et Plass. Nous montrons
notamment comment cette structure de donn\'ees s'\'ecrit naturellement
comme un foncteur, transformant une structure de s\'equence en une
autre structure de m\^eme interface. Cette fonctorisation a de
nombreuses applications au-del\`a de l'article original. Nous en
donnons plusieurs, dont un \'editeur de texte dont les performances
sur de tr\`es gros fichiers sont bien meilleures que celles des
\'editeurs les plus populaires.}
}
@inproceedings{Filliatre07mix,
author = {Jean-Christophe Filli\^atre},
title = {{Formal Verification of MIX Programs}},
booktitle = {{Journ{\'e}es en l'honneur de Donald E. Knuth}},
year = 2007,
address = {Bordeaux, France},
month = {October},
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/verifmix.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/verifmix.pdf},
abstract = {We introduce a methodology to formally verify MIX programs.
It consists in annotating a MIX program with logical annotations
and then to turn it into a set of purely sequential programs on
which classical techniques can be applied.
Contrary to other approaches of verification of unstructured
programs, we do not impose the location of annotations but only the
existence of at least one invariant on each cycle in the control
flow graph. A prototype has been implemented and used to verify
several programs from \emph{The Art of Computer Programming}.},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux}
}
@inproceedings{FilliatreLetouzey04esop,
author = {Jean-Christophe Filli\^atre and Pierre Letouzey},
title = {{Functors for Proofs and Programs}},
booktitle = {Proceedings of The European Symposium on Programming},
year = 2004,
address = {Barcelona, Spain},
month = apr,
series = {Lecture Notes in Computer Science},
volume = 2986,
pages = {370--384},
topics = {team},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/fpp.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/fpp.pdf}
}
@inproceedings{hubert05sefm,
author = {Thierry Hubert and Claude March\'e},
topics = {team},
title = {A case study of {C} source code verification: the {Schorr-Waite} algorithm},
crossref = {sefm05},
type_publi = {icolcomlec},
url = {http://www.lri.fr/~marche/hubert05sefm.ps},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {SEFM}
}
@inproceedings{hubert07hav,
author = {Thierry Hubert and Claude March\'e},
title = {Separation Analysis for Deductive Verification},
booktitle = {Heap Analysis and Verification (HAV'07)},
year = 2007,
address = {Braga, Portugal},
month = mar,
topics = {team, lri},
hal = {https://hal.inria.fr/hal-03630177},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
pages = {81--93},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {HAV}
}
@inproceedings{labbe07,
author = {S\'ebastien Labb\'e and Jean-Pierre Gallois and
Marc Pouzet},
title = {Slicing Communicating Automata Specifications
For Efficient Model Reduction},
booktitle = {18th Australian Conference on Software Engineering (ASWEC)},
year = 2007,
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {ASWEC}
}
@inproceedings{MandelMaranget08esop,
author = {Louis Mandel and Luc Maranget},
title = {Programming in {JoCaml} (Tool Demonstration)},
crossref = {esop08},
year = 2008,
pages = {108--111},
x-pdf = {http://www.lri.fr/~mandel/papers/MandelMaranget-ESOP-2008.pdf},
url = {http://www.lri.fr/~mandel/papers/MandelMaranget-ESOP-2008.pdf},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{lucy:lctes09,
author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
and Marc Pouzet and Pascal Raymond},
title = {{Synchronous Objects with Scheduling Policies}:
Introducing safe shared memory in {Lustre}},
year = {2009},
month = jun,
address = {Dublin},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
x-type = {article},
topics = {team},
x-support = {actes},
x-equipes = {demons PROVAL ext}
}
@inproceedings{lucy:emsoft09,
author = {Marc Pouzet and Pascal Raymond},
title = {Modular Static Scheduling of Synchronous Data-flow
Networks: An efficient symbolic representation},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'09)},
address = {Grenoble, France},
month = {October},
year = 2009,
topics = {team},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext}
}
@inproceedings{marche07plpv,
author = {Claude March\'e},
title = {Jessie: an intermediate Language for {Java} and {C} Verification},
booktitle = {Programming Languages meets Program Verification (PLPV)},
year = {2007},
topics = { team},
isbn = {978-1-59593-677-6},
pages = {1--2},
doi = {10.1145/1292597.1292598},
publisher = {ACM Press},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {PLPV},
address = {Freiburg, Germany}
}
@inproceedings{filliatre08smt,
author = {Jean-Christophe Filli\^atre},
title = {{Using SMT solvers for deductive verification of C and Java programs}},
booktitle = {{SMT 2008: 6th International Workshop on Satisfiability Modulo}},
editor = {Clark Barrett and Leonardo de Moura},
year = 2008,
topics = { team},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes_aux},
x-cle-support = {SMT},
address = {Princeton, USA}
}
@inproceedings{filliatre09afm,
author = {Jean-Christophe Filli\^atre},
title = {{Invited tutorial: Why --- an intermediate language for deductive program verification}},
booktitle = {{Automated Formal Methods (AFM09)}},
editor = {Hassen Sa\"{\i}di and Natarajan Shankar},
year = 2009,
topics = { team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {AFM},
address = {Grenoble, France}
}
@inproceedings{marche07rta,
author = {March\'e, Claude and Zantema, Hans},
title = {The Termination Competition},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
crossref = {rta07},
pages = {303--313},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {RTA},
x-pdf = {http://www.lri.fr/~marche/marche07rta.pdf},
url = {http://www.lri.fr/~marche/marche07rta.pdf},
x-slides = {http://www.lri.fr/~marche/marche07rta-slides.pdf}
}
@inproceedings{marche07wst,
author = {Claude March{\'e} and Hans Zantema and Johannes Waldmann},
title = {The Termination Competition 2007},
crossref = {wst07},
topics = {team},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
url = {http://www.lri.fr/~marche/termination-competition/},
note = {\url{http://www.lri.fr/~marche/termination-competition/}},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {WST}
}
@inproceedings{MandelPlateau09_HFL,
address = {York, UK},
author = {Albert Cohen and Louis Mandel and Florence Plateau and Marc Pouzet},
booktitle = {Hardware Design using Functional languages (HFL 09)},
month = mar,
title = {Relaxing Synchronous Composition with Clock Abstraction},
year = {2009},
pages = {35-52},
x-international-audience = {yes},
x-proceedings = {yes},
topics = {team},
x-support = {actes_aux},
x-equipes = {demons PROVAL alchemy},
x-type = {article},
type_publi = {icolcomlec}
}
@inproceedings{MandelPlateauPouzet-DCC-10,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {Clock Typing of n-Synchronous Programs},
booktitle = {Designing Correct Circuits ({DCC 2010})},
year = 2010,
month = mar,
address = {Paphos, Cyprus},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {DCCircuits},
x-type = {article},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{Pouzet08c,
author = {Albert Cohen and Louis Mandel and Florence Plateau and
Marc Pouzet},
title = {{Abstraction of Clocks in Synchronous Data-flow Systems}},
booktitle = {The Sixth ASIAN Symposium on Programming Languages and Systems
(APLAS)},
abstract = { Synchronous data-flow languages such as Lustre manage infinite
sequences or streams as basic values. Each stream is
associated to a clock which defines the instants where the
current value of the stream is present. This clock is a type
information and a dedicated type system --- the so-called
clock-calculus --- statically rejects programs which cannot be
executed synchronously. In existing synchronous languages, it
amounts at asking whether two streams have the same clocks and thus
relies on clock equality only. Recent works have shown the interest
of introducing some relaxed notion of synchrony, where two streams can
be composed as soon as they can be synchronized through the
introduction of a finite buffer (as done in the SDF model of Edward
Lee). This technically consists in replacing typing by
subtyping. The present paper introduces a simple way to achieve
this relaxed model through the use of clock
envelopes. These clock envelopes are sets of concrete clocks which
are not necessarily periodic. This allows to model various features
in real-time embedded software such as bounded jitter as found in
video-systems, execution time of real-time processes and
scheduling resources or the communication through buffers. We
present the algebra of clock envelopes and its main theoretical
properties.},
x-pdf = {http://www.lri.fr/~plateau/papers/aplas08.pdf},
url = {http://www.lri.fr/~plateau/papers/aplas08.pdf},
year = 2008,
month = dec,
date = {9--11},
series = {Lecture Notes in Computer Science},
volume = {5356},
pages = {237--254},
address = {Bangalore, India},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {APLAS},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
topics = {team}
}
@inproceedings{Pouzet08b,
author = {Gwenael Delaval and Alain Girault and Marc Pouzet},
title = {{A Type System for the Automatic Distribution
of Higher-order Synchronous Dataflow Programs}},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
year = 2008,
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {LCTES},
address = {Tucson, Arizona},
month = jun,
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
topics = {team}
}
@inproceedings{Pouzet08a,
author = {Dariusz Biernacki and Jean-Louis Cola\c{c}o and Gr\'egoire Hamon
and Marc Pouzet},
title = {{Clock-directed Modular Code Generation of Synchronous Data-flow
Languages}},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
year = 2008,
address = {Tucson, Arizona},
month = jun,
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {LCTES},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
topics = {team}
}
@inproceedings{mandel05ppdp,
author = {Louis Mandel and Marc Pouzet},
title = {{ReactiveML, a Reactive Extension to ML}},
booktitle = {ACM International Conference
on Principles and Practice of Declarative Programming
(PPDP)},
year = 2005,
pages = {82--93},
x-pdf = {http://www.lri.fr/~mandel/papers/MandelPouzet-PPDP-2005.pdf},
url = {http://www.lri.fr/~mandel/papers/MandelPouzet-PPDP-2005.pdf},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {PPDP},
address = {Lisboa},
month = jul
}
@inproceedings{MandelPlateau2008SLAP,
author = {Louis Mandel and Florence Plateau},
title = {Interactive Programming of Reactive Systems},
booktitle = {Proceedings of Model-driven High-level Programming of Embedded Systems ({SLA++P'08})},
year = 2008,
month = apr,
address = {Budapest, Hungary},
pages = {44--59},
x-pdf = {http://www.lri.fr/~mandel/papers/MandelPlateau-SLAP-2008.pdf},
url = {http://www.lri.fr/~mandel/papers/MandelPlateau-SLAP-2008.pdf},
topics = {team},
type_publi = {icolcomlec},
series = {Electronic Notes in Computer Science},
publisher = {Elsevier Science Publishers},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ENTCS},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{MorelMandel2007FESCA,
author = {Lionel Morel and Louis Mandel},
title = {Executable Contracts for Incremental Prototypes of Embedded Systems},
booktitle = {Formal Foundations of Embedded Software
and Component-Based Software Architectures ({FESCA'07})},
month = mar,
year = 2007,
x-pdf = {http://www.lri.fr/~mandel/papers/MorelMandel-FESCA-2007.pdf},
url = {http://www.lri.fr/~mandel/papers/MorelMandel-FESCA-2007.pdf},
pages = {123--136},
topics = {team},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
serie = {Electronic Notes in Computer Science},
publisher = {Elsevier Science Publishers},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ENTCS}
}
@inproceedings{HalbwachsMandel2006ACSD,
author = {Nicolas Halbwachs and Louis Mandel},
title = {Simulation and verification of asynchronous systems by means of a synchronous model},
booktitle = {Sixth International Conference on Application of Concurrency to System Design ({ACSD'06})},
year = {2006},
address = {Turku, Finland},
month = jun,
pages = {3--14},
x-pdf = {http://www.lri.fr/~mandel/papers/HalbwachsMandel-ACSD-2006.pdf},
url = {http://www.lri.fr/~mandel/papers/HalbwachsMandel-ACSD-2006.pdf},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {ACSD}
}
@inproceedings{SamperMaraninchiMounierMandel2006InterSense,
author = {Ludovic Samper and Florence Maraninchi and Laurent Mounier
and Louis Mandel},
title = {{GLONEMO}: Global and Accurate Formal Models for the Analysis of Ad hoc Sensor Networks},
booktitle = {Proceedings of the First International Conference on Integrated Internet Ad hoc and Sensor Networks ({InterSense'06})},
year = {2006},
address = {Nice, France},
month = may,
publisher = {ACM Press},
url = {http://www.lri.fr/~mandel/papers/SamperMaraninchiMounierMandel-InterSense-2006.pdf},
x-pdf = {http://www.lri.fr/~mandel/papers/SamperMaraninchiMounierMandel-InterSense-2006.pdf},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {Bodynets}
}
@inproceedings{MandelBenbadis2005SLAP,
author = {Louis Mandel and Farid Benbadis},
title = {Simulation of Mobile Ad hoc Network Protocols in {ReactiveML}},
booktitle = {Proceedings of Synchronous Languages, Applications, and Programming ({SLAP'05})},
publisher = {Elsevier Science Publishers},
year = 2005,
month = apr,
address = {Edinburgh, Scotland},
x-pdf = {http://www.lri.fr/~mandel/papers/MandelBenbadis-SLAP-2005.pdf},
url = {http://www.lri.fr/~mandel/papers/MandelBenbadis-SLAP-2005.pdf},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {ENTCS}
}
@inproceedings{MandelPouzet2005JFLA,
author = {Louis Mandel and Marc Pouzet},
title = {{ReactiveML}, un langage pour la programmation r{\'e}active en {ML}},
crossref = {jfla05},
pages = {1-16},
url = {http://www.lri.fr/~mandel/papers/MandelPouzet-JFLA-2005.ps},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@inproceedings{marche05tphols,
topics = {team},
author = {Claude March\'e and Christine Paulin-Mohring},
title = {Reasoning about {Java} Programs with Aliasing and Frame
Conditions},
crossref = {tphols2005},
pages = {179--194},
topics = {team,lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {TPHOLs},
url = {http://www.lri.fr/~marche/marche05tphols.ps}
}
@inproceedings{marche06sefm,
author = {Claude March\'e and Nicolas Rousset},
topics = {team},
title = {Verification of {Java Card} Applets Behavior with
respect to Transactions and Card Tears},
crossref = {sefm06},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {SEFM}
}
@inproceedings{marche06wst,
author = {Claude March{\'e} and Hans Zantema},
title = {The Termination Competition 2006},
crossref = {wst06},
year = 2006,
topics = {team},
type_publi = {icolcomlec},
url = {http://www.lri.fr/~marche/termination-competition/},
note = {\url{http://www.lri.fr/~marche/termination-competition/}},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {WST}
}
@inproceedings{moy07ccpp,
author = {Yannick Moy},
title = {Union and Cast in Deductive Verification},
booktitle = {Proceedings of the {C/C++} Verification Workshop},
year = 2007,
volume = {Technical Report ICIS-R07015},
month = jul,
pages = {1--16},
publisher = {Radboud University Nijmegen},
x-pdf = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
url = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
topics = {team, lri},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux}
}
@inproceedings{moy07hav,
author = {Yannick Moy and Claude March\'e},
title = {Inferring Local (Non-)Aliasing and Strings for Memory Safety},
booktitle = {Heap Analysis and Verification (HAV'07)},
year = 2007,
address = {Braga, Portugal},
month = mar,
pages = {35--51},
topics = {team lri},
type_digiteo = {conf_autre},
type_publi = {icolcomlec},
x-pdf = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
url = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {HAV}
}
@inproceedings{moy08vmcai,
author = {Yannick Moy},
title = {Sufficient Preconditions for Modular Assertion Checking},
crossref = {vmcai08},
pages = {188--202},
x-pdf = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
url = {http://www.lri.fr/~moy/publis/moy08vmcai.pdf},
topics = {team, lri},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {VMCAI},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{oury05tphols,
author = {Nicolas Oury},
title = {Extensionality in the {Calculus of Constructions}},
topics = {team,lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
pages = {278--293},
x-cle-support = {TPHOLs},
crossref = {tphols2005}
}
@inproceedings{signoles05jfla,
author = {Julien Signoles},
title = {Une approche fonctionnelle du mod\`ele vue-contr\^oleur},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla05},
pages = {63--78}
}
@inproceedings{sozeau06types,
author = {Matthieu Sozeau},
title = {Subset coercions in {C}oq},
year = 2007,
crossref = {types06},
pages = {237--252},
url = {http://www.lri.fr/~sozeau/research/publications/Subset_Coercions_in_Coq.pdf},
x-slides = {http://www.lri.fr/~sozeau/research/publications/Subset_Coercions_in_Coq-types06-210406.pdf},
abstract = {We propose a new language for writing programs with dependent
types on top of the {C}oq proof assistant. This language permits
to establish a phase distinction between writing and proving
algorithms in the {C}oq environment. Concretely, this means allowing
to write algorithms as easily as in a practical functional programming
language whilst giving them as rich a specification as desired and
proving that the code meets the specification using the whole {C}oq
proof apparatus. This is achieved by extending conversion to an
equivalence which relates types and subsets based on them, a technique
originating from the ``Predicate subtyping'' feature of PVS
and following mathematical convention. The typing judgements can be
translated to the Calculus of Inductive Constructions by means of an interpretation
which inserts coercions at the appropriate places. These coercions can
contain existential variables representing the propositional parts of
the final term, corresponding to proof obligations (or PVS
type-checking conditions). A prototype implementation of this process
is integrated with the {C}oq environment.},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {TYPES}
}
@inproceedings{sozeau07icfp,
author = {Matthieu Sozeau},
title = {{P}rogram-ing Finger Trees in {C}oq},
pages = {13--24},
doi = {10.1145/1291151.1291156},
url = {http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq.pdf},
x-slides = {http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq-icfp07-011007.pdf},
copyright = {ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'07},
abstract = {Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent
data structure with good performance. Their genericity permits developing
a wealth of structures like ordered sequences or interval trees
on top of a single implementation. However, the type systems
used by current functional languages do not guarantee the coherent
parameterization and specialization of Finger Trees, let alone the
correctness of their implementation.
We present a certified implementation of Finger Trees solving
these problems using the {P}rogram extension of {C}oq.
We not only implement the structure but also prove its
invariants along the way, which permit building certified
structures on top of Finger Trees in an elegant way.},
crossref = {icfp07},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ICFP}
}
@inproceedings{sozeau08tphols,
author = {Matthieu Sozeau and Nicolas Oury},
crossref = {tphols2008},
url = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes.pdf},
x-slides = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf},
title = {{F}irst-{C}lass {T}ype {C}lasses},
abstract = {
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for
specifying with abstract structures by quantification on contexts. However,
both systems are limited by second-class implementations of these constructs,
and these limitations are only overcomed by ad-hoc extensions to
the respective systems. We propose an embedding of type classes into a
dependent type theory that is first-class and supports some of the most
popular extensions right away. The implementation is correspondingly
cheap, general and very well integrated inside the system, as we have
experimented in Coq. We show how it can be used to help structured
programming and proving by way of examples.},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {TPHOLs},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{bol08rnc,
title = {Formal proof for delayed finite field arithmetic using floating point operators},
author = {Sylvie Boldo and Marc Daumas and Pascal Giorgi},
booktitle = {Proceedings of the 8th Conference on Real Numbers and
Computers},
year = {2008},
address = {Santiago de Compostela, Spain},
month = jul,
pages = {113--122},
editor = {Daumas, Marc and Bruguera, Javier},
x-pdf = {http://hal.archives-ouvertes.fr/docs/00/27/89/89/PDF/rnc.pdf},
hal = {http://hal.inria.fr/inria-00278989/en/},
topics = {team,lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{bardou08ftfjp,
author = {Romain Bardou},
title = {Ownership, Pointer Arithmetic and Memory Separation},
crossref = {ftfjp08},
topics = {team},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {FTJP},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
url = {http://romain.bardou.fr/papers/jcown.pdf}
}
@inproceedings{bol05arith,
author = {Sylvie Boldo and Jean-Michel Muller},
title = {Some Functions Computable with a Fused-mac},
year = 2005,
address = {Cape Cod, USA},
booktitle = {Proceedings of the 17th Symposium on Computer Arithmetic},
url = {http://perso.ens-lyon.fr/jean-michel.muller/FmacArith.pdf},
editor = {Montuschi, Paolo and Schwarz, Eric},
pages = {52-58},
topics = {team,lri},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
type_publi = {icolcomlec}
}
@inproceedings{cohen05emsoft,
crossref = {pouzet05emsoft}
}
@inproceedings{pouzet05emsoft,
author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
and Claire Pagetti and Florence Plateau and Marc Pouzet},
title = {Synchronizing Periodic Clocks},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'05)},
address = {Jersey city, New Jersey, USA},
month = sep,
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {EMSOFT},
year = 2005
}
@inproceedings{colaco05emsoft,
author = {Jean-Louis Cola\c{c}o and Bruno Pagano and Marc Pouzet},
title = {{A Conservative Extension of Synchronous Data-flow with
State Machines}},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'05)},
address = {Jersey city, New Jersey, USA},
month = sep,
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {EMSOFT},
year = 2005
}
@inproceedings{cohen06popl,
crossref = {pouzet06popl}
}
@inproceedings{pouzet06popl,
author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
and Claire Pagetti and Florence Plateau and Marc Pouzet},
title = {{N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems}},
booktitle = {ACM International Conference on
Principles of Programming Languages (POPL'06)},
address = {Charleston, South Carolina, USA},
month = {January},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {POPL},
year = 2006
}
@inproceedings{colaco06emsoft,
author = {Jean-Louis Cola\c{c}o and Gr\'egoire Hamon and Marc Pouzet},
title = {{Mixing Signals and Modes in Synchronous
Data-flow Systems}},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'06)},
address = {Seoul, South Korea},
month = {October},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {EMSOFT},
topics = {team},
year = 2006
}
@inproceedings{lucy:cdc10,
author = {Albert Benveniste and Benoit Caillaud and Marc Pouzet},
title = {{The Fundamentals of Hybrid Systems Modelers}},
booktitle = {49th IEEE International Conference on Decision and
Control (CDC)},
year = {2010},
address = {Atlanta, Georgia, USA},
month = {December 15-17},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {CDC},
x-type = {article}
}
@inproceedings{lescuyer08tpholset,
author = {St\'ephane Lescuyer and Sylvain Conchon},
title = {A Reflexive Formalization of a {SAT} Solver in {Coq}},
booktitle = {Emerging Trends of the 21st International Conference on Theorem Proving in Higher Order Logics},
year = 2008,
topics = {team},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {?},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{boldo06scan,
author = {Sylvie Boldo and Marc Daumas and William Kahan and
Guillaume Melquiond},
title = {Proof and certification for an accurate discriminant},
booktitle = {12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
year = {2006},
address = {Duisburg,Germany},
topics = {team},
type_publi = {colloque},
url = {http://scan2006.uni-due.de/show_abstracts.php?title=+Proof+and+certification+for+an+accurate+discriminant},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SCAN},
month = {sep}
}
@inproceedings{mlpost09jfla,
author = {Romain Bardou and Jean-Christophe Filli\^atre and Johannes Kanig and St\'ephane Lescuyer},
title = {{Faire bonne figure avec Mlpost}},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/mlpost-fra.pdf},
abstract = {Cet article pr\'esente Mlpost, une biblioth\`eque Ocaml de dessin
scientifique. Elle s'appuie sur Metapost, qui permet notamment
d'inclure des fragments \LaTeX\ dans les figures. Ocaml offre une
alternative s\'eduisante aux langages de macros \LaTeX, aux langages
sp\'ecialis\'es ou m\^eme aux outils graphiques. En particulier,
l'utilisateur de Mlpost b\'en\'eficie de toute l'expressivit\'e
d'Ocaml et de son typage statique. Enfin Mlpost propose un style
d\'eclaratif qui diff\`ere de celui, souvent imp\'eratif, des outils existants.},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla09}
}
@inproceedings{mandel-plateau09jfla,
author = {Louis Mandel and Florence Plateau},
title = {{Abstraction d'horloges dans les syst\`emes synchrones flot de donn\'ees}},
url = {http://www.lri.fr/~plateau/papers/jfla09.pdf},
abstract = {Les langages synchrones flot de donn\'ees tels que
Lustre manipulent des s\'equences infinies de
donn\'ees comme valeurs de base. Chaque flot est
associ\'e \`a une horloge qui d\'efinit les instants
o\`u sa valeur est pr\'esente. Cette horloge est une
information de type et un syst\`eme de types
d\'edi\'e, le calcul d'horloges, rejette
statiquement les programmes qui ne peuvent pas \^etre
ex\'ecut\'es de mani\`ere synchrone. Dans les
langages synchrones existants, cela revient \`a se
demander si deux flots ont la m\^eme horloge et repose
donc uniquement sur l'\'egalit\'e d'horloges. Des
travaux r\'ecents ont montr\'e l'int\'er\^et
d'introduire une notion rel\^ach\'ee du synchronisme,
o\`u deux flots peuvent \^etre compos\'es d\`es qu'ils
peuvent \^etre synchronis\'es par l'introduction d'un
buffer de taille born\'ee (comme c'est fait dans le
mod\`ele SDF d'Edward Lee). Techniquement, cela
consiste \`a remplacer le typage par du
sous-typage. Ce papier est une traduction et
am\'elioration technique de~\cite{Pouzet08c} qui pr\'esente
un moyen simple de mettre en oeuvre ce mod\`ele
rel\^ach\'e par l'utilisation d'horloges abstraites.
Les valeurs abstraites repr\'esentent des ensembles
d'horloges concr\`etes qui ne sont pas
n\'ecessairement p\'eriodiques. Cela permet de
mod\'eliser divers aspects des logiciels
temps-r\'eel embarqu\'es, tels que la gigue born\'ee
pr\'esente dans les syst\`emes vid\'eo, le temps
d'ex\'ecution des processus temps r\'eel et, plus
g\'en\'eralement, la communication \`a travers des
buffers de taille born\'ee. Nous pr\'esentons ici
l'alg\`ebre des horloges abstraites et leurs
principales propri\'et\'es th\'eoriques.},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla09}
}
@inproceedings{regis-gianas-pottier-08,
author = {Yann R\'egis-Gianas and Fran\c{c}ois Pottier},
title = {A {Hoare} Logic for Call-by-Value Functional
Programs},
year = {2008},
url = {http://cristal.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf},
doi = {10.1007/978-3-540-70594-9_17},
pages = {305--335},
topics = {team},
abstract = {We present a Hoare logic for a call-by-value
programming language equipped with recursive,
higher-order functions, algebraic data types, and a
polymorphic type system in the style of Hindley and
Milner. It is the theoretical basis for a tool that
extracts proof obligations out of programs annotated
with logical assertions. These proof obligations,
expressed in a typed, higher-order logic, are
discharged using off-the-shelf automated or interactive
theorem provers. Although the technical apparatus that
we exploit is by now standard, its application to
functional programming languages appears to be new, and
(we claim) deserves attention. As a sample application,
we check the partial correctness of a balanced binary
search tree implementation.},
booktitle = {Proceedings of the Ninth International Conference on
Mathematics of Program Construction (MPC'08)},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {MPC},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{boldo09calculemus,
author = {Sylvie Boldo and Jean-Christophe Filli\^atre and Guillaume Melquiond},
title = {Combining {C}oq and {G}appa for {C}ertifying {F}loating-{P}oint
{P}rograms },
booktitle = {16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning},
pages = {59--74},
year = {2009},
month = jul,
volume = {5625},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
address = {Grand Bend, Canada},
doi = {10.1007/978-3-642-02614-0_10},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-support = {actes},
topics = {team}
}
@inproceedings{boldo09icalp,
author = {Sylvie Boldo},
title = {Floats and Ropes: A Case Study for Formal Numerical Program Verification},
booktitle = {36th International Colloquium on Automata, Languages and Programming},
pages = {91--102},
year = {2009},
volume = {5556},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-support = {actes},
topics = {team},
doi = {10.1007/978-3-642-02930-1_8},
x-url = {http://fost.saclay.inria.fr/files/icalp2009trackb_submission_48.pdf}
}
@inproceedings{ayad10ijcar,
author = {Ali Ayad and Claude March\'e},
title = {Multi-Prover Verification of Floating-Point Programs},
crossref = {ijcar10},
pages = {127--141},
hal = {http://hal.inria.fr/inria-00534333},
x-equipes = {demons PROVAL EXT},
topics = {team},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {IJCAR},
x-type = {article},
x-editorial-board = {yes}
}
@inproceedings{HurlinBS09,
author = {Cl\'ement Hurlin and Fran\c{c}ois Bobot and Alexander J. Summers},
title = {Size Does Matter : Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic},
booktitle = {International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09)},
url = {http://www.lri.fr/~bobot/publis/Hurlin_Bobot_Summers_iwaco09.pdf},
note = {Coq proofs: \url{http://www-sop.inria.fr/everest/Clement.Hurlin/disprove.tgz}},
month = jul,
year = {2009},
topics = {team},
abstract = {We describe an algorithm to disprove entailment between
separation logic formulas. We abstract models
of formulas by their size and check whether two formulas
have models whose sizes are compatible.
Given two formulas $A$ and $B$ that do not have compatible models,
we can conclude that $A$ does not entail $B$. We provide
two different abstractions (of different precision) of models.
Our algorithm is of interest wherever entailment checking
is performed (such as in program verifiers).},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {GB,NL},
hal = {http://hal.inria.fr/hal-00777577}
}
@inproceedings{KanigFilliatre09wml,
author = {Johannes Kanig and Jean-Christophe Filli\^atre},
title = {{Who: A Verifier for Effectful Higher-order Programs}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Edinburgh, Scotland, UK},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
month = aug,
year = 2009,
url = {https://usr.lmf.cnrs.fr/~jcf/publis/wml09.pdf},
hal = {http://hal.inria.fr/hal-00777585},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {ML},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
abstract = {We present Who, a tool for verifying effectful higher-order
functions. It features {\em Effect polymorphism}, higher-order logic
and the possibility to reason about state in the logic, which enable
highly modular specifications of generic code. Several small
examples and a larger case study demonstrate its usefulness. The
Who~tool is intended to be used as an intermediate language for
verification tools targeting ML-like programming languages.}
}
@inproceedings{MandelPlateauPouzet-MLworkshop-2009,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {The {ReactiveML} Toplevel (Tool Demonstration)},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Edinburgh, Scotland, UK},
topics = {team, lri},
type_publi = {icolcomlec},
month = aug,
year = 2009,
x-type = {article},
x-support = {actes_aux},
x-equipes = {demons PROVAL},
x-cle-support = {ML},
x-international-audience = {yes},
x-proceedings = {no},
x-editorial-board = {yes}
}
@inproceedings{tafat10foveoos,
title = {A Refinement Methodology for Object-Oriented Programs},
author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
crossref = {foveoos10},
x-equipes = {demons PROVAL EXT},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes_aux},
x-type = {article},
x-cle-support = {FOVEOOS},
pages = {143--159},
hal = {http://hal.inria.fr/inria-00534336},
topics = {team}
}
@inproceedings{tafat11foveoos,
title = {A Refinement Methodology for Object-Oriented Programs},
author = {Asma Tafat and Sylvain Boulm\'e and Claude March\'e},
x-equipes = {demons PROVAL EXT},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-type = {article},
x-cle-support = {FOVEOOS},
topics = {team},
pages = {153--167},
hal = {http://hal.inria.fr/inria-00534336},
crossref = {postfoveoos10}
}
@inproceedings{LescuyerConchon09frocos,
author = {St{\'e}phane Lescuyer and Sylvain Conchon},
title = {Improving {Coq} Propositional Reasoning using a Lazy {CNF} Conversion Scheme},
topics = {team},
x-support = {actes},
pages = {287-303},
doi = {10.1007/978-3-642-04222-5_18},
crossref = {frocos09}
}
@inproceedings{conchon10jfla,
author = {Conchon, Sylvain and Filli\^atre, Jean-Christophe
and Le Fessant, Fabrice and Robert, Julien and Von Tokarski, Guillaume},
title = {{Observation temps-r\'eel de programmes Caml}},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla10},
url = {http://www.lri.fr/~conchon/publis/ocamlviz-jfla2010.pdf}
}
@inproceedings{MandelPlateau10jfla,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n}~: une extension n-synchrone de {Lustre}},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateau-JFLA-2010.pdf},
abstract = {Les langages synchrones flot de donn\'ees permettent de programmer
des r\'eseaux de processus communicant sans buffers.
Pour cela, chaque
flot est associ\'e \`a un type d'horloges, qui indique les instants de
pr\'esence de valeurs sur le flot. La communication entre deux
processus \verb+f+ et \verb+g+ peut \^etre faite sans buffer si le
type du flot de sortie de \verb+f+ est \'egal au type du flot d'entr\'ee
de~\verb+g+.
Un syst\`eme de type, le calcul d'horloge, inf\`ere des types tels que
cette condition est v\'erifi\'ee.
Le mod\`ele n-synchrone a pour but de rel\^acher ce mod\`ele de
programmation en autorisant les communications \`a travers des buffers
de taille born\'ee. En pratique, cela consiste \`a introduire une
r\`egle de sous-typage dans le calcul d'horloge.
Nous avons pr\'esent\'e l'ann\'ee derni\`ere un article d\'ecrivant comment
abstraire des horloges pour v\'erifier la relation de
sous-typage. Cette ann\'ee, nous pr\'esentons un langage de
programmation n-synchrone~: Lucy-n. Dans ce langage, l'inf\'erence
des types d'horloges est param\'etrable par l'algorithme de r\'esolution
des contraintes de sous-typage. Nous montrons ici un algorithme
bas\'e sur les travaux de
l'an dernier et comment programmer en Lucy-n \`a travers l'exemple
d'une application de traitement multim\'edia.},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla10}
}
@inproceedings{MandelPlateau10gpl,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n~:} une extension n-synchrone de {Lustre}},
booktitle = {{Journ\'ees nationales du GDR-GPL}},
year = {2010},
editor = {\'Eric Cariou and Laurence Duchien and Yves Ledru},
address = {{Pau, France}},
month = mar,
organization = {{GDR GPL}},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {JGDRGPL},
x-type = {article},
annote = {Invited, selected paper}
}
@inproceedings{mandel10jfla,
author = {Louis Mandel},
title = {Cours de {ReactiveML}},
url = {http://www.lri.fr/~mandel/papiers/Mandel-JFLA-2010.pdf},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-type = {article},
x-cle-support = {JFLA},
crossref = {jfla10}
}
@inproceedings{MandelPlateauPouzet-MPC-2010,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n}: a n-Synchronous Extension of {Lustre}},
booktitle = {Tenth International Conference on Mathematics of Program Construction ({MPC 2010})},
year = 2010,
month = jun,
address = {Qu{\'e}bec, Canada},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateauPouzet-MPC-10.pdf},
abstract = {Synchronous functional languages such as Lustre
or Lucid Synchrone define a
restricted class of Kahn Process Networks which can be executed with
no buffer.
Every expression is associated to a clock indicating the instants
when a value is present. A dedicated type system, the clock
calculus, checks that the actual clock of a stream equals its
expected clock and thus does not need to be buffered.
The n-synchrony relaxes synchrony by allowing the
communication through bounded buffers whose size is computed at
compile-time.
It is obtained by extending the clock calculus with
a subtyping rule which defines buffering points.
This paper presents the first implementation of the n-synchronous
model inside a Lustre-like language called Lucy-n. The language
extends Lustre with an explicit \verb-buffer- construct whose size
is automatically computed during the clock calculus.
This clock calculus is defined as an inference type system and is
parametrized by the clock language and the algorithm used to solve
subtyping constraints. We detail here one algorithm based on the
abstraction of clocks, an idea originally introduced
in~\cite{Pouzet08c}. The paper presents a simpler, yet more
precise, clock abstraction for which the main algebraic properties have
been proved in Coq. Finally, we illustrate the language on various
examples including a video application.},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {MPC},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{MandelPlateau-MPC-2012,
author = {Louis Mandel and Florence Plateau},
title = {Scheduling and Buffer Sizing of n-Synchronous Systems:
Typing of Ultimately Periodic Clocks in {Lucy-n}},
booktitle = {Eleventh International Conference on Mathematics of Program Construction ({MPC'12})},
year = 2012,
month = jun,
address = {Madrid, Spain},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateau-MPC-2012.pdf},
abstract = {Lucy-n is a language for programming networks of processes
communicating through bounded buffers. A dedicated type
system, termed a clock calculus, automatically computes static
schedules of the processes and the sizes of the buffers between
them.
In this article, we present a new algorithm which solves the
subtyping constraints generated by the clock calculus. The
advantage of this algorithm is that it finds schedules for tightly
coupled systems. Moreover, it does not overestimate the buffer
sizes needed and it provides a way
to favor either system throughput or buffer size minimization.},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {MPC},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{cimatti10date,
author = {Alessandro Cimatti and Anders Franzen and Alberto Griggio and
Krishnamani Kalyanasundaram and Marco Roveri},
title = {Tighter Integration of {BDDs} and {SMT} for Predicate
Abstraction},
hal = {http://hal.inria.fr/inria-00535785},
x-equipes = {demons PROVAL EXT},
x-support = {actes},
x-type = {article},
x-cle-support = {DATE},
topics = {team},
crossref = {date10}
}
@inproceedings{edmonson09arith,
author = {William Edmonson and Guillaume Melquiond},
title = {{IEEE} interval standard working group - {P1788}: current status},
booktitle = {Proceedings of the 19th IEEE Symposium on Computer Arithmetic},
editor = {Javier D. Bruguera and Marius Cornea and Debjit DasSarma and John Harrison},
address = {Portland, OR, USA},
year = {2009},
pages = {231--234},
doi = {10.1109/ARITH.2009.36},
topics = {team},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {US},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
type_publi = {icolcomlec}
}
@inproceedings{Pouzet-lctes09,
author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
and Marc Pouzet and Pascal Raymond},
title = {{Synchronous Objects with Scheduling Policies}:
Introducing safe shared memory in {Lustre}},
year = {2009},
month = jun,
address = {Dublin},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
url-useless-since-prefix-missing = {lctes09.pdf},
x-proceedings = {yes},
x-international-audience = {yes},
x-type = {article},
x-support = {actes},
topics = {team}
}
@inproceedings{Pouzet-emsoft09,
author = {Marc Pouzet and Pascal Raymond},
title = {Modular Static Scheduling of Synchronous Data-flow
Networks: An efficient symbolic representation},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'09)},
address = {Grenoble, France},
month = {October},
x-proceedings = {yes},
x-international-audience = {yes},
year = 2009,
url-useless-since-prefix-missing = {emsoft09.pdf},
x-type = {article},
x-support = {actes},
topics = {team}
}
@inproceedings{tushkanova10ldta,
author = {Tushkanova, Elena and Giorgetti, Alain and
March{\'e}, Claude and Kouchnarenko, Olga},
title = {Specifying Generic {Java} Programs: two case studies},
booktitle = {Tenth Workshop on Language Descriptions, Tools and Applications},
editor = {Claus Brabrand and Pierre-Etienne Moreau},
publisher = {ACM Press},
year = 2010,
x-equipes = {demons PROVAL EXT},
topics = {team},
hal = {http://hal.inria.fr/inria-00525784/en/},
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {LDTA},
x-type = {article},
x-editorial-board = {yes}
}
@inproceedings{boldo10-nfm,
author = {Sylvie Boldo and Nguyen, Thi Minh Tuyen},
title = {Hardware-independent proofs of numerical programs},
booktitle = {Proceedings of the Second NASA Formal Methods Symposium},
year = 2010,
series = {NASA Conference Publication},
address = {Washington D.C., USA},
month = apr,
x-equipes = {demons PROVAL},
x-support = {actes},
x-cle-support = {NASAFM},
x-type = {article},
topics = {team},
pages = {14--23},
editor = {C\'esar Mu{\~n}oz},
hal = {http://hal.inria.fr/inria-00534410/en/},
x-pdf = {http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{boldo10-itp,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
booktitle = {Interactive Theorem Proving},
year = 2010,
series = {Lecture Notes in Computer Science},
x-address = {Edinburgh, Scotland},
x-month = jul,
publisher = {Springer},
x-editor = {Matt Kaufmann and Lawrence C. Paulson},
volume = 6172,
pages = {147--162},
hal = {http://hal.inria.fr/inria-00450789/en},
doi = {10.1007/978-3-642-14052-5_12/},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-cle-support = {ITProving},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@inproceedings{boldo10-nsv,
author = {Sylvie Boldo},
title = {{Formal verification of numerical programs: from C annotated programs to Coq proofs}},
booktitle = {Proceedings of the Third International Workshop on Numerical Software Verification},
address = {Edinburgh, Scotland},
year = {2010},
month = jul,
x-international-audience = {yes},
x-invited-conference = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
note = {NSV-8},
annote = {Invited paper},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {NSV},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/inria-00534400/en/}
}
@inproceedings{herms10coq,
author = {Paolo Herms},
title = {Certification of a chain for deductive program verification},
booktitle = {2nd Coq Workshop, satellite of ITP'10},
year = 2010,
x-international-audience = {yes},
x-proceedings = {no},
hal = {http://hal.inria.fr/inria-00535640},
editor = {Yves Bertot},
x-equipes = {demons PROVAL},
x-support = {actes_aux},
x-cle-support = {COQ},
x-type = {article},
topics = {team}
}
@inproceedings{bardou11jfla,
author = {Bardou, Romain and March\'e, Claude},
title = {Perle de preuve: les tableaux creux},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla11}
}
@inproceedings{filliatre11jfla,
author = {Filli\^atre, Jean-Christophe and Kalyanasundaram, Krishnamani},
title = {Une biblioth\`eque de calcul distribu\'e pour {Objective Caml}},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla11},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/jfla-2011.pdf}
}
@inproceedings{MandelPlateau11jfla,
author = {Louis Mandel and Florence Plateau},
title = {Typage des horloges p{\'e}riodiques en {Lucy-n}},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateau-JFLA-2011.pdf},
abstract = {Lucy-n est un langage permettant de programmer des r{\'e}seaux de
processus communiquant {\`a} travers des buffers de taille
born{\'e}e. La taille des buffers et les rythmes d'ex{\'e}cution relatifs
des processus sont calcul{\'e}s par une phase de typage appel{\'e}e calcul
d'horloge. Ce typage n{\'e}cessite la r{\'e}solution d'un ensemble de
contraintes de sous-typage. L'an dernier, nous avons propos{\'e} un
algorithme de r{\'e}solution de ces contraintes utilisant des m{\'e}thodes
issues de l'interpr{\'e}tation abstraite. Cette ann{\'e}e nous pr{\'e}sentons
un algorithme tirant profit de toute l'information contenue dans les
types.},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA},
crossref = {jfla11}
}
@inproceedings{filliatre10-opencert,
author = {Manuel Barbosa and Jean-Christophe Filli\^atre and Jorge Sousa Pinto and B\'arbara Vieira},
title = {A Deductive Verification Platform for Cryptographic Software},
booktitle = {4th International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010)},
year = 2010,
address = {Pisa, Italy},
month = {September},
volume = {33},
publisher = {Electronic Communications of the EASST},
url = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/461},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {OSSC},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-pays = {PT}
}
@inproceedings{contejean10gpl,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
and Andrei Paskevich and Olivier Pons and Xavier
Urbain},
title = {{A3PAT, an Approach for Certified Automated Termination Proofs}},
booktitle = {{Journ\'ees nationales du GDR-GPL}},
year = {2010},
editor = {\'Eric Cariou and Laurence Duchien and Yves Ledru},
address = {{Pau, France}},
month = mar,
organization = {{GDR GPL}},
topics = {team},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {JGDRGPL},
x-type = {article},
annote = {Invited, selected paper}
}
@inproceedings{lucy:lctes11,
author = {Albert Benveniste and Timothy Bourke and
Benoit Caillaud and Marc Pouzet},
title = {{Divide and recycle: types and compilation for a
hybrid synchronous language}},
booktitle = {ACM SIGPLAN/SIGBED Conference on Languages,
Compilers, Tools and Theory for Embedded Systems (LCTES'11)},
month = {April},
address = {Chicago, USA},
year = 2011,
url = {lctes11.pdf},
abstract = {Hybrid modelers such as Simulink have become corner stones of embedded
systems development.
They allow both \emph{discrete} controllers and their \emph{continuous}
environments to be expressed \emph{in a single language}.
Despite the availability of such tools, there remain a number of issues
related to the lack of reproducibility of simulations and to the
separation of the continuous part, which has to be exercised by a
numerical solver, from the discrete part, which must be guaranteed not to
evolve during a step.
Starting from a minimal, yet full-featured, Lustre-like synchronous
language, this paper presents a conservative extension
where data-flow equations can be mixed with ordinary differential
equations (ODEs) with possible reset.
A type system is proposed to statically distinguish discrete computations
from continuous ones and to ensure that signals are used in their proper
domains.
We propose a semantics based on \emph{non-standard analysis} which gives a
synchronous interpretation to the whole language, clarifies the
discrete/continuous interaction and the treatment of zero-crossings, and
also allows the correctness of the type system to be established.
The extended data-flow language is realized through a source-to-source
transformation into a synchronous subset, which can then be compiled using
existing tools into routines that are both efficient and bounded in their
use of memory.
These routines are orchestrated with a single off-the-shelf numerical
solver using a simple but precise algorithm which treats causally-related
cascades of zero-crossings.
We have validated the viability of the approach through experiments with
the SUNDIALS library.},
x-type = {article},
x-support = {actes},
x-proceedings = {yes},
x-international-audience = {yes},
topics = {team}
}
@inproceedings{dross11tap,
author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy},
title = {{Correct Code Containing Containers}},
booktitle = {5th International Conference on Tests and Proofs (TAP'11)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6706},
pages = {102--118},
year = 2011,
address = {Zurich},
month = jun,
url = {http://proval.lri.fr/publications/dross11tap.pdf},
hal = {http://hal.inria.fr/hal-00777683},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {TAP},
abstract = {
For critical software development, containers such as lists, vectors, sets or
maps are an attractive alternative to ad-hoc data structures based on
pointers.
As standards like DO-178C put formal verification and testing on an equal
footing, it is important to give users the ability to apply both to the
verification of code using containers.
In this paper,
we present a definition of containers whose aim is to facilitate their
use in certified software, using modern proof technology and novel
specification languages. Correct usage of containers and user-provided
correctness properties can be checked either by execution during testing
or by formal proof with an automatic prover.
We present a formal semantics for containers and an axiomatization of this
semantics targeted at automatic provers. We have proved in Coq that the
formal semantics is consistent and that the axiomatization thereof is
correct.}
}
@inproceedings{filliatre11tfp,
author = {Jean-Christophe Filli\^atre and Krishnamani Kalyanasundaram},
title = {Functory: A Distributed Computing Library for {Objective Caml}},
booktitle = {Trends in Functional Programming},
year = 2011,
series = {Lecture Notes in Computer Science},
volume = {7193},
pages = {65--81},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {TFP},
x-equipes = {demons PROVAL},
address = {Madrid, Spain},
month = {May},
abstract = {We present Functory, a distributed computing library for
Objective Caml. The main features of this library
include (1) a polymorphic API, (2) several implementations to
adapt to different deployment scenarios such as sequential,
multi-core or network, and (3) a reliable fault-tolerance mechanism.
This paper describes the motivation behind this work, as well as
the design and implementation of the library. It also demonstrates
the potential of the library using realistic experiments.},
url = {https://usr.lmf.cnrs.fr/~jcf/publis/tfp11.pdf}
}
@inproceedings{boogie11why3,
topics = {team},
hal = {http://hal.inria.fr/hal-00790310},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
title = {Why3: Shepherd Your Herd of Provers},
booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
year = 2011,
address = {Wroc\l{}aw, Poland},
month = {August},
pages = {53--64},
note = {\url{https://hal.inria.fr/hal-00790310}},
x-international-audience = {yes},
x-proceedings = {yes},
x-cle-support = {BOOGIE},
x-type = {actes_aux},
x-support = {article},
x-equipes = {demons PROVAL},
keywords = {Why3},
abstract = {Why3 is the next generation of the
Why software verification platform.
Why3 clearly separates the purely logical
specification part from generation of verification conditions for programs.
This article focuses on the former part.
Why3 comes with a new enhanced language of
logical specification. It features a rich library of
proof task transformations that can be chained to produce a suitable
input for a large set of theorem provers, including SMT solvers,
TPTP provers, as well as interactive proof assistants.}
}
@inproceedings{mandel11fmcad,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {Static Scheduling of Latency Insensitive Designs with {Lucy-n}},
booktitle = {Formal Methods in Computer Aided Design ({FMCAD 2011})},
year = 2011,
month = oct,
address = {Austin, TX, USA},
hal = {http://hal.inria.fr/hal-00654843},
url = {http://www.lri.fr/~mandel/papiers/MandelPlateauPouzet-FMCAD-2011.pdf},
webpage = {http://www.lri.fr/~mandel/lucy-n/fmcad11/},
abstract = {Lucy-n is a dataflow programming language similar to Lustre
extended with a buffer operator. This language is based on the
n-synchronous model which was initially introduced for programming
multimedia streaming applications. In this article, we show that
Lucy-n is also applicable to model Latency Insensitive
Designs~(LID). In order to model relay stations, we have to
introduce a delay operator. Thanks to this new operator, a LID can be
described by a Lucy-n program. Then, the Lucy-n compiler
automatically provides static schedules for computation nodes and
buffer sizes needed in the shell wrappers.},
topics = {team},
x-teams = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {FMCAD},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{BolMel11,
author = {Sylvie Boldo and Guillaume Melquiond},
title = {{Flocq}: A Unified Library for Proving Floating-point Algorithms in {Coq}},
booktitle = {Proceedings of the 20th IEEE Symposium on Computer Arithmetic},
editor = {Elisardo Antelo and David Hough and Paolo Ienne},
address = {T{\"u}bingen, Germany},
year = {2011},
pages = {243--252},
doi = {10.1109/ARITH.2011.40},
hal = {http://hal.archives-ouvertes.fr/inria-00534854/},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{nguyen11cpp,
author = {Thi Minh Tuyen Nguyen and Claude March\'e},
title = {Hardware-Dependent Proofs of Numerical Programs},
crossref = {cpp2011},
pages = {314--329},
topics = {team},
x-equipes = {demons PROVAL},
x-support = {actes},
x-cle-support = {CPP},
x-type = {article},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
hal = {http://hal.inria.fr/hal-00772508}
}
@inproceedings{BobotPaskevich2011frocos,
author = {Fran\c{c}ois Bobot and Andrei Paskevich},
title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
pages = {87--102},
topics = {team},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL},
x-cle-support = {FROCOS},
url = {http://proval.lri.fr/publications/bobot11frocos.pdf},
crossref = {frocos11}
}
@inproceedings{herms12vstte,
title = {A Certified Multi-prover Verification Condition Generator},
author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
crossref = {vstte12},
hal = {http://hal.inria.fr/hal-00639977},
pages = {2--17},
x-equipes = {demons PROVAL ext},
url = {http://proval.lri.fr/publications/herms12vstte.pdf},
topics = {team}
}
@inproceedings{filliatre12vstte,
author = {Jean-Christophe Filli\^atre},
title = {Verifying Two Lines of {C} with {Why3}: an Exercise in Program Verification},
crossref = {vstte12},
pages = {83--97},
x-equipes = {demons PROVAL},
topics = {team},
keywords = {Why3},
url = {http://proval.lri.fr/publications/filliatre12vstte.pdf},
abstract = {This article details the formal verification of a 2-line C program
that computes the number of solutions to the $n$-queens problem.
The formal proof of (an abstraction of) the C code
is performed using the Why3 tool to generate
the verification conditions and several provers (Alt-Ergo, CVC3,
Coq) to discharge them. The main purpose of this article is to
illustrate the use of Why3 in verifying an algorithmically complex
program.}
}
@inproceedings{lelay12jfla,
author = {Catherine Lelay and Guillaume Melquiond},
title = {Diff\'erentiabilit\'e et int\'egrabilit\'e en {C}oq. {A}pplication \`a la formule de d'{A}lembert},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
crossref = {jfla12},
hal = {http://hal.inria.fr/hal-00642206/fr/}
}
@inproceedings{baelde11sofsem,
author = {David Baelde and
Romain Beauxis and
Samuel Mimram},
title = {Liquidsoap: A High-Level Programming Language for Multimedia
Streaming},
crossref = {sofsem11},
topics = {team, lri},
type_publi = {colcomlec},
x-type = {article},
x-support = {actes},
x-cle-support = {SOFSEM},
x-equipes = {demons PROVAL ext},
year = 2011
}
@inproceedings{baelde12itp,
title = {{Towards Provably Robust Watermarking}},
author = {David Baelde and Pierre Courtieu and David Gross-Amblard and Christine Paulin-Mohring},
abstract = {{Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.}},
keywords = {watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving},
year = 2012,
topics = {team},
x-equipes = {demons PROVAL ext},
month = aug,
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {article},
x-cle-support = {ITProving},
x-type = {article},
series = {Lecture Notes in Computer Science},
volume = {7406},
pdf = {http://hal.inria.fr/hal-00682398/PDF/techreport.pdf},
hal = {http://hal.inria.fr/hal-00682398},
booktitle = {ITP 2012}
}
@inproceedings{mentre12abz,
author = {David Mentr\'e and Claude March\'e and Jean-Christophe Filli\^atre and Masashi Asuka},
title = {Discharging Proof Obligations from {Atelier~B} using
Multiple Automated Provers},
booktitle = {ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z},
series = {Lecture Notes in Computer Science},
editor = {Steve Reeves and Elvinia Riccobene},
publisher = {Springer},
volume = {7316},
pages = {238--251},
year = 2012,
address = {Pisa, Italy},
month = jun,
abstract = {We present a method to discharge proof obligations from Atelier~B
using multiple SMT solvers. It is based on a faithful modeling of
B's set theory into polymorphic first-order logic. We report on two
case studies demonstrating a significant improvement in the ratio of
obligations that are automatically discharged.},
obsoletepdf = {https://usr.lmf.cnrs.fr/~jcf/publis/abz12.pdf},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {ABZ},
x-pays = {jp},
hal_id = {hal-00681781},
hal = {http://hal.inria.fr/hal-00681781/en/},
note = {\url{http://hal.inria.fr/hal-00681781/en/}}
}
@inproceedings{bormer11foveoos,
author = {Thorsten Bormer and Marc Brockschmidt and Dino Distefano and Gidon Ernst and Jean-Christophe Filli\^atre and Radu Grigore and Marieke Huisman and Vladimir Klebanov and Claude March\'e and Rosemary Monahan and Wojciech Mostowski and Nadia Polikarpova and Christoph Scheben and Gerhard Schellhorn and Bogdan Tofan and Julian Tschannen and Mattias Ulbrich},
title = {The {COST IC0701} Verification Competition 2011},
url = {http://proval.lri.fr/publications/bormer12foveoos.pdf},
crossref = {postfoveoos11},
x-type = {article},
x-equipes = {demons PROVAL ext},
topics = {team},
hal = {http://hal.inria.fr/hal-00789525}
}
@inproceedings{filliatre12aipa,
author = {Jean-Christophe Filli\^atre},
title = {{Combining Interactive and Automated Theorem Proving
in Why3 (invited talk)}},
booktitle = {{Automation in Proof Assistants 2012}},
editor = {Keijo Heljanko and Hugo Herbelin},
month = {April},
year = 2012,
topics = {team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {APA},
address = {Tallinn, Estonia}
}
@inproceedings{filliatre12boogie,
author = {Jean-Christophe Filli\^atre},
title = {{Combining Interactive and Automated Theorem Proving
using Why3 (invited tutorial)}},
booktitle = {{Second International Workshop on Intermediate Verification Languages (BOOGIE 2012)}},
editor = {Zvonimir Rakamari\'c},
month = {July},
year = 2012,
topics = {team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
x-cle-support = {BOOGIE},
address = {Berkeley, California, USA}
}
@inproceedings{conchon12cav,
author = {Sylvain Conchon and Amit Goel and Sava Krsti{\'c}
and Alain Mebsout and Fatiha Za{\"i}di},
title = {{Cubicle}: A Parallel {SMT}-based Model Checker for
Parameterized Systems},
booktitle = {CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification},
year = {2012},
topics = {team},
hal = {http://hal.archives-ouvertes.fr/hal-00799272},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL Fortesse ext},
x-type = {article},
x-support = {actes},
x-cle-support = {CAV},
editor = {Madhusudan Parthasarathy and Sanjit A. Seshia},
series = {Lecture Notes in Computer Science},
volume = 7358,
month = jul,
address = {Berkeley, California, USA},
publisher = {Springer},
abstract = { Cubicle is a new model checker for verifying safety
properties of parameterized systems. It implements a
parallel symbolic backward reachability procedure
using Satisfiabilty Modulo Theories. Experiments
done on classic and challenging mutual exclusion
algorithms and cache coherence protocols show that
Cubicle is effective and competitive with
state-of-the-art model checkers.}
}
@inproceedings{bobot12ijcar,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and
\'Evelyne Contejean and Mohamed Iguernelala and
Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
Solving Linear Integer Arithmetic},
booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
Conference on Automated Reasoning},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
series = {Lecture Notes in Computer Science},
address = {Manchester, UK},
month = jun,
volume = {7364},
pages = {67--81},
hal = {http://hal.inria.fr/hal-00687640},
doi = {10.1007/978-3-642-31365-3_8},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
type_publi = {icolcomlec},
publisher = {Springer},
abstract = {This paper describes a novel decision procedure for
quantifier-free linear integer arithmetic. Standard
techniques usually relax the initial problem to the
rational domain and then proceed either by
projection (e.g. Omega-Test) or by branching/cutting
methods (branch-and-bound, branch-and-cut, Gomory
cuts). Our approach tries to bridge the gap between
the two techniques: it interleaves an exhaustive
search for a model with bounds inference. These
bounds are computed provided an oracle capable of
finding constant positive linear combinations of
affine forms. We also show how to design an
efficient oracle based on the Simplex procedure. Our
algorithm is proved sound, complete, and terminating
and is implemented in the Alt-Ergo theorem
prover. Experimental results are promising and show
that our approach is competitive with
state-of-the-art SMT solvers.}
}
@inproceedings{filliatre12compare,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich and Aaron Stump},
title = {The 2nd Verified Software Competition: Experience Report},
booktitle = {COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems},
address = {Manchester, UK},
month = jun,
year = 2012,
hal = {http://hal.inria.fr/hal-00798777},
editor = {Vladimir Klebanov and Sarah Grebing},
publisher = {EasyChair},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {no},
x-equipes = {demons PROVAL ext},
x-support = {actes_aux},
x-cle-support = {COMPARE},
x-type = {article},
topics = {team},
abstract = {We report on the second verified software competition. It was
organized by the three authors on a 48 hours period on November
8--10, 2011. This paper describes the competition, presents the five
problems that were proposed to the participants, and gives an
overview of the solutions sent by the 29 teams that entered the
competition.},
url = {https://usr.lmf.cnrs.fr/~jcf/pub/compare2012.pdf}
}
@inproceedings{filliatre12inforum,
author = {M\'ario Pereira and Jean-Christophe Filli\^atre and
Sim{\~a}o Melo de Sousa},
title = {{ARMY}: a Deductive Verification Platform for {ARM} Programs Using {Why3}},
month = {September},
year = 2012,
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {no},
x-equipes = {demons PROVAL ext},
x-support = {rapport},
x-cle-support = {INFORUM},
x-type = {article},
topics = {team},
keywords = {Why3},
abstract = {Unstructured (low-level) programs tend to be challenging
to prove correct, since the control flow is
arbitrary complex and there are no obvious points in
the code where to insert logical assertions. In this
paper, we present a system to formally verify ARM
programs, based on a flow sequentialization
methodology and a formalized ARM semantics. This
system, built upon the why3 verification platform,
takes an annotated ARM program, turns it into a set
of purely sequential flow programs, translates these
programs' instructions into the corresponding
formalized opcodes and finally calls the Why3 VCGen
to generate the verification conditions that can
then be discharged by provers. A prototype has been
implemented and used to verify several programming
examples.},
booktitle = {INForum 2012},
url = {http://inforum.org.pt/INForum2012/docs/20120013.pdf}
}
@inproceedings{bobot12icfem,
hal = {http://hal.inria.fr/hal-00825088},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre},
title = {Separation Predicates: a Taste of Separation Logic in
First-Order Logic},
booktitle = {14th International Conference on Formal Ingineering Methods
(ICFEM)},
volume = 7635,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
address = {Kyoto, Japan},
month = {November},
year = 2012,
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL},
x-support = {article},
x-cle-support = {ICFEM},
x-type = {actes},
type_publi = {icolcomlec},
topics = {team},
abstract = {This paper introduces \emph{separation predicates}, a technique to
reuse some ideas from separation logic in the framework of program
verification using a traditional first-order logic. The purpose is
to benefit from existing specification languages, verification
condition generators, and automated theorem provers.
Separation predicates are automatically derived
from user-defined inductive predicates.
We illustrate
this idea on a non-trivial case study, namely the composite pattern,
which is specified in C/ACSL and verified in a fully automatic way
using SMT solvers Alt-Ergo, CVC3, and Z3.},
url = {http://hal.inria.fr/hal-00825088}
}
@inproceedings{boldo12cpp,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Improving Real Analysis in {Coq}: a User-Friendly Approach to Integrals and Derivatives},
booktitle = {Proceedings of the Second International Conference on Certified Programs and Proofs},
pages = {289--304},
year = {2012},
editor = {Chris Hawblitzel and Dale Miller},
volume = {7679},
optnumber = {},
series = {Lecture Notes in Computer Science},
address = {Kyoto, Japan},
month = dec,
optorganization = {},
optpublisher = {},
optnote = {},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL},
x-support = {actes},
x-cle-support = {CPP},
x-type = {article},
hal = {http://hal.inria.fr/hal-00712938},
doi = {10.1007/978-3-642-35308-6_22},
topics = {team}
}
@inproceedings{conchon12smt,
author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
title = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
pages = {12--21},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-cle-support = {SMT},
x-type = {article},
crossref = {smt2012},
topics = {team}
}
@inproceedings{dross12smt,
author = {Claire Dross and Sylvain Conchon and Johannes Kanig and Andrei Paskevich},
title = {Reasoning with Triggers},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
x-cle-support = {SMT},
crossref = {smt2012},
topics = {team}
}
@inproceedings{cousineau12fm,
author = {Denis Cousineau and
Damien Doligez and
Leslie Lamport and
Stephan Merz and
Daniel Ricketts and
Hern{\'a}n Vanzetto},
title = {{TLA+} Proofs},
pages = {147--154},
hal = {http://hal.inria.fr/hal-00726631},
x-equipes = {demons PROVAL ext},
topics = {team},
crossref = {fm2012}
}
@inproceedings{cousineau12rta,
author = {Denis Cousineau and Olivier Hermant},
title = {A Semantic Proof that Reducibility Candidates entail Cut
Elimination},
pages = {133--148},
doi = {10.4230/LIPIcs.RTA.2012.133},
hal = {http://hal.archives-ouvertes.fr/hal-00743284},
crossref = {rta12},
x-equipes = {demons PROVAL ext},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {RTA},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
topics = {team}
}
@inproceedings{benzaken13popl,
author = {V\'eronique Benzaken and Giuseppe Castagna and Kim Nguyen and J\'er\^ome Sim\'eon},
title = {Static and Dynamic Semantics of {NoSQL} Languages},
topics = {team},
hal = {http://hal.archives-ouvertes.fr/hal-00797956},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
crossref = {popl13}
}
@inproceedings{benzaken11,
author = {V\'eronique Benzaken and Jean-Daniel Fekete and Pierre-Luc H\'emery and Wael Khemiri and Ioana Manolescu},
title = {{EdiFlow: data-intensive interactive workflows for visual analytics}},
year = {2011},
booktitle = {{International Conference on Data Engineering (ICDE)}},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
crossref = {icde11}
}
@inproceedings{marche13jfla,
author = {Claude March\'e and Asma Tafat},
title = {Calcul de plus faible pr\'econdition, revisité en {Why3}},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
hal = {http://hal.inria.fr/hal-00778791}
}
@inproceedings{conchon13jfla,
author = {Sylvain Conchon and Alain Mebsout and Fatiha Za\"{\i}di},
title = {V\'erification de syst\`emes param\'etr\'es avec {Cubicle}},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL Fortesse},
x-type = {article},
x-support = {actes},
hal = {http://hal.inria.fr/hal-00778832}
}
@inproceedings{filliatre13jfla,
author = {Jean-Christophe Filli\^atre and R\'emy El Siba\"{\i}e},
title = {{Combine} : une biblioth\`eque {OCaml} pour la combinatoire},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
note = {\url{https://github.com/backtracking/combine/}},
hal = {http://hal.inria.fr/hal-00779431},
url = {http://hal.inria.fr/hal-00779431}
}
@inproceedings{mandel13jfla,
author = {Louis Mandel and C{\'e}dric Pasteur},
title = {R{\'e}activit{\'e} des syst{\`e}mes coop{\'e}ratifs : le cas de {ReactiveML}},
crossref = {jfla13},
topics = {team},
type_publi = {colcomlec},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
note = {\url{http://rml.lri.fr/jfla13}},
hal = {http://hal.inria.fr/hal-00779789},
url = {http://www.lri.fr/~mandel/publications/MandelPasteur-JFLA-2013.pdf},
abstract = {La concurrence coop{\'e}rative est un mod{\`e}le de programmation tr{\`e}s
r{\'e}pandu. On peut par exemple l'utiliser en OCaml {\`a} travers des
biblioth{\`e}ques comme Lwt, Async ou Equeue. Il a de nombreux avantages
tels que l'absence de courses critiques et des implantations l{\'e}g{\`e}res
et efficaces. N{\'e}anmoins, un des inconv{\'e}nients majeurs de ce mod{\`e}le
est qu'il d{\'e}pend de la discipline du programmeur pour garantir que le
syst{\`e}me est r{\'e}actif : un processus peut emp{\^e}cher les autres de
s'ex{\'e}cuter.
ReactiveML est un langage qui {\'e}tend OCaml avec des constructions de
concurrence coop{\'e}rative. Il propose une analyse statique, l'analyse de
r{\'e}activit{\'e}, qui permet de d{\'e}tecter les expressions qui risquent de
produire des comportements non coop{\'e}ratifs. Dans cet article, nous
pr{\'e}sentons cette analyse statique qui se d{\'e}finit {\`a} l'aide d'un syst{\`e}me
de types et effets. Ainsi, comme le typage de donn{\'e}es aide les
programmeurs {\`a} d{\'e}tecter des erreurs d'ex{\'e}cution au plus t{\^o}t, l'analyse
de r{\'e}activit{\'e} aide {\`a} d{\'e}tecter des erreurs de concurrence.}
}
@inproceedings{BaudartJacquemardMandelPouzet-EMSOFT-2013,
hal = {http://hal.inria.fr/hal-00850299},
author = {Guillaume Baudart and Florent Jacquemard and Louis Mandel and Marc Pouzet},
title = {A Synchronous Embedding of {Antescofo}, a Domain-Specific Language for Interactive Mixed Music},
booktitle = {Thirteen International Conference on Embedded Software (EMSOFT'13)},
year = 2013,
month = sep,
address = {Montreal, Canada},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
url = {http://reactiveml.org/publications/BaudartJacquemardMandelPouzet-EMSOFT-2013.pdf},
webpage = {http://reactiveml.org/emsoft13},
abstract = {Antescofo is recently developed software for \emph{musical score
following} and \emph{mixed music}: it automatically, and in
real-time, synchronizes electronic instruments with a musician playing
on a classical instrument. Therefore, it faces some of the same major
challenges as embedded systems.
The system provides a programming language used by composers to
specify musical pieces that mix interacting electronic and classical
instruments. This language is developed with and for musicians and it
continues to evolve according to their needs. Yet its semantics has
only recently been formally defined. This paper presents a
\emph{synchronous semantics} for the core language of Antescofo and
an alternative implementation based on an embedding inside an
existing synchronous language, namely ReactiveML.
The semantics reduces to a few rules, is mathematically precise and
leads to an interpretor of only a few hundred lines. The efficiency of this
interpretor compares well with that of the actual implementation: on
all musical pieces we have tested, response times have been less than
the reaction time of the human ear. Moreover, this embedding
permitted the prototyping of several new programming constructs, some
of which are described in this paper.}
}
@inproceedings{BaudartMandelPouzet-FARM-2013,
hal = {http://hal.inria.fr/hal-00850294},
author = {Guillaume Baudart and Louis Mandel and Marc Pouzet},
title = {Programming Mixed Music in {ReactiveML}},
booktitle = {ACM SIGPLAN Workshop on Functional Art, Music, Modeling and Design ({FARM'13})},
year = 2013,
month = sep,
address = {Boston, USA},
note = {Workshop ICFP 2013},
url = {http://reactiveml.org/publications/BaudartMandelPouzet-FARM-2013.pdf},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
webpage = {http://reactiveml.org/farm13},
abstract = {Mixed music is about live musicians interacting with electronic
parts which are controlled by a computer during the performance.
It allows composers to use and combine traditional instruments with
complex synthesized sounds and other electronic devices.
There are several languages dedicated to the writing of mixed music
scores. Among them, the Antescofo language coupled with an
advanced score follower allows a composer to manage the reactive
aspects of musical performances: how electronic parts interact with
a musician.
However these domain specific languages do not offer the
expressiveness of functional programming.
We embed the Antescofo language in a reactive functional
programming language, ReactiveML. This approach offers to the composer
recursion, higher order, inductive types, as well as a
simple way to program complex reactive behaviors thanks to the
synchronous model of concurrency on which ReactiveML is built.
This article presents how to program mixed music in ReactiveML through
several examples.}
}
@inproceedings{MandelPasteurPouzet-PPDP-2013,
hal = {http://hal.inria.fr/hal-00850290},
author = {Louis Mandel and C{\'e}dric Pasteur and Marc Pouzet},
title = {Time Refinement in a Functional Synchronous Language},
booktitle = {Proceedings of 15th {ACM SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP'13})},
year = 2013,
address = {Madrid, Spain},
month = sep,
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
url = {http://reactiveml.org/publications/MandelPasteurPouzet-PPDP-2013.pdf},
webpage = {http://reactiveml.org/ppdp13},
abstract = {Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent.
We propose an extension of the synchronous model of concurrency, called \emph{reactive domains}, to simplify the programming of such systems. Reactive domains allow the creation of local time scales and enable \emph{refinement}, that is, the replacement of an approximation of a system with a more detailed version without changing its behavior as observed by the rest of the program.
Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We present an operational semantics for the extended language and a type system that ensures the soundness of programs.}
}
@inproceedings{mandel12cp,
author = {Vijay Saraswat and David Cunningham and Liana Hadarean and Louis Mandel and Avraham Shinnar and Olivier Tardieu},
title = {Constrained Types - Future Directions},
booktitle = {18th International Conference on Principles and Practice of Constraint Programming},
year = 2012,
month = oct,
address = {Qu{\'e}bec City, Canada},
note = {Position Paper},
url = {http://www.lri.fr/~mandel/publications/SaraswatCunninghamHadareanMandelShinnarTardieu-CP-2012.pdf},
abstract = {The use of constraints in types is quite natural. Yet, integrating constraint based types into the heart of a modern, statically typed, object-oriented programming language is quite tricky. Over the last five years we have designed and implemented the constrained types framework in the programming language X10. In this paper we review the conceptual design, the practical implementation issues, and the many new questions that are raised. We expect the pursuit of these questions to be a profitable area of future work.},
topics = {team},
type_publi = {colloque},
x-equipes = {demons PROVAL ext},
hal = {http://hal.inria.fr/hal-00798046}
}
@inproceedings{paskevich13cade,
hal = {http://hal.inria.fr/hal-00825086},
author = {Jasmin C. Blanchette and Andrei Paskevich},
title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
crossref = {cade13},
x-equipes = {demons PROVAL},
x-type = {article},
topics = {team},
url = {http://www4.in.tum.de/~blanchet/tff1short.pdf}
}
@inproceedings{boldo13arith,
author = {Sylvie Boldo},
title = {How to Compute the Area of a Triangle: a Formal Revisit},
booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
address = {Austin, Texas, USA},
year = {2013},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-international-audience = {yes},
x-proceedings = {yes},
hal = {http://hal.inria.fr/hal-00790071}
}
@inproceedings{bolmel13arith,
author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
address = {Austin, Texas, USA},
year = {2013},
topics = {team},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-international-audience = {yes},
x-proceedings = {yes},
hal = {http://hal.inria.fr/hal-00743090}
}
@inproceedings{filliatre13esop,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Why3 --- Where Programs Meet Provers},
booktitle = {Proceedings of the 22nd European Symposium on Programming},
month = mar,
year = 2013,
volume = {7792},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthias Felleisen and Philippa Gardner},
pages = {125--128},
hal = {http://hal.inria.fr/hal-00789533},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{chargueraud13esop,
author = {Arthur Chargu{\'e}raud},
title = {Pretty-Big-Step Semantics},
booktitle = {Proceedings of the 22nd European Symposium on Programming},
month = mar,
year = 2013,
volume = {7792},
editor = {Matthias Felleisen and Philippa Gardner},
pages = {41--60},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
hal = {http://hal.inria.fr/hal-00798227},
topics = {team,lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{chargueraud13ppopp,
author = {Umut A. Acar and Arthur Chargu{\'e}raud and Mike Rainey},
title = {Scheduling parallel programs by work stealing with private deques},
booktitle = {Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming},
month = feb,
year = 2013,
series = {PPoPP '13},
pages = {219-228},
publisher = {ACM Press},
doi = {10.1145/2442516.2442538},
hal = {http://hal.inria.fr/hal-00863028},
topics = {team,lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {PPOPP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre13plmw,
author = {Jean-Christophe Filli\^atre},
title = {{Deductive Program Verification}},
booktitle = {{Programming Languages Mentoring Workshop (PLMW 2013)}},
editor = {Nate Foster and Philippa Gardner and Alan Schmitt and
Gareth Smith and Peter Thieman and Tobias Wrigstad},
month = {January},
hal = {http://hal.inria.fr/hal-00799190},
year = 2013,
topics = {team},
type_digiteo = {conf_autre},
type_publi = {colloque},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {no},
x-invited-conference = {yes},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {actes},
address = {Rome, Italy}
}
@inproceedings{filliatre13cade,
author = {Jean-Christophe Filli\^atre},
title = {One Logic To Use Them All},
crossref = {cade13},
pages = {1--20},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-invited-conference = {yes},
hal = {http://hal.inria.fr/hal-00809651/en/}
}
@inproceedings{bobot13vstte,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
hal = {http://hal.inria.fr/hal-00875395},
title = {Preserving User Proofs Across Specification Changes},
crossref = {vstte13},
pages = {191--201},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{IshMelNak13,
hal = {http://hal.inria.fr/hal-00806701},
author = {Daisuke Ishii and Guillaume Melquiond and Shin Nakajima},
title = {Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus},
booktitle = {Proceedings of the 10th Conference on Integrated Formal Methods},
editor = {Einar Broch Johnsen and Luigia Petre},
address = {Turku, Finland},
year = {2013},
pages = {139--153},
series = {Lecture Notes in Computer Science},
volume = {7940},
doi = {10.1007/978-3-642-38613-8_10},
topics = {team,lri},
type_publi = {icolcomlec}
}
@inproceedings{kanig12hilt,
topics = {team},
author = {Johannes Kanig and Edmond Schonberg and Claire Dross},
title = {{Hi-Lite}: the convergence of compiler technology and program
verification},
pages = {27--34},
editor = {Ben Brosgol and Jeff Boleng and S. Tucker Taft},
booktitle = {Proceedings of the 2012 ACM Conference on High Integrity
Language Technology, HILT '12},
address = {Boston, USA},
publisher = {ACM Press},
year = 2012
}
@inproceedings{clochard14plpv,
hal = {http://hal.inria.fr/hal-00913431},
topics = {team},
author = {Martin Clochard and Claude March\'e and Andrei Paskevich},
title = {Verified Programs with Binders},
booktitle = {Programming Languages meets Program Verification (PLPV)},
year = 2014,
publisher = {ACM Press},
type_digiteo = {conf_isbn},
type_publi = {colloque},
x-equipes = {demons Toccata},
x-support = {actes},
x-cle-support = {PLPV}
}
@inproceedings{castagna14popl,
hal = {http://hal.archives-ouvertes.fr/hal-00880744},
topics = {team},
author = {Giuseppe Castagna and Hyeonseung Im and Serge{\"\i} Lenglet and Kim Nguyen and Luca Padovani and Zhiwu Xu},
title = {Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation},
crossref = {popl2014}
}
@inproceedings{castagna15popl,
hal = {},
topics = {team},
author = {Giuseppe Castagna and Kim Nguyen and Zhiwu Xu and Pietro Abate},
title = {Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. },
crossref = {popl2015}
}
@inproceedings{clochard14popl,
hal = {http://hal.inria.fr/hal-00920955},
topics = {team},
author = {M. Clochard and S. Chaudhuri and A. Solar-Lezama},
title = {Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search},
crossref = {popl2014}
}
@inproceedings{bodin14popl,
hal = {http://hal.inria.fr/hal-00910135},
topics = {team},
author = {M. Bodin and A. Chargu{\'e}raud and D. Filaretti and P. Gardner and S. Maffeis and D. Naudziuniene and A. Schmitt and G. Smith},
title = {A Trusted Mechanised {JavaScript} Specification},
crossref = {popl2014}
}
@inproceedings{filliatre14cav,
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
pages = {1--16},
crossref = {cav2014},
topics = {team},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
hal_id = {hal-00873187},
hal = {http://hal.archives-ouvertes.fr/hal-00873187/en/},
pdf = {http://hal.archives-ouvertes.fr/hal-00873187/PDF/main.pdf},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without any observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.
}
}
@inproceedings{delahaye14afadl,
topics = {team},
hal_id = {hal-00998094},
hal = {http://hal.inria.fr/hal-00998094/en/},
title = {Le projet {BWare} : une plate-forme pour la v{\'e}rification automatique d'obligations de preuve {B}},
author = {Delahaye, David and March{\'e}, Claude and Mentr{\'e}, David},
abstract = {Le projet de recherche industrielle BWare (ANR-12-INSE-0010) est financ{\'e} pour 4 ans par le programme \emph{Ing{\'e}nierie Num{\'e}rique \& S{\'e}curit{\'e}} (INS) de l'Agence Nationale de la Recherche (ANR) et a d{\'e}but{\'e} en septembre 2012 (voir le site web du projet : \url{http://bware.lri.fr}). Le consortium du projet BWare associe les partenaires acad{\'e}miques Cedric, LRI, et Inria, ainsi que les partenaires industriels Mitsubishi Electric R\&D Centre Europe (MERCE), ClearSy, et OCamlPro},
booktitle = {Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels (AFADL)},
publisher = {EasyChair},
address = {Paris, France},
audience = {nationale},
year = 2014,
month = jun
}
@inproceedings{delahaye14abz,
topics = {team},
crossref = {abz2014},
hal_id = {hal-00998092},
hal = {http://hal.inria.fr/hal-00998092/en/},
title = {The {BWare} Project: Building a Proof Platform for the Automated Verification of {B} Proof Obligations},
author = {Delahaye, David and Dubois, Catherine and March{\'e}, Claude and Mentr{\'e}, David},
abstract = { We introduce BWare, an industrial research project
that aims to provide a mechanized framework to
support the automated veri cation of proof
obligations coming from the development of
industrial applications using the B method and
requiring high integrity. The methodology adopted
consists in building a generic verification platform
relying on di erent theorem provers, such as rst
order provers and SMT (Satisfiability Modulo
Theories) solvers. Beyond the multi-tool aspect of
our methodology, the originality of this project
also resides in the requirement for the veri cation
tools to produce proof objects, which are to be
checked independently. In this paper, we present
some preliminary results of BWare, as well as some
current major lines of work},
language = {Anglais},
affiliation = {Centre d'Etude et De Recherche en Informatique du Cnam - CEDRIC , TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , Mitsubishi Electric R\&D Centre Europe [France] - MERCE-France},
pages = {290--293}
}
@inproceedings{conchon14abz,
topics = {team},
hal = {https://hal.inria.fr/hal-01093000},
author = {Sylvain Conchon and Mohamed Iguernelala},
title = {Tuning the {Alt-Ergo} {SMT} Solver for {B} Proof Obligations},
pages = {294--297},
year = 2014,
crossref = {abz2014},
doi = {10.1007/978-3-662-43652-3_27}
}
@inproceedings{cfmp14vstte,
hal = {http://hal.inria.fr/hal-01067197},
author = {Martin Clochard and Jean-Christophe
Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Formalizing Semantics with an Automatic Program
Verifier},
pages = {37--51},
crossref = {vstte14},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{cfp15vstte,
hal = {http://hal.inria.fr/hal-01162661},
author = {Martin Clochard and Jean-Christophe
Filli\^atre and Andrei Paskevich},
title = {How to avoid proving the absence of integer overflows},
pages = {94--109},
crossref = {vstte15},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{clochard14vstte,
hal = {http://hal.inria.fr/hal-01067217},
author = {Martin Clochard},
title = {Automatically verified implementation of data structures
based on {AVL} trees},
pages = {167--180},
crossref = {vstte14},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{conchon13fmcad,
topics = {team},
hal = {http://hal.archives-ouvertes.fr/hal-00924640},
title = {Invariants for Finite Instances and Beyond},
author = {Conchon, Sylvain and Goel, Amit and Krsti{\'c}, Sava and Mebsout, Alain and Za{\"\i}di, Fatiha},
abstract = {Verification of safety properties of concurrent programs with an arbitrary numbers of processes is an old challenge. In particular, complex parameterized protocols like FLASH are still out of the scope of state-of-the-art model checkers. In this paper, we describe a new algorithm, called Brab, that is able to automatically infer invariants strong enough to prove a protocol like FLASH. Brab computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system. These approximations (candidate invariants) are then model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.},
booktitle = {FMCAD},
pages = {61--68},
address = {Portland, Oregon, {\'E}tats-Unis},
audience = {internationale},
doi = {10.1109/FMCAD.2013.6679392},
year = 2013,
month = oct
}
@inproceedings{conchon14jfla,
hal = {https://hal.inria.fr/hal-01088655},
topics = {team},
author = {Sylvain Conchon and David Declerck and Luc Maranget and Alain Mebsout},
title = {Vérification de programmes {C} concurrents avec {Cubicle} : Enfoncer les barrières},
crossref = {jfla14}
}
@inproceedings{filliatre14jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre},
title = {Le petit guide du bouturage, ou comment r\'ealiser des arbres mutables en {OCaml}},
crossref = {jfla14},
note = {\url{https://usr.lmf.cnrs.fr/~jcf/publis/bouturage.pdf}}
}
@inproceedings{clochard15jfla,
hal = {https://hal.inria.fr/hal-01094488},
topics = {team},
author = {Martin Clochard and L\'eon Gondelman},
title = {Double {WP}: vers une preuve automatique d'un compilateur},
crossref = {jfla15}
}
@inproceedings{acar14esa,
topics = {team},
title = {Theory and Practice of Chunked Sequences},
author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
hal = {https://hal.inria.fr/hal-01087245},
booktitle = {European Symposium on Algorithms},
address = {Wroclaw, Poland},
editor = {Schulz, AndreasS. and Wagner, Dorothea},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8737,
pages = {25--36},
year = 2014,
month = sep,
doi = {10.1007/978-3-662-44777-2_3},
keywords = {Data structure ; Sequence ; Chunk ; Amortization}
}
@inproceedings{lelay15coq,
topics = {team},
title = {How to express convergence for analysis in {Coq}},
author = {Lelay, Catherine},
hal = {https://hal.archives-ouvertes.fr/hal-01169321},
booktitle = {The 7th Coq Workshop},
address = {Sophia Antipolis, France},
year = 2015,
month = jun,
keywords = {Coq proof assistant ; Analysis ; Limits ; Filters ; Type-Classes ; Canonical Structures}
}
@inproceedings{conchon13synasc,
topics = {team},
author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo},
year = 2013,
doi = {10.1109/SYNASC.2013.29},
booktitle = {15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
pages = {161--168}
}
@inproceedings{lelay14jfla,
topics = {team},
title = {{Coq passe le bac}},
author = {Lelay, Catherine},
booktitle = {{JFLA - Journ{\'e}es francophones des langages applicatifs}},
address = {Fr{\'e}jus, France},
year = {2014},
month = jan,
x-proceedings = {no},
x-international-audience = {no},
x-editorial-board = {yes},
x-invited-conference = {yes},
x-scientific-popularization = {no}
}
@inproceedings{pereira16jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {It\'erer avec confiance},
crossref = {jfla16},
hal = {https://hal.inria.fr/hal-01240891}
}
@inproceedings{pereira16nfm,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {A Modular Way to Reason About Iteration},
crossref = {nfm16},
abstract = { In this paper we present an approach to specify
programs performing iterations. The idea is to
specify iteration in terms of the nite sequence of
the elements enumerated so far, and only those. In
particular, we are able to deal with
non-deterministic and possibly innite iteration. We
show how to cope with the issue of an iteration no
longer being consistent with mutable data. We
validate our proposal using the deductive verication
tool Why3 and two iteration paradigms, namely
cursors and higher-order iterators. For each
paradigm, we verify several implementations of
iterators and client code. This is done in a modular
way, i.e., the client code only relies on the
specication of the iteration. },
hal = {https://hal.inria.fr/hal-01281759}
}
@inproceedings{fumex16nfm,
topics = {team},
author = {Fumex, Cl\'ement and Dross, Claire and Gerlach, Jens and March\'e, Claude},
title = {Specification and Proof of High-Level Functional Properties of Bit-Level Programs},
pages = {291--306},
crossref = {nfm16},
hal = {https://hal.inria.fr/hal-01314876}
}
@inproceedings{hauzar16sefm,
topics = {team},
author = {Hauzar, David and March\'e, Claude and Moy, Yannick},
title = {Counterexamples from Proof Failures in {SPARK}},
booktitle = {Software Engineering and Formal Methods},
year = 2016,
pages = {215--233},
doi = {10.1007/978-3-319-41591-8_15},
editor = {De Nicola, Rocco and Eva K\"uhn},
series = {Lecture Notes in Computer Science},
address = {Vienna, Austria},
hal = {https://hal.inria.fr/hal-01314885}
}
@inproceedings{filliatre16,
topics = {team},
author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
title = {Producing All Ideals of a Forest, Formally (Verification Pearl)},
crossref = {vstte16},
hal = {https://hal.inria.fr/hal-01316859}
}
@inproceedings{clochard16,
topics = {team},
author = {Martin Clochard and L\'eon Gondelman and M\'ario Pereira},
title = {The {Matrix} Reproved},
crossref = {vstte16},
hal = {https://hal.inria.fr/hal-01316902}
}
@inproceedings{kosmatov16isola,
topics = {team},
title = {Static versus Dynamic Verification in {Why3}, {Frama-C} and {SPARK
2014}},
author = {Kosmatov, Nikolai and March{\'e}, Claude and Moy, Yannick and
Signoles, Julien},
hal = {https://hal.inria.fr/hal-01344110},
booktitle = {7th International Symposium on Leveraging Applications of Formal
Methods, Verification and Validation (ISoLA)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
year = 2016,
pages = {461--478},
volume = {9952},
editor = {Tiziana Margaria and Bernhard Steffen},
address = {Corfu, Greece},
month = oct,
doi = {10.1007/978-3-319-47166-2_32}
}
@inproceedings{boldo16nsv,
title = {{Computing a correct and tight rounding error bound using
rounding-to-nearest}},
author = {Boldo, Sylvie},
hal = {https://hal.inria.fr/hal-01377152},
booktitle = {{9th International Workshop on Numerical Software Verification}},
address = {Toronto, Canada},
year = {2016},
month = jul,
pdf = {https://hal.inria.fr/hal-01377152/file/article.pdf},
topics = {team}
}
@inproceedings{boldo16hccv,
title = {{Iterators: where folds fail}},
author = {Boldo, Sylvie},
hal = {https://hal.inria.fr/hal-01377155},
booktitle = {{Workshop on High-Consequence Control Verification}},
address = {Toronto, Canada},
year = {2016},
month = jul,
pdf = {https://hal.inria.fr/hal-01377155/file/abstract.pdf},
topics = {team}
}
@inproceedings{chargueraud:hal-01245872,
topics = {team},
title = {{Machine-Checked Verification of the Correctness and Amortized
Complexity of an Efficient Union-Find Implementation}},
author = {Chargu\'eraud, Arthur and Pottier, Fran\c{c}ois},
booktitle = {{6th International Conference on Interactive Theorem Proving
(ITP)}},
address = {Nanjing, China},
year = 2015,
month = aug,
doi = {10.1007/978-3-319-22102-1\_9},
hal = {https://hal.inria.fr/hal-01245872},
pdf = {https://hal.inria.fr/hal-01245872/document},
hal_id = {hal-01245872},
hal_version = {v1},
x-proceedings = {yes},
x-international-audience = {yes},
x-editorial-board = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{acar:hal-01245837,
topics = {team},
title = {{A Work-Efficient Algorithm for Parallel Unordered Depth-First
Search}},
author = {Acar, Umut A. and Chargu\'eraud, Arthur and Rainey, Mike},
booktitle = {{Proceedings of the International Conference for High Performance
Computing, Networking, Storage and Analysis}},
address = {Austin, Texas, United States},
year = {2015},
month = nov,
doi = {10.1145/2807591.2807651},
hal = {https://hal.inria.fr/hal-01245837},
pdf = {https://hal.inria.fr/hal-01245837/document},
hal_id = {hal-01245837},
hal_version = {v1},
x-proceedings = {yes},
x-international-audience = {yes},
x-editorial-board = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{boldo:hal-01391578,
topics = {team},
title = {{A Coq Formal Proof of the Lax-Milgram theorem}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian
and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-01391578},
booktitle = {{Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
series = {CPP 2017},
location = {Paris, France},
year = {2017},
month = jan,
pages = {79--89},
pdf = {https://hal.inria.fr/hal-01391578/file/article.pdf},
doi = {10.1145/3018610.3018625},
publisher = {ACM},
address = {New York, NY, USA}
}
@inproceedings{chargueraud:hal-01245865,
topics = {team},
title = {{Higher-Order Representation Predicates in Separation Logic}},
author = {Chargu{\'e}raud, Arthur},
hal = {https://hal.inria.fr/hal-01245865},
booktitle = {{Proceedings of the 5th ACM SIGPLAN Conference on Certified
Programs and Proofs}},
address = {Saint Petersburg, Florida, United States},
year = {2016},
month = jan,
hal_id = {hal-01245865},
hal_version = {v1}
}
@inproceedings{mahboubi16itp,
topics = {team},
title = {Formally Verified Approximations of Definite Integrals},
author = {Mahboubi, Assia and Melquiond, Guillaume and Sibut-Pinote, Thomas},
hal = {https://hal.inria.fr/hal-01289616},
booktitle = {Proceedings of the 7th International Conference on Interactive Theorem Proving},
address = {Nancy, France},
editor = {Jasmin Christian Blanchette and Stephan Merz},
series = {Lecture Notes in Computer Science},
volume = {9807},
year = {2016},
month = aug,
doi = {10.1007/978-3-319-43144-4\_17},
pdf = {https://hal.inria.fr/hal-01289616/file/main.pdf},
hal_id = {hal-01289616},
hal_version = {v2}
}
@inproceedings{chen17jfla,
topics = {team},
author = {Ran Chen and Jean-Jacques L\'evy},
title = {Une preuve formelle de l'algorithme de {Tarjan-1972} pour trouver les composantes fortement connexes dans un graphe},
crossref = {jfla17},
hal = {https://hal.inria.fr/hal-01405424}
}
@inproceedings{clochard17jfla,
topics = {team},
title = {{Preuves taill{\'e}es en biseau}},
author = {Clochard, Martin},
hal = {https://hal.inria.fr/hal-01404935},
crossref = {jfla17}
}
@inproceedings{pereira17jfla,
topics = {team},
title = {{D{\'e}fonctionnaliser pour prouver}},
author = {Pereira, M{\'a}rio},
hal = {https://hal.inria.fr/hal-01378068},
crossref = {jfla17}
}
@inproceedings{conchon17cav,
author = {Sylvain Conchon and Mohamed Iguernlala and Kailiang Ji and
Guillaume Melquiond and Cl\'ement Fumex},
topics = {team},
hal = {https://hal.inria.fr/hal-01522770},
title = {A Three-tier Strategy for Reasoning about
Floating-Point Numbers in {SMT}},
booktitle = {Computer Aided Verification},
year = 2017,
pages = {419--435},
series = {Lecture Notes in Computer Science},
volume = 10427,
doi = {10.1007/978-3-319-63390-9_22}
}
@inproceedings{rieuhelft17jfla,
topics = {team},
title = {Result graphs for an abstract interpretation-based static analyzer},
author = {Rapha{\"e}l Rieu-Helft and Pascal Cuoq},
crossref = {jfla17}
}
@inproceedings{fumex17vstte,
topics = {team},
hal = {https://hal.inria.fr/hal-01534533/},
author = {Cl\'ement Fumex and Claude March\'e and Yannick Moy},
title = {Automating the Verification of Floating-Point Programs},
crossref = {vstte17}
}
@inproceedings{jeannerod17vstte,
topics = {team},
hal = {https://hal.inria.fr/hal-01534747},
author = {Nicolas Jeannerod and Claude March\'e and Ralf Treinen},
title = {A Formally Verified Interpreter for a Shell-like Programming
Language},
crossref = {vstte17}
}
@inproceedings{boldo17arith,
topics = {team},
title = {Round-off Error Analysis of Explicit One-Step Numerical Integration Methods},
author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
hal = {https://hal.archives-ouvertes.fr/hal-01581794},
booktitle = {24th IEEE Symposium on Computer Arithmetic},
address = {London, United Kingdom},
year = {2017},
month = jul,
doi = {10.1109/ARITH.2017.22},
pdf = {https://hal.archives-ouvertes.fr/hal-01581794/file/arith_hal.pdf}
}
@inproceedings{boldo17itp,
topics = {team},
title = {Formal Verification of a Floating-Point Expansion Renormalization Algorithm},
author = {Boldo, Sylvie and Joldes, Mioara and Muller, Jean-Michel and Popescu, Valentina},
hal = {https://hal.archives-ouvertes.fr/hal-01512417},
year = {2017},
month = sep,
pdf = {https://hal.archives-ouvertes.fr/hal-01512417/file/itp17.pdf},
booktitle = {Proceedings of the 8th International Conference on Interactive Theorem Proving},
address = {Brasilia, Brazil}
}
@inproceedings{BCF17b,
topics = {team},
title = {Preuve formelle du th{\'e}or{\`e}me de {Lax--Milgram}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.archives-ouvertes.fr/hal-01581807},
booktitle = {{16{\`e}mes journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels}},
address = {Montpellier, France},
year = {2017},
month = jun,
pdf = {https://hal.archives-ouvertes.fr/hal-01581807/file/article_afadl.pdf}
}
@inproceedings{Faissole17,
topics = {team},
title = {{Formalization and closedness of finite dimensional subspaces}},
author = {Faissole, Florian},
url = {https://hal.inria.fr/hal-01630411},
booktitle = {{SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing}},
address = {Timisoara, Romania},
year = {2017},
month = sep,
keywords = {filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq},
pdf = {https://hal.inria.fr/hal-01630411/file/synasc_hal.pdf},
hal_id = {hal-01630411},
hal_version = {v1}
}
@inproceedings{acar:hal-01409022,
topics = {team},
title = {Dag-calculus: a calculus for parallel computation},
author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike and Sieczkowski, Filip},
hal = {https://hal.inria.fr/hal-01409022},
booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP)},
address = {Nara, Japan},
pages = {18--32},
year = 2016,
month = sep,
doi = {10.1145/2951913.2951946}
}
@inproceedings{chen17vstte,
topics = {team},
title = {A Semi-automatic Proof of Strong connectivity},
author = {Chen, Ran and L{\'e}vy, Jean-Jacques},
hal = {https://hal.inria.fr/hal-01632947},
booktitle = {9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
address = {Heidelberg, Germany},
year = 2017,
month = jul
}
@inproceedings{rieuhelft17vstte,
topics = {team},
title = {How to Get an Efficient yet Verified Arbitrary-Precision Integer Library},
author = {Rieu-Helft, Rapha{\"e}l and March{\'e}, Claude and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01519732},
booktitle = {9th Working Conference on Verified Software: Theories, Tools, and Experiments},
address = {Heidelberg, Germany},
series = {Lecture Notes in Computer Science},
volume = 10712,
year = 2017,
month = jul,
pages = {84--101},
doi = {10.1007/978-3-319-72308-2_6},
keywords = {arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier},
pdf = {https://hal.inria.fr/hal-01519732/file/main.pdf}
}
@inproceedings{spitters18jfla,
topics = {team},
crossref = {jfla18},
title = {Preuves constructives de programmes probabilistes},
author = {Faissole, Florian and Spitters, Bas},
hal = {https://hal.inria.fr/hal-01654459},
hal_id = {hal-01654459},
hal_version = {v1}
}
@inproceedings{faissole18jfla,
topics = {team},
crossref = {jfla18},
title = {D{\'e}finir le fini : deux formalisations d'espaces de dimension finie},
author = {Faissole, Florian},
hal = {https://hal.inria.fr/hal-01654457},
pdf = {https://hal.inria.fr/hal-01654457/file/jfla.pdf},
hal_id = {hal-01654457},
hal_version = {v1}
}
@inproceedings{rieuhelft18jfla,
topics = {team},
crossref = {jfla18},
title = {{Un m{\'e}canisme d'extraction vers C pour Why3}},
author = {Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-01653153},
pdf = {https://hal.inria.fr/hal-01653153/file/main.pdf},
hal_id = {hal-01653153},
hal_version = {v1}
}
@inproceedings{fpds18jfla,
topics = {team},
crossref = {jfla18},
title = {V{\'e}rification de programmes fortement imp{\'e}ratifs avec {W}hy3},
author = {Jean-Christophe Filli{\^a}tre and M{\'a}rio Pereira and
Sim{\~a}o Melo de Sousa},
hal = {https://hal.inria.fr/hal-01649989},
pdf = {https://hal.inria.fr/hal-01649989/file/main.pdf},
hal_id = {hal-01649989},
hal_version = {v2}
}
@inproceedings{conchon17icfem,
topics = {team},
author = {Conchon, Sylvain and Declerck, David and Za{\"i}di, Fatiha},
editor = {Duan, Zhenhua and Ong, Luke},
title = {Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-W},
booktitle = {International Conference on Formal Engineering Methods},
year = 2017,
series = {Lecture Notes in Computer Science},
number = 10610,
pages = {88--104}
}
@inproceedings{boldo18arith,
topics = {team},
title = {A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers},
author = {Boldo, Sylvie and Faissole, Florian and Tourneur, Vincent},
hal = {https://hal.inria.fr/hal-01772272},
booktitle = {25th IEEE Symposium on Computer Arithmetic},
address = {Amherst, MA, United States},
year = 2018,
month = jun
}
@inproceedings{melquiond18ijcar,
topics = {team},
title = {A {Why3} Framework for Reflection Proofs and its Application to {GMP}'s Algorithms},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-01699754},
booktitle = {9th International Joint Conference on Automated Reasoning},
address = {Oxford, United Kingdom},
editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
series = {Lecture Notes in Computer Science},
year = 2018,
month = jul
}
@inproceedings{roux18tacas,
topics = {team},
title = {A Non-linear Arithmetic Procedure for Control-Command Software Verification},
author = {Roux, Pierre and Iguernlala, Mohamed and Conchon, Sylvain},
hal = {https://hal.archives-ouvertes.fr/hal-01737737},
booktitle = {24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
address = {Thessalonique, Greece},
year = 2018,
month = apr
}
@inproceedings{dailler2018,
topics = {team},
hal = {https://hal.inria.fr/hal-01936302},
author = {Dailler, Sylvain and March{\'e}, Claude and Moy, Yannick},
title = {Lightweight Interactive Proving inside an Automatic Program
Verifier},
booktitle = {Proceedings of the Fourth Workshop on Formal Integrated
Development Environment, F-IDE, Oxford, UK,
July 14, 2018},
year = {2018},
doi = {10.4204/EPTCS.284.1}
}
@inproceedings{faissole:hal-01405762,
topics = {team},
title = {Synthetic topology in {HoTT} for probabilistic programming},
author = {Faissole, Florian and Spitters, Bas},
booktitle = {The Third International Workshop on Coq for Programming Languages (CoqPL 2017)},
address = {Paris, France},
year = 2017,
month = jan,
hal = {https://hal.inria.fr/hal-01405762}
}
@inproceedings{clochard20popl,
topics = {team},
title = {Deductive Verification with Ghost Monitors},
author = {Clochard, Martin and March\'e, Claude and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-02368284},
booktitle = {Principles of Programming Languages},
address = {New Orleans, United States},
year = 2020,
doi = {10.1145/3371070}
}
@inproceedings{conchon17fmcad,
topics = {team},
hal = {https://hal.inria.fr/hal-01927220},
author = {Sylvain Conchon and
Amit Goel and
Sava Krstic and
Rupak Majumdar and
Mattias Roux},
title = {{FAR-Cubicle} - {A} new reachability algorithm for {Cubicle}},
booktitle = {Formal Methods in Computer Aided Design},
pages = {172--175},
year = 2017,
doi = {10.23919/FMCAD.2017.8102256},
editor = {Daryl Stewart and Georg Weissenbacher}
}
@inproceedings{rieuhelft19jfla,
topics = {team},
title = {Un m{\'e}canisme de preuve par r{\'e}flexion pour {Why3} et son application aux algorithmes de {GMP}},
author = {Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-01943010},
crossref = {jfla19}
}
@inproceedings{galloiswong19jfla,
topics = {team},
title = {Formalisation en {Coq} d'algorithmes de filtres num{\'e}riques},
author = {Gallois-Wong, Diane},
hal = {https://hal.inria.fr/hal-01929531},
booktitle = {30{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
year = 2019,
month = jan
}
@inproceedings{gospelfm19,
topics = {team},
crossref = {fm19},
author = {Arthur Chargu\'eraud and Jean-Christophe Filli\^atre and Cl\'audio Belo Louren\c{c}o and M\'ario Pereira},
title = {{GOSPEL} --- Providing {OCaml} with a Formal Specification Language},
hal = {https://hal.inria.fr/hal-02157484}
}
@inproceedings{filliatre19jfla,
author = {Jean-Christophe Filli\^atre},
title = {Retour sur 25 ans de programmation avec {OCaml}},
crossref = {jfla19},
note = {S\'eminaire invit\'e},
hal = {https://hal.inria.fr/hal-02406208},
topics = {team, lri},
type_publi = {diffusion},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-support = {diffusion},
x-invited-conference = {yes}
}
@inproceedings{filliatre18itp,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification},
crossref = {itp2018},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre18fide,
author = {Jean-Christophe Filli\^atre},
title = {Auto-active verification using {Why3}'s {IDE}},
booktitle = {4th Workshop on Formal Integrated Development Environment},
year = 2018,
month = jul,
address = {Oxford, UK},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre17keysymposium,
author = {Jean-Christophe Filli\^atre},
title = {{Why3} --- where programs meet provers},
booktitle = {KeY Symposium 2017},
year = 2017,
month = oct,
address = {Rastatt, Germany},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre17verifythis,
author = {Jean-Christophe Filli\^atre},
title = {{Why3} Tutorial},
booktitle = {VerifyThis 2017},
year = 2017,
month = apr,
address = {Uppsala, Sweden},
note = {Invited tutorial},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre17framacsparkday,
author = {Jean-Christophe Filli\^atre},
title = {The {Why3} tool for deductive verification and verified {OCaml} libraries},
booktitle = {Frama-C \& SPARK Day 2019},
year = 2019,
month = jun,
address = {Paris, France},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre14msc,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification with {Why3}},
booktitle = {Mathematical Structures of Computation --- Formal Proof, Symbolic Computation and Computer Arithmetic},
year = 2014,
month = feb,
address = {Lyon, France},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre13msr,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification with {Why3}},
booktitle = {MSR-Inria Joint Centre ``Spring Day''},
year = 2013,
month = may,
address = {Lyon, France},
note = {Invited talk},
topics = {team, lri},
type_publi = {colloque},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{filliatre19ifm,
author = {Jean-Christophe Filli\^atre},
title = {Deductive Verification of {OCaml} Libraries},
booktitle = {15th International Conference on integrated Formal Methods},
year = 2019,
month = dec,
address = {Bergen, Norway},
note = {Invited talk},
topics = {team, lri},
hal = {https://hal.inria.fr/hal-02406253},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes}
}
@inproceedings{becker19vstte,
topics = {team},
title = {Ghost Code in Action: Automated Verification of a Symbolic Interpreter},
author = {Becker, Benedikt and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-02276257},
booktitle = {Verified Software: Tools, Techniques and Experiments},
address = {New York, United States},
editor = {Supratik Chakraborty and Jorge A.Navas},
series = {Lecture Notes in Computer Science},
volume = 12031,
year = 2019,
month = jul,
doi = {10.1007/978-3-030-41600-3_8}
}
@inproceedings{conchon18smt,
topics = {team},
title = {{Alt-Ergo} 2.2},
author = {Conchon, Sylvain and Coquereau, Albin and Iguernlala, Mohamed and Mebsout, Alain},
hal = {https://hal.inria.fr/hal-01960203},
booktitle = {SMT Workshop: International Workshop on Satisfiability Modulo Theories},
address = {Oxford, United Kingdom},
year = 2018,
month = jul,
pdf = {https://hal.inria.fr/hal-01960203/file/Alt-Ergo-2.2--SMT-Workshop-2018.pdf},
hal_id = {hal-01960203},
hal_version = {v1}
}
@inproceedings{filliatre20jfla,
topics = {team},
author = {Jean-Christophe Filli\^atre},
title = {Mesurer la hauteur d'un arbre},
crossref = {jfla20},
topics = {team},
note = {\url{https://usr.lmf.cnrs.fr/~jcf/hauteur/}},
x-slides = {https://usr.lmf.cnrs.fr/~jcf/hauteur/pres-hauteur.pdf},
hal = {https://hal.inria.fr/hal-02315541}
}
@inproceedings{blot19jfla,
topics = {team},
title = {{SMTCoq}: automatisation expressive et extensible dans {Coq}},
author = {Blot, Valentin and Bousalem, Amina and Garchery, Quentin and Keller, Chantal},
hal = {https://hal.archives-ouvertes.fr/hal-02369249},
crossref = {jfla19}
}
@inproceedings{melquiond19jfla,
topics = {team},
title = {Computer Arithmetic and Formal Proofs},
author = {Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-02013540},
crossref = {jfla19}
}
@inproceedings{kawamura19tamc,
topics = {team},
title = {Second-Order Linear-Time Computability with Applications to Computable Analysis},
author = {Kawamura, Akitoshi and Steinberg, Florian and Thies, Holger},
hal = {https://hal.inria.fr/hal-02148490},
booktitle = {15th Annual Conference Theory and Applications of Models of Computation},
address = {Tokyo, Japan},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 11436,
pages = {337--358},
year = 2019,
month = apr
}
@inproceedings{melquiond19arith,
topics = {team},
title = {Formal Verification of a State-of-the-Art Integer Square Root},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha\"el},
hal = {https://hal.inria.fr/hal-02092970},
booktitle = {Symposium on Computer Arithmetic},
address = {Kyoto, Japan},
pages = {183--186},
year = 2019,
month = jun
}
@inproceedings{garchery20jfla,
topics = {team},
title = {Des transformations logiques passent leur certicat},
author = {Garchery, Quentin and Keller, Chantal and March{\'e}, Claude and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-02384946},
crossref = {jfla20}
}
@inproceedings{conchon19icfem,
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-02420588},
author = {Sylvain Conchon and Mattias Roux},
title = {Reasoning About Universal Cubes in {MCMT}},
booktitle = {International Conference on Formal Engineering Methods},
pages = {270--285},
editor = {Yamine A{\"{\i}}t Ameur and Shengchao Qin},
series = {Lecture Notes in Computer Science},
volume = 11852,
publisher = {Springer},
year = 2019
}
@inproceedings{conchon18ijcar,
topics = {team},
hal = {https://hal.inria.fr/hal-02420590},
author = {Sylvain Conchon and David Declerck and Fatiha Za{\"{\i}}di},
title = {Cubicle-W : Parameterized Model Checking on Weak Memory},
booktitle = {International Joint Conference on Automated Reasoning},
pages = {152--160},
editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
series = {Lecture Notes in Computer Science},
volume = 10900,
publisher = {Springer},
year = 2018
}
@inproceedings{conchon18netsy,
topics = {team},
hal = {https://hal.inria.fr/hal-02001652},
author = {Sylvain Conchon and
Giorgio Delzanno and
Angelo Ferrando},
title = {Declarative Parameterized Verification of Topology-Sensitive Distributed
Protocols},
pages = {209--224},
year = 2018,
editor = {Andreas Podelski and
Fran{\c{c}}ois Ta{\"{\i}}ani},
booktitle = {Networked Systems, 6th International Conference, Revised Selected Papers},
series = {Lecture Notes in Computer Science}
}
@inproceedings{paskevich20isola,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Abstraction and Genericity in {Why3}},
booktitle = {9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},
month = oct,
year = 2020,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 12476,
pages = {122--142},
editor = {Tiziana Margaria and Bernhard Steffen},
address = {Rhodes, Greece},
topics = {team},
note = {See also \url{https://usr.lmf.cnrs.fr/~jcf/isola-2020/}},
hal = {https://hal.inria.fr/hal-02696246}
}
@inproceedings{filliatre20coqworkshop,
author = {Jean-Christophe Filli\^atre},
title = {A {Coq} retrospective - at the heart of {Coq} architecture, the genesis of version 7.0},
booktitle = {The Coq Workshop 2020},
year = 2020,
month = {July},
address = {virtual},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes},
hal = {https://hal.inria.fr/hal-02890460},
url = {https://www.youtube.com/watch?v=tROOcO44Uho#t=64.5m}
}
@inproceedings{becker20tacas,
topics = {team},
title = {Analysing installation scenarios of {Debian} packages},
author = {Becker, Benedikt and Jeannerod, Nicolas and March{\'e}, Claude and R{\'e}gis-Gianas, Yann and Sighireanu, Mihaela and Treinen, Ralf},
hal = {https://hal.archives-ouvertes.fr/hal-02355602},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
series = {Lecture Notes in Computer Science},
volume = 12079,
pages = {235--253},
year = 2020,
doi = {10.1007/978-3-030-45237-7_14}
}
@inproceedings{diverio20vtltc,
topics = {team},
title = {``{You-Know-Why}'': an Early-Stage Prototype of a Key Server Developed using {Why3}},
author = {Diverio, Diego and Belo Louren\c{c}o, Cl{\'a}udio and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03002187},
booktitle = {VerifyThis Long-term Challenge 2020: Proceedings of the Online-Event},
address = {Dublin, Ireland},
publisher = {Karlsruhe Institute of Technology},
pages = {4--7},
year = 2020,
month = apr,
doi = {10.5445/IR/1000119426}
}
@inproceedings{faissole19afadl,
topics = {team},
title = {{Formalisation en Coq des erreurs d'arrondi de m{\'e}thodes de Runge-Kutta pour les syst{\`e}mes matriciels}},
author = {Faissole, Florian},
hal = {https://hal.archives-ouvertes.fr/hal-02391924},
booktitle = {AFADL 2019 - 18e journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels},
address = {Toulouse, France},
year = 2019,
month = jun
}
@inproceedings{steinberg19itp,
topics = {team},
title = {{Quantitative continuity and Computable Analysis in Coq}},
author = {Steinberg, Florian and Thies, Holger and Th{\'e}ry, Laurent},
hal = {https://hal.archives-ouvertes.fr/hal-02426470},
note = {The version accepted to the conference can be accessed at https://drops.dagstuhl.de/opus/volltexte/2019/11083/},
booktitle = {{ITP 2019 - Tenth International Conference on Interactive Theorem Proving}},
address = {Portland, United States},
year = 2019,
month = sep,
doi = {10.4230/LIPIcs.ITP.2019.28},
keywords = {Computable analysis ; Coq ; Contionuous functionals ; Discontinuity ; Closed choice on the natura},
hal_id = {hal-02426470},
hal_version = {v1}
}
@inproceedings{belo19formalise,
topics = {team},
title = {{A Generalized Program Verification Workflow Based on Loop Elimination and SA Form}},
author = {Belo Louren\c{c}o, Cl{\'a}udio and Frade, Maria Jo{\~a}o and Sousa Pinto, Jorge},
hal = {https://hal.inria.fr/hal-02431769},
booktitle = {{FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering}},
address = {Montreal, Canada},
year = 2019,
month = may,
pdf = {https://hal.inria.fr/hal-02431769/file/main.pdf},
hal_id = {hal-02431769},
hal_version = {v1}
}
@inproceedings{hilaire19arith,
topics = {team},
title = {{Optimal Word-Length Allocation for the Fixed-Point Implementation of Linear Filters and Controllers}},
author = {Hilaire, Thibault and Ouzia, Hac{\`e}ne and Lopez, Benoit},
hal = {https://hal.sorbonne-universite.fr/hal-02393851},
booktitle = {{ARITH 2019 - IEEE 26th Symposium on Computer Arithmetic}},
address = {Kyoto, Japan},
publisher = {IEEE},
pages = {175-182},
year = 2019,
month = jun,
doi = {10.1109/ARITH.2019.00040},
keywords = {fixed-point arithmetic ; word-length allocation},
pdf = {https://hal.sorbonne-universite.fr/hal-02393851/file/arith.pdf},
hal_id = {hal-02393851},
hal_version = {v1}
}
@inproceedings{becker21fide,
topics = {team},
title = {Explaining Counterexamples with Giant-Step Assertion Checking},
author = {Becker, Benedikt and Belo Louren\c{c}o, Cl{\'a}udio and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03217393},
booktitle = {6th Workshop on Formal Integrated Development Environments (F-IDE 2021)},
editor = {Creissac Campos, Jos{\'e} and Paskevich, Andrei},
series = {Electronic Proceedings in Theoretical Computer Science},
doi = {10.4204/EPTCS.338.10},
year = 2021,
month = may
}
@inproceedings{melquiond20issac,
topics = {team},
title = {{WhyMP}, a Formally Verified Arbitrary-Precision Integer Library},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-02566654},
booktitle = {45th International Symposium on Symbolic and Algebraic Computation (ISSAC)},
pages = {352--359},
year = 2020,
doi = {10.1145/3373207.3404029},
keywords = {Integer arithmetic ; Deductive program verification ; Mathematical library}
}
@inproceedings{boldo20arith,
topics = {team},
title = {A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm},
author = {Boldo, Sylvie and Gallois-Wong, Diane and Hilaire, Thibault},
hal = {https://hal.inria.fr/hal-02982017},
booktitle = {27th IEEE Symposium on Computer Arithmetic (ARITH)},
publisher = {IEEE},
pages = {9--16},
year = 2020,
doi = {10.1109/ARITH48897.2020.00011},
keywords = {Dot Product ; Sum-of-Products ; Correct Round- ing ; Odd Rounding ; Fixed-Point Arithmetic}
}
@inproceedings{lecomte20erts,
topics = {team},
title = {Low Cost High Integrity Platform},
author = {Lecomte, Thierry and D{\'e}harbe, David and Sabatier, Denis and Prun, Etienne and P{\'e}ronne, Patrick and Chailloux, Emmanuel and Varoumas, Steven and Susungi, Adilla and Conchon, Sylvain},
hal = {https://hal.archives-ouvertes.fr/hal-02446132},
booktitle = {10th European Congress on Embedded Real Time Systems (ERTS)},
address = {Toulouse, France},
year = 2020,
keywords = {Safety ; Certification ; Formal methods}
}
@inproceedings{jaloyan20icfem,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03094566},
booktitle = {Formal Methods and Software Engineering (ICFEM)},
pages = {55--72},
year = 2020,
doi = {10.1007/978-3-030-63406-3\_4}
}
@inproceedings{filliatrepascutto21,
author = {Jean-Christophe Filli\^atre and Cl\'ement Pascutto},
title = {{Ortac}: Runtime Assertion Checking for {OCaml}},
year = 2021,
topics = {team},
booktitle = {Proceedings of the 21st International Conference on Runtime Verification (RV'21)},
month = may,
hal = {https://hal.inria.fr/hal-03252901},
abstract = {Runtime assertion checking (RAC) is a convenient set of
techniques that lets developers abstract away the
process of verifying the correctness of their
programs by writing formal specifications and
automating their verification at runtime. In this
work, we present ortac, a runtime assertion checking
tool for OCaml libraries and programs. OCaml is a
functional programming lan- guage in which idioms
rely on an expressive type system, modules, and
interface abstractions. ortac consumes interfaces
annotated with type invariants and function
contracts and produces code wrappers with the same
signature that check these specifications at
runtime. It provides a flexible framework for
traditional assertion checking, monitoring mis-
behaviors without interruptions, and automated fuzz
testing for OCaml programs. This paper presents an
overview of ortac features and highlights its main
design choices.}
}
@inproceedings{belo21fmics,
topics = {team},
title = {Automated Verification of Temporal Properties of {Ladder} Programs},
author = {Belo Louren{\c c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03281580},
booktitle = {Formal Methods for Industrial Critical Systems},
doi = {10.1007/978-3-030-85248-1_2},
series = {Lecture Notes in Computer Science},
volume = 12863,
pages = {21--38},
year = 2021
}
@inproceedings{osborne21ocaml,
topics = {team},
title = {Leveraging Formal Specifications to Generate Fuzzing Suites},
author = {Osborne, Nicolas and Pascutto, Cl{\'e}ment},
hal = {https://hal.inria.fr/hal-03328646},
booktitle = {OCaml Users and Developers Workshop, co-located with the 26th ACM SIGPLAN International Conference on Functional Programming},
year = 2021
}
@inproceedings{garchery21pxtp,
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-03349223},
title = {A Framework for Proof-carrying Logical Transformations},
author = {Garchery, Quentin},
booktitle = {Proof eXchange for Theorem Proving},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = 336,
pages = {5--23},
year = 2021,
month = jul,
doi = {10.4204/EPTCS.336.2}
}
@inproceedings{filliatre21rv,
topics = {team},
title = {{Ortac}: Runtime Assertion Checking for {OCaml}},
author = {Filli{\^a}tre, Jean-Christophe and Pascutto, Cl{\'e}ment},
hal = {https://hal.inria.fr/hal-03252901},
booktitle = {21st International Conference on Runtime Verification},
year = 2021
}
@inproceedings{filliatre22rv,
topics = {team},
title = {Optimizing Prestate Copies in Runtime Verification of Function Postconditions},
author = {Filli{\^a}tre, Jean-Christophe and Pascutto, Cl{\'e}ment},
hal = {https://hal.inria.fr/hal-03690675v1},
booktitle = {22nd International Conference on Runtime Verification},
year = 2022
}
@inproceedings{weens21nsv,
topics = {team},
title = {Modeling round-off errors in hydrodynamic simulations},
author = {Weens, William and Vazquez-Gonzalez, Thibaud and Ben Salem-Knapp, Louise},
hal = {https://hal.inria.fr/hal-03351754},
booktitle = {14th International Workshop on Numerical Software Verification},
year = 2021
}
@inproceedings{balabonski21fscd,
topics = {team},
title = {A strong call-by-need calculus},
author = {Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-03149692},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction},
editor = {Naoki Kobayashi},
volume = 195,
pages = {9:1--9:22},
year = 2021,
doi = {10.4230/LIPIcs.FSCD.2021.9}
}
@inproceedings{boldo21arith,
topics = {team},
title = {Some Formal Tools for Computer Arithmetic: {Flocq} and {Gappa}},
author = {Boldo, Sylvie and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-03233227},
booktitle = {28th IEEE International Symposium on Computer Arithmetic},
editor = {Mioara Joldes and Fabrizio Lamberti},
year = 2021
}
@inproceedings{bensalemknapp21afadl,
topics = {team},
title = {La double pr{\'e}cision suffit-elle {\`a} l'exascale ?},
author = {Ben Salem-Knapp, Louise and Vazquez-Gonzalez, Thibaud and Weens, William},
hal = {https://hal.inria.fr/hal-03351615},
booktitle = {20{\`e}mes journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels},
year = 2021
}
@inproceedings{melquiond21fide,
topics = {team},
title = {Plotting in a Formally Verified Way},
author = {Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-03168208},
booktitle = {6th Workshop on Formal Integrated Development Environment},
volume = 338,
pages = {39--45},
year = 2021,
doi = {10.4204/EPTCS.338.6}
}
@inproceedings{denis22icfem,
topics = {team},
title = {{Creusot}: a Foundry for the Deductive Verication of {Rust} Programs},
author = {Denis, Xavier and Jourdan, Jacques-Henri and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-03737878},
booktitle = {International Conference on Formal Engineering Methods - ICFEM},
address = {Madrid, Spain},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
year = 2022,
keywords = {Rust programming language ; Deductive program verification ; Aliasing and Ownership ; Prophecies ; Traits}
}
@inproceedings{matsushita22pldi,
topics = {team},
title = {{RustHornBelt}: a semantic foundation for functional verification of {Rust} programs with unsafe code},
author = {Matsushita, Yusuke and Denis, Xavier and Jourdan, Jacques-Henri and Dreyer, Derek},
hal = {https://hal.inria.fr/hal-03777103},
booktitle = {International Conference on Programming Language Design and Implementation},
publisher = {ACM},
pages = {841--856},
year = 2022,
doi = {10.1145/3519939.3523704}
}
@inproceedings{vanstrydonck22csf,
topics = {team},
title = {Proving full-system security properties under multiple attacker models on capability machines},
author = {Van Strydonck, Thomas and Georges, A{\"i}na Linn and Gu{\'e}neau, Arma{\"e}l and Trieu, Alix and Timany, Amin and Piessens, Frank and Birkedal, Lars and Devriese, Dominique},
hal = {https://hal.inria.fr/hal-03826851},
booktitle = {CSF 2022 - 35th IEEE Computer Security Foundations Symposium},
year = 2022
}
@inproceedings{boldo23fm,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Induction Principle and {Tonelli's} Theorem},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Martin, Vincent and Mayero, Micaela and Mouhcine, Houda},
hal = {https://hal.inria.fr/hal-03889276},
booktitle = {25th International Symposium on Formal Methods (FM 2023)},
series = {Lecture Notes in Computer Science},
volume = 14000,
pages = {39--55},
year = 2023,
doi = {10.1007/978-3-031-27481-7\_4}
}
@inproceedings{filliatre23jfla,
topics = {team},
title = {L'arithm{\'e}tique de s{\'e}paration},
author = {Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03886759},
booktitle = {JFLA 2023 - 34{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Timothy Bourke and Delphine Demange},
pages = {274--283},
year = 2023
}
@inproceedings{andres22jfla,
topics = {team},
title = {Connecter l'{\'e}cosyst{\`e}me {OCaml} {\`a} {Software} {Heritage} via opam},
author = {Andr{\`e}s, L{\'e}o and Boujbel, Raja and Gesbert, Louis and Pinto, Dario},
hal = {https://hal.inria.fr/hal-03626845},
booktitle = {33{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Chantal Keller and Timothy Bourke},
pages = {227--234},
year = 2022
}
@inproceedings{bozman22jfla,
topics = {team},
title = {Jouez {\`a} Faire Consensus Avec {MITTEN} (d{\'e}monstration)},
author = {Bozman, {\c C}agdas and Iguernlala, Mohamed and Laporte, Michael and Levillain, Maxime and Mebsout, Alain and Conchon, Sylvain},
hal = {https://hal.inria.fr/hal-03626847},
booktitle = {33{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs},
editor = {Chantal Keller and Timothy Bourke},
pages = {248--250},
year = 2022
}
@inproceedings{geneau23arith,
topics = {team},
author = {Geneau de Lamarli{\`e}re, Paul and Melquiond, Guillaume and Faissole, Florian},
title = {Slimmer Formal Proofs for Mathematical Libraries},
hal = {https://inria.hal.science/hal-04165169},
booktitle = {Int. Conf. on Computer Arithmetic},
year = 2023
}
@inproceedings{conchon21iccl,
topics = {team},
author = {Sylvain Conchon and Giorgio Delzanno and Arnaud Sangnier},
editor = {Stefania Monica and Federico Bergenti},
title = {Verification of Contact Tracing Protocols via SMT-based Model Checking
and Counting Abstraction},
booktitle = {Proceedings of the 36th Italian Conference on Computational Logic,
Parma, Italy, September 7-9, 2021},
series = {{CEUR} Workshop Proceedings},
volume = 3002,
pages = {77--91},
publisher = {CEUR-WS.org},
year = 2021,
url = {https://ceur-ws.org/Vol-3002/paper24.pdf}
}
@inproceedings{conchon21fmbc,
topics = {team},
author = {Sylvain Conchon and Alexandrina Korneva and {\c{C}}agdas Bozman and
Mohamed Iguernlala and Alain Mebsout},
editor = {Bruno Bernardo and Diego Marmsoler},
title = {Formally Documenting Tenderbake (Short Paper)},
booktitle = {3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV
2021, July 18-19, 2021, Los Angeles, California, {USA} (Virtual Conference)},
series = {OASIcs},
volume = 95,
pages = {4:1--4:9},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = 2021,
doi = {10.4230/OASICS.FMBC.2021.4}
}
@inproceedings{conchon22fab,
topics = {team},
author = {Sylvain Conchon},
editor = {Sara Tucci Piergiovanni and Natacha Crooks},
title = {Some Insights on Open Problems in Blockchains: Explorative Tracks
for Tezos (Invited Talk)},
booktitle = {5th International Symposium on Foundations and Applications of Blockchain
2022, {FAB} 2022, June 3, 2022, Berkeley, CA, {USA}},
series = {OASIcs},
volume = 101,
pages = {2:1--2:1},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = 2022,
doi = {10.4230/OASICS.FAB.2022.2}
}
@inproceedings{conchon23sefm,
topics = {team},
hal = {https://inria.hal.science/hal-04394062},
author = {Sylvain Conchon and Alexandrina Korneva},
editor = {Carla Ferreira and Tim A. C. Willemse},
title = {The Cubicle Fuzzy Loop: {A} Fuzzing-Based Extension for the {Cubicle}
Model Checker},
booktitle = {Software Engineering and Formal Method},
series = {Lecture Notes in Computer Science},
volume = 14323,
pages = {30--46},
publisher = {Springer},
year = 2023,
doi = {10.1007/978-3-031-47115-5\_3}
}
@inproceedings{marche24jfla,
topics = {team},
author = {March{\'e}, Claude and Cousineau, Denis},
hal = {https://inria.hal.science/hal-04342273},
year = 2024,
title = {De l'avantage de nuancer les d{\'e}cisions binaires},
booktitle = {35es Journ{\'e}es Francophones des Langages Applicatifs}
}
@inproceedings{timany24popl,
topics = {team},
title = {The Logical Essence of Well-Bracketed Control Flow},
author = {Timany, Amin and Gu{\'e}neau, Arma{\"e}l and Birkedal, Lars},
hal = {https://hal.science/hal-04271457},
booktitle = {POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages},
organization = {SIGPLAN},
publisher = {ACM},
year = 2024
}
@inproceedings{pottier24popl,
topics = {team},
title = {Thunks and Debits in Separation Logic with Time Credits},
author = {Pottier, Fran{\c c}ois and Gu{\'e}neau, Arma{\"e}l and Jourdan, Jacques-Henri and M{\'e}vel, Glen},
hal = {https://hal.science/hal-04238691},
booktitle = {POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages},
organization = {SIGPLAN},
publisher = {ACM},
volume = 8,
year = 2024
}
@inproceedings{bonnot24fmcad,
topics = {team},
title = {Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function},
author = {Bonnot, Paul and Boyer, Beno{\^i}t and Faissole, Florian and March{\'e}, Claude and Rieu-Helft, Rapha{\"e}l},
hal = {https://inria.hal.science/hal-04674600},
booktitle = {Formal Methods in Computer-Aided Design},
publisher = {IEEE},
year = 2024
}
@inproceedings{andres23ifl,
topics = {team},
title = {{Wasocaml}: compiling {OCaml} to {WebAssembly}},
author = {Andr{\`e}s, L{\'e}o and Chambart, Pierre and Filli{\^a}tre, Jean-Christophe},
hal = {https://inria.hal.science/hal-04311345},
booktitle = {35th Symposium on Implementation and Application of Functional Languages},
editor = {Jo{\~a}o Saraiva and Jo{\~a}o Fernandes},
year = 2023
}
@inproceedings{filliatre24bigspec,
author = {Jean-Christophe Filli\^atre},
title = {Proofs on Inductive Predicates in Why3},
booktitle = {Big Specification: Specification, Proof, and Testing at Scale},
year = 2024,
month = {October},
address = {Cambridge, UK},
note = {Invited talk},
topics = {team, lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {invitation},
x-invited-conference = {yes},
x-international-audience = {yes},
hal = {https://hal.science/hal-04734466}
}
@inproceedings{gueneau23oopsla,
topics = {team},
title = {{Melocoton}: A Program Logic for Verified Interoperability Between {OCaml} and {C}},
author = {Gu{\'e}neau, Arma{\"e}l and Hostert, Johannes and Spies, Simon and Sammler, Michael and Birkedal, Lars and Dreyer, Derek},
hal = {https://inria.hal.science/hal-04203298},
booktitle = {Object-Oriented Programming, Systems, Languages \& Applications},
publisher = {ACM},
year = 2023,
doi = {10.1145/3622823}
}
@inproceedings{denis23tacas,
topics = {team},
title = {Specifying and Verifying Higher-order Rust Iterators},
author = {Denis, Xavier and Jourdan, Jacques-Henri},
hal = {https://hal.science/hal-03827702},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
editor = {Sriram Sankaranarayanan and Natasha Sharygina},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 13994,
pages = {93--110},
year = 2023,
doi = {10.1007/978-3-031-30820-8\_9}
}
@inproceedings{mahboubi23types,
topics = {team},
title = {Manifest Termination},
author = {Mahboubi, Assia and Melquiond, Guillaume},
hal = {https://inria.hal.science/hal-04172297},
booktitle = {29th International Conference on Types for Proofs and Programs},
address = {Valencia, Spain},
pages = {1--3},
year = 2023
}
@inproceedings{melquiond24coq,
topics = {team},
title = {Turning the {Coq} Proof Assistant into a Pocket Calculator},
author = {Melquiond, Guillaume},
hal = {https://inria.hal.science/hal-04702129},
booktitle = {Coq 2024 - 15th Coq Workshop},
address = {Tbilisi, Georgia},
year = 2024
}
@inproceedings{faissole24itp,
topics = {team},
title = {End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation},
author = {Faissole, Florian and Geneau de Lamarli{\`e}re, Paul and Melquiond, Guillaume},
hal = {https://hal.science/hal-04515714},
booktitle = {5th International Conference on Interactive Theorem
Proving},
publisher = {Leibniz International Proceedings in Informatics},
address = {Tbilisi, Georgia},
volume = 309,
pages = {14:1-14:18},
year = 2024,
doi = {10.4230/LIPIcs.ITP.2024.14}
}
@inproceedings{melquiond24icfp,
topics = {team},
title = {A Safe Low-level Language for Computer Algebra and its Formally Verified Compiler},
author = {Melquiond, Guillaume and Moreau, Josu{\'e}},
hal = {https://inria.hal.science/hal-04485670},
booktitle = {29th ACM SIGPLAN International Conference on Functional Programming},
address = {Milan, Italy},
volume = 8,
number = {ICFP},
pages = {121--146},
year = 2024
}
@inproceedings{boldo24thedu,
topics = {team},
title = {Teaching Divisibility and Binomials with {Coq}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Hamelin, David and Mayero, Micaela and Rousselin, Pierre},
hal = {https://hal.science/hal-04725586},
booktitle = {13th International Workshop on Theorem proving components for Educational software},
address = {Nancy, France},
year = 2024
}
@inproceedings{saudubray25jfla,
topics = {team},
title = {Faire chauffer {Why3} avec de l'induction},
author = {Saudubray, Henri and Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei},
hal = {https://inria.hal.science/hal-04859412},
booktitle = {36es Journ{\'e}es Francophones des Langages Applicatifs},
address = {Roiff{\'e}, France},
year = 2025
}
@inproceedings{geneau25jfla,
topics = {team},
title = {V{\'e}rification de bout en bout d'une fonction de biblioth{\`e}que math{\'e}matique},
author = {Geneau de Lamarli{\`e}re, Paul},
hal = {https://inria.hal.science/hal-04859533},
booktitle = {36es Journ{\'e}es Francophones des Langages Applicatifs},
address = {Roiff{\'e}, France},
year = 2025
}
@inproceedings{patault25jfla,
topics = {team},
title = {Remonter les barri{\`e}res pour ouvrir une cl{\^o}ture},
author = {Patault, Paul and Golfouse, Arnaud and Denis, Xavier},
hal = {https://inria.hal.science/hal-04859517},
booktitle = {36es Journ{\'e}es Francophones des Langages Applicatifs},
address = {Roiff{\'e}, France},
year = 2025
}
@inproceedings{moreau25jfla,
topics = {team},
title = {Des briques de calcul formel plus solides avec {Capla}},
author = {Moreau, Josu{\'e}},
hal = {https://inria.hal.science/hal-04859452},
booktitle = {36es Journ{\'e}es Francophones des Langages Applicatifs},
address = {Roiff{\'e}, France},
year = 2025
}
@inproceedings{paskevich25esop,
topics = {team},
title = {{Coma, an Intermediate Verification Language with Explicit Abstraction Barriers}},
author = {Paskevich, Andrei and Patault, Paul and Filli{\^a}tre, Jean-Christophe},
url = {https://hal.science/hal-04839768},
booktitle = {Accepted for ESOP'25},
year = 2025,
pdf = {https://hal.science/hal-04839768v1/file/main.pdf},
hal_id = {hal-04839768},
hal_version = {v1}
}
@inproceedings{mevel21formal,
topics = {team},
author = {Glen Mével and Jacques-Henri Jourdan},
title = {Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model},
month = {September},
year = {2021},
booktitle = {International Conference on Functional Programming (ICFP)},
organization = {ACM},
doi = {10.1145/3473571}
}
@inproceedings{mevel20cosmo,
topics = {team},
author = {Glen Mével and Jacques-Henri Jourdan and François
Pottier},
title = {Cosmo: A Concurrent Separation Logic for {Multicore
OCaml}},
year = {2020},
booktitle = {International Conference on Functional Programming (ICFP)},
organization = {ACM},
doi = {10.1145/3408978}
}
@inproceedings{dang2020rustbelt,
topics = {team},
author = {Dang, Hoang-Hai and Jourdan, Jacques-Henri and Kaiser, Jan-Oliver and Dreyer Derek},
title = {{RustBelt} Meets Relaxed Memory},
booktitle = {Symposium on Principles of Programming Languages (POPL)},
year = {2020},
organization = {ACM},
doi = {10.1145/3371102}
}
@proceedings{afm07,
title = {{Proceedings of the second workshop on Automated formal methods}},
booktitle = {{Proceedings of the second workshop on Automated formal methods}},
year = 2007,
editor = {John Rushby and N. Shankar},
publisher = {ACM Press},
isbn = {978-1-59593-879-4}
}
@proceedings{cade05,
title = {20th International Conference on Automated Deduction},
booktitle = {20th International Conference on Automated Deduction (CADE-20)},
address = {Tallinn, Estonia},
month = jul,
year = 2005,
editor = {Robert Nieuwenhuis},
series = {Lecture Notes in Artificial Intelligence},
volume = 3632,
publisher = {Springer},
isbn = {3-540-28005-7}
}
@proceedings{icde11,
title = {Proceedings of the Twenty Seventh International Conference on
Data Engineering},
booktitle = {Proceedings of the Twenty Seventh International Conference on
Data Engineering},
editor = {Serge Abiteboul and Christoph Koch and Tan Kian Lee},
year = 2011,
month = apr,
publisher = {{IEEE} Comp. Soc. Press}
}
@proceedings{popl13,
title = {Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = 2013,
booktitle = {Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
editor = {R. Cousot},
address = {Roma, Italy},
month = jan,
publisher = {ACM Press}
}
@proceedings{popl2014,
title = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = 2014,
booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
address = {San Diego, USA},
month = jan,
publisher = {ACM Press}
}
@proceedings{popl2015,
title = {Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = 2015,
booktitle = {Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
address = {Mumbai, India},
month = jan,
publisher = {ACM Press}
}
@proceedings{rta04,
title = {15th International Conference on Rewriting Techniques and Applications},
booktitle = {15th International Conference on Rewriting Techniques and Applications},
editor = {Vincent van Oostrom},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 3091,
month = jun,
year = 2004,
address = {Aachen, Germany},
isbn = {3-540-22153-0}
}
@proceedings{rta11,
booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA 11)},
series = {Leibniz International Proceedings in Informatics},
year = {2011},
volume = {10},
editor = {Manfred Schmidt-Schau{\ss}},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Novi Sad, Serbia},
isbn = {978-3-939897-30-9},
issn = {1868-8969}
}
@proceedings{rta12,
title = {23rd International Conference on Rewriting Techniques and Applications},
booktitle = {23nd International Conference on Rewriting Techniques and Applications},
series = {Leibniz International Proceedings in Informatics},
year = {2012},
volume = {15},
editor = {Ashish Tiwari},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Nagoya, Japan},
isbn = {978-3-939897-38-5}
}
@proceedings{ijcar06,
title = {International Joint Conference on Automated Reasoning},
booktitle = {Third International Joint Conference on Automated Reasoning},
editor = {Ulrich Furbach and Natarajan Shankar},
year = 2006,
series = {Lecture Notes in Computer Science},
volume = 4130,
address = {Seattle, USA},
month = aug,
publisher = {Springer}
}
@proceedings{ijcar10,
title = {International Joint Conference on Automated Reasoning},
booktitle = {Fifth International Joint Conference on Automated Reasoning},
year = 2010,
editor = {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
address = {Edinburgh, Scotland},
month = jul,
series = {Lecture Notes in Artificial Intelligence},
volume = {6173},
publisher = {Springer}
}
@proceedings{tacas2011,
title = {Tools and Algorithms for the Construction and Analysis of Systems},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
year = 2011,
month = apr,
editor = {Parosh A. Abdulla and K. Rustan M. Leino},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6605},
isbn = {978-3-642-19834-2},
address = {Saarbr{\"u}cken, Germany}
}
@proceedings{tphols2005,
title = {Theorem Proving in Higher Order Logics:
18th International Conference, TPHOLs 2005},
booktitle = {18th International Conference on Theorem Proving in Higher Order Logics},
editor = {J. Hurd and T. Melham},
series = {Lecture Notes in Computer Science},
year = 2005,
volume = 3603,
addresse = {Oxford, UK},
month = aug,
publisher = {Springer}
}
@proceedings{tphols2008,
title = {Theorem Proving in Higher Order Logics:
21th International Conference, TPHOLs 2008},
booktitle = {21th International Conference on Theorem Proving in Higher Order Logics},
editor = {Otmame A{\"i}t-Mohamed and C\'esar Mu{\~n}oz and Sofi\`ene Tahar},
series = {Lecture Notes in Computer Science},
volume = 5170,
year = 2008,
addresse = {Montr\'eal, Canada},
month = aug,
publisher = {Springer}
}
@proceedings{types03,
editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
title = {3rd International Workshop on Types for Proofs and Programs},
booktitle = {3rd International Workshop on Types for Proofs and Programs},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 3085,
year = 2004,
isbn = {3-540-22164-6},
month = apr,
address = {Torino, Italy}
}
@proceedings{types06,
editor = {Thorsten Altenkirch and Conor Mc Bride},
title = {Types for Proofs and Programs, International Workshop, TYPES
2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
booktitle = {Types for Proofs and Programs, International Workshop, TYPES
2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4502},
year = {2007},
isbn = {978-3-540-74463-4}
}
@proceedings{wst06,
booktitle = {{Extended Abstracts of the 8th International Workshop on Termination, WST'06}},
title = {{Extended Abstracts of the 8th International Workshop on Termination, WST'06}},
year = {2006},
editor = {Alfons Geser and Harald Sondergaard},
month = aug
}
@proceedings{wst07,
booktitle = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
title = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
year = {2007},
editor = {Dieter Hofbauer and Alexander Serebrenik},
month = jun
}
@proceedings{amast04,
title = {Algebraic Methodology and Software Technology},
booktitle = {Algebraic Methodology and Software Technology},
year = 2004,
series = {Lecture Notes in Computer Science},
volume = 3116,
address = {Stirling, UK},
month = jul,
publisher = {Springer}
}
@proceedings{pepm04,
title = {Partial Evaluation and Program Manipulation},
year = 2004,
booktitle = {ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation},
address = {Verona, Italy},
month = aug,
publisher = {ACM Press}
}
@proceedings{pepm10,
title = {Partial Evaluation and Program Manipulation},
year = 2010,
booktitle = {ACM SIGPLAN 2010 Symposium on Partial Evaluation and Program Manipulation},
editor = {John P. Gallagher and Janis Voigtl{\"a}nder},
address = {Madrid, Spain},
month = jan,
publisher = {ACM Press},
isbn = {978-1-60558-727-1}
}
@proceedings{icfem04,
title = {Formal Engineering Methods},
year = 2004,
booktitle = {6th International Conference on Formal Engineering Methods},
series = {Lecture Notes in Computer Science},
volume = 3308,
editor = {Jim Davies and Wolfram Schulte and Mike Barnett},
address = {Seattle, WA, USA},
month = nov,
publisher = {Springer}
}
@proceedings{date10,
title = {Design, Automation \& Test in {E}urope},
year = 2010,
booktitle = {Design, Automation \& Test in {E}urope},
address = {Dresden. Germany},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
month = mar,
publisher = {IEEE}
}
@proceedings{cav07,
editor = {Werner Damm and Holger Hermanns},
title = {Computer Aided Verification},
booktitle = {19th International Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4590,
address = {Berlin, Germany},
month = jul,
year = {2007}
}
@proceedings{cav2014,
editor = {Armin Biere and Roderick Bloem},
title = {Computer Aided Verification},
booktitle = {26th International Conference on Computer Aided Verification},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8859,
address = {Vienna, Austria},
month = jul,
year = 2014
}
@proceedings{jfla05,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2005,
booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = mar,
publisher = {INRIA}
}
@proceedings{jfla06,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2006,
booktitle = {Dix-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla07,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2007,
booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla08,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2008,
booktitle = {Dix-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
publisher = {INRIA}
}
@proceedings{jfla09,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2009,
booktitle = {Vingti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Saint-Quentin sur Is\`ere},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla10,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2010,
booktitle = {Vingt-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Vieux-Port La Ciotat, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla11,
title = {Journ\'ees Francophones des Langages Applicatifs},
editor = {Sylvain Conchon},
year = 2011,
booktitle = {Vingt-deuxi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {La Bresse, France},
publisher = {INRIA},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{jfla12,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2012,
booktitle = {Vingt-troisi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = feb,
address = {Carnac, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-cle-support = {JFLA}
}
@proceedings{jfla13,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2013,
booktitle = {Vingt-quatri\`emes Journ\'ees Francophones des Langages Applicatifs},
month = feb,
address = {Aussois, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla14,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2014,
booktitle = {Vingt-cinqui\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Fr\'ejus, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla15,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2015,
booktitle = {Vingt-sixi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Val d'Ajol, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla16,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2016,
booktitle = {Vingt-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Saint-Malo, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla17,
topics = {team},
hal = {https://hal.inria.fr/hal-01662072},
title = {Journ\'ees Francophones des Langages Applicatifs},
editor = {Boldo, Sylvie and Signoles, Julien},
year = 2017,
booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
month = jan,
address = {Gourette, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {JFLA}
}
@proceedings{jfla18,
topics = {team},
title = {Vingt-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Banyuls-sur-mer, France},
year = 2018,
month = jan,
editor = {Boldo, Sylvie and Magaud, Nicolas},
hal = {https://hal.inria.fr/hal-01707376}
}
@proceedings{jfla19,
title = {Trenti\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trenti\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Les Rousses, France},
year = 2019,
month = jan,
editor = {Magaud, Nicolas and Dargaye, Zaynah},
hal = {https://hal.archives-ouvertes.fr/hal-01985195v1}
}
@proceedings{jfla20,
title = {Trente-et-uni\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trente-et-uni\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Gruissan, France},
year = 2020,
month = jan,
editor = {Dargaye, Zaynah and R\'egis-Gianas, Yann}
}
@proceedings{sefm05,
title = {Software Engineering and Formal Methods},
year = 2005,
booktitle = {3rd IEEE International Conference on Software Engineering
and Formal Methods (SEFM'05)},
address = {Koblenz, Germany},
editor = {Bernhard K. Aichernig and Bernhard Beckert},
publisher = {{IEEE} Comp. Soc. Press},
month = sep
}
@proceedings{sefm06,
title = {Software Engineering and Formal Methods},
year = 2006,
editor = {Dang Van Hung and Paritosh Pandya},
booktitle = {4th IEEE International Conference on Software Engineering
and Formal Methods (SEFM'06)},
address = {Pune, India},
publisher = {{IEEE} Comp. Soc. Press},
month = sep
}
@proceedings{rta07,
editor = {Franz Baader},
title = {Term Rewriting and Applications},
booktitle = {18th International Conference on Rewriting Techniques and Applications (RTA'07)},
address = {Paris, France},
month = jun,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4533,
year = 2007
}
@proceedings{fm05,
editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
title = {Formal Methods},
booktitle = {International Symposium of Formal Methods Europe (FM'05)},
address = {Newcastle,UK},
month = jul,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3582},
year = 2005
}
@proceedings{mpc2006,
editor = {Tarmo Uustalu},
title = {Mathematics of Program Construction, 8th International Conference,
MPC 2006},
booktitle = {Mathematics of Program Construction, MPC 2006},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
month = jul,
address = {Kuressaare, Estonia},
volume = {4014},
year = {2006}
}
@proceedings{icfp07,
editor = {Ralf Hinze and Norman Ramsey},
title = {Proceedings of the 12th ACM SIGPLAN International Conference
on Functional Programming, ICFP 2007},
booktitle = {12th ACM SIGPLAN International Conference
on Functional Programming, ICFP 2007},
address = {Freiburg, Germany},
publisher = {ACM Press},
year = {2007},
isbn = {978-1-59593-815-2}
}
@proceedings{icfp08,
editor = {James Hook and Peter Thiemann},
title = {Proceeding of the 13th ACM SIGPLAN international conference
on Functional programming, ICFP 2008},
booktitle = {13th ACM SIGPLAN international conference
on Functional programming, ICFP 2008},
address = {Victoria, BC, Canada},
publisher = {ACM},
year = {2008},
month = sep,
isbn = {978-1-59593-919-7}
}
@proceedings{frocos07,
editor = {Boris Konev and Frank Wolter},
title = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
booktitle = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
month = sep,
year = 2007,
address = {Liverpool,UK},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
volume = 4720,
isbn = {978-3-540-74620-1}
}
@proceedings{frocos09,
editor = {Silvio Ghilardi and
Roberto Sebastiani},
title = {Frontiers of Combining Systems, 7th International Symposium,
FroCoS 2009, Proceedings},
booktitle = {Frontiers of Combining Systems, 7th International Symposium, Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5749},
year = {2009},
month = sep,
address = {Trento, Italy},
isbn = {978-3-642-04221-8},
doi = {http://dx.doi.org/10.1007/978-3-642-04222-5},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{frocos11,
editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
title = {Frontiers of Combining Systems, 8th International Symposium,
FroCoS 2011, Proceedings},
booktitle = {Frontiers of Combining Systems, 8th International Symposium, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6989},
year = {2011},
month = oct,
address = {Saarbr\"ucken, Germany},
isbn = {978-3-642-24363-9},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes}
}
@proceedings{vmcai08,
editor = {Francesco Logozzo and Doron Peled and Lenore Zuck},
title = {Verification, Model Checking, and Abstract Interpretation},
booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 4905,
address = {San Francisco, California, USA},
month = jan,
year = {2008}
}
@proceedings{esop08,
title = {17th European Symposium on Programming (ESOP'08)},
booktitle = {17th European Symposium on Programming (ESOP'08)},
year = 2008,
address = {Budapest, Hungary},
month = apr
}
@proceedings{ftfjp08,
title = {Formal Techniques for Java-like Programs},
year = 2008,
booktitle = {Formal Techniques for Java-like Programs (FTfJP'08)},
address = {Paphos, Cyprus},
month = jul
}
@proceedings{esop2014,
title = {23rd European Symposium on Programming (ESOP)},
year = 2014,
booktitle = {ESOP},
editor = {Zhong Shao},
series = {Lecture Notes in Computer Science},
address = {Grenoble},
month = apr,
publisher = {Springer}
}
@proceedings{foveoos10,
editor = {Bernhard Beckert and Claude March\'e},
title = {Formal Verification of Object-Oriented Software, Papers Presented at the International Conference},
booktitle = {Formal Verification of Object-Oriented Software, Papers Presented at the International Conference},
address = {Paris, France},
month = jun,
series = {Karlsruhe Reports in Informatics},
note = {\url{http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083}},
year = 2010,
hal = {http://hal.inria.fr/hal-00772519},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes},
x-pays = {DE}
}
@proceedings{postfoveoos10,
editor = {Bernhard Beckert and Claude March\'e},
title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
publisher = {Springer},
topics = {team},
series = {Lecture Notes in Computer Science},
volume = 6528,
month = jan,
year = 2011,
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-type = {edition},
x-cle-support = {FOVEOOS},
x-pays = {DE}
}
@proceedings{postfoveoos11,
editor = {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov},
title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7421,
year = 2012,
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {actes},
x-cle-support = {FOVEOOS}
}
@proceedings{fast05,
booktitle = {Proceedings of FAST'05},
year = 2005,
editor = {R.~Gorrieri and F.~Martinelli and P.~Ryan and S.~Schneider},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {3866}
}
@proceedings{cpp2011,
title = {International Conference on Certified Programs and Proofs},
year = 2011,
booktitle = {Certified Programs and Proofs},
editor = {Jean-Pierre Jouannaud and Zhong Shao},
series = {Lecture Notes in Computer Science},
month = dec,
publisher = {Springer}
}
@proceedings{vstte12,
booktitle = {Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE)},
month = jan,
year = 2012,
address = {Philadelphia, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Rajeev Joshi and Peter M{\"u}ller and Andreas Podelski},
series = {Lecture Notes in Computer Science},
volume = 7152,
publisher = {Springer}
}
@proceedings{sofsem11,
editor = {Ivana Cern{\'a} and
Tibor Gyim{\'o}thy and
Juraj Hromkovic and
Keith G. Jeffery and
Rastislav Kr{\'a}lovic and
Marko Vukolic and
Stefan Wolf},
booktitle = {37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11)},
address = {Nov{\'y} Smokovec, Slovakia},
title = {SOFSEM 2011: Theory and Practice of Computer Science - 37th
Conference on Current Trends in Theory and Practice of Computer
Science},
publisher = {Springer},
month = jan,
series = {Lecture Notes in Computer Science},
volume = {6543},
year = {2011},
isbn = {978-3-642-18380-5},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes},
x-support = {actes},
x-pays = {SK}
}
@proceedings{smt2012,
booktitle = {SMT workshop},
editor = {Pascal Fontaine and Amit Goel},
publisher = {LORIA},
url = {http://smt2012.loria.fr/},
year = 2012,
x-international-audience = {yes},
x-proceedings = {no},
address = {Manchester, UK}
}
@proceedings{fm2012,
editor = {Dimitra Giannakopoulou and Dominique M{\'e}ry},
title = {FM 2012: Formal Methods - 18th International Symposium},
booktitle = {18th International Symposium on Formal Methods},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {FM},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 7436,
year = 2012,
isbn = {978-3-642-32758-2},
ee = {http://dx.doi.org/10.1007/978-3-642-32759-9}
}
@proceedings{cade13,
title = {24th International Conference on Automated Deduction},
booktitle = {24th International Conference on Automated Deduction (CADE-24)},
address = {Lake Placid, USA},
month = {June},
year = 2013,
series = {Lecture Notes in Artificial Intelligence},
volume = 7898,
publisher = {Springer}
}
@proceedings{vstte13,
booktitle = {Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE)},
month = may,
year = 2013,
address = {Atherton, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Ernie Cohen and Andrey Rybalchenko},
series = {Lecture Notes in Computer Science},
volume = {8164},
publisher = {Springer}
}
@proceedings{vstte14,
booktitle = {6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2014,
address = {Vienna, Austria},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Dimitra Giannakopoulou and Daniel Kroening},
series = {Lecture Notes in Computer Science},
volume = 8471,
publisher = {Springer}
}
@proceedings{vstte15,
booktitle = {7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2015,
address = {San Francisco, California, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Arie Gurfinkel and Sanjit A. Seshia},
series = {Lecture Notes in Computer Science},
volume = 9593,
publisher = {Springer}
}
@proceedings{vstte16,
booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
month = jul,
year = 2016,
address = {Toronto, Canada},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Sandrine Blazy and Marsha Chechik},
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
@proceedings{vstte17,
topics = {team},
hal = {https://hal.inria.fr/hal-01670145},
title = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
booktitle = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
month = dec,
year = 2017,
address = {Heidelberg, Germany},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Andrei Paskevich and Thomas Wies},
series = {Lecture Notes in Computer Science},
number = 10712,
publisher = {Springer}
}
@proceedings{itp2018,
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8},
doi = {10.1007/978-3-319-94821-8},
isbn = {978-3-319-94820-1}
}
@proceedings{abz2014,
booktitle = {Abstract State Machines, Alloy, B, VDM, and Z (ABZ)},
publisher = {Springer},
address = {Toulouse, France},
volume = 8477,
series = {Lecture Notes in Computer Science},
audience = {internationale},
year = 2014,
month = jun
}
@proceedings{nfm16,
booktitle = {8th NASA Formal Methods Symposium},
address = {Minneapolis, MN, USA},
audience = {internationale},
year = 2016,
month = jun,
editor = {Rayadurgam, Sanjai and Tkachuk, Oksana},
series = {Lecture Notes in Computer Science},
volume = {9690},
publisher = {Springer}
}
@proceedings{fm19,
title = {FM 2019 23rd International Symposium on Formal Methods},
booktitle = {FM 2019 23rd International Symposium on Formal Methods},
month = oct,
year = 2019,
address = {Porto, Portugal},
editor = {Annabelle McIver and Maurice ter Beek}
}