2012-conference.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2012-conference.cite -ob 2012-conference.bib -c 'year = 2012 and topics : "team" and $type="inproceedings"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@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{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{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{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{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
}
@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{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{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{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{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}
}