@comment{{This file has been generated by bib2bib 1.97pl2}}

@comment{{Command line: bib2bib -oc 2007-conference.cite -ob 2007-conference.bib -c 'year = 2007 and topics : "team" and $type="inproceedings"' /users/demons/filliatr/bibliodemons/abbrevs.bib /users/demons/filliatr/bibliodemons/demons.bib /users/demons/filliatr/bibliodemons/demons2.bib /users/demons/filliatr/bibliodemons/demons3.bib /users/demons/filliatr/bibliodemons/team.bib /users/demons/filliatr/bibliodemons/crossrefs.bib}}

@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 = {June}, 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{BoldoFilliatre07, author = {Sylvie Boldo and Jean-Christophe Filli\^atre}, title = {{Formal Verification of Floating-Point Programs}}, booktitle = {18th IEEE International Symposium on Computer Arithmetic}, pages = {187-194}, month = {June}, year = 2007, 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 = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf}, url = {http://www.lri.fr/~filliatr/ftp/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{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 = {http://dx.doi.org/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{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 = {http://www.lri.fr/~filliatr/ftp/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 = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf}, url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf}, x-editorial-board = {yes}, x-international-audience = {yes}, x-proceedings = {yes} }

@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 = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf}, url = {http://www.lri.fr/~filliatr/ftp/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}, pages = {37--45}, year = 2007, address = {Freiburg, Germany}, month = {October}, topics = {team, lri}, type_publi = {icolcomlec}, type_digiteo = {conf_isbn}, x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf}, url = {http://www.lri.fr/~filliatr/ftp/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{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 = {http://dx.doi.org/10.1007/978-3-540-74621-8_10}, abstract = {http://www.lri.fr/~contejea/publis/2007frocos/abstract.html} }

@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{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}, type_digiteo = {conf_isbn}, type_publi = {icolcomlec}, x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf}, url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf}, x-equipes = {demons PROVAL EXT}, x-type = {articlecourt}, x-support = {actes}, x-cle-support = {CAV} }

@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, note = {\url{http://knuth07.labri.fr/exposes.php}}, address = {Bordeaux, France}, month = {October}, topics = {team, lri}, type_publi = {colcomlec}, type_digiteo = {conf_autre}, x-pdf = {http://www.lri.fr/~filliatr/publis/verifmix.pdf}, url = {http://www.lri.fr/~filliatr/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{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}, type_publi = {icolcomlec}, type_digiteo = {conf_autre}, pages = {81--93}, url = {http://www.lri.fr/~marche/hubert07hav.pdf}, x-pdf = {http://www.lri.fr/~marche/hubert07hav.pdf}, 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{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 = {http://doi.acm.org/10.1145/1292597.1292598}, url = {http://doi.acm.org/10.1145/1292597.1292598}, publisher = {ACM}, 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{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{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{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{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 = {http://doi.acm.org/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, http://doi.acm.org/10.1145/1291151.1291156}, 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} }

@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{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{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{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{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{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{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{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} }