Journal articles

2007

auteur
Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu
titre
Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools
article
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.321-341. ⟨10.1007/s00165-007-0027-6⟩
DOI
DOI : 10.1007/s00165-007-0027-6
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00097383/file/fac07.pdf BibTex
auteur
Dominique Barth, Johanne Cohen, Alain Denise, Romain Rivière
titre
Shuffling biological sequences with motif constraints.
article
Journal of Discrete Algorithms, Elsevier, 2007, ⟨10.1016/j.jda.2007.06.001⟩
DOI
DOI : 10.1016/j.jda.2007.06.001
Accès au bibtex
BibTex
auteur
Dominique Barth, Johanne Cohen, Taoufik Faik
titre
On the B-Continuity Property of Graphs
article
Discrete Applied Mathematics, Elsevier, 2007, 155 (13), pp.1761 - 1768. ⟨10.1016/j.dam.2007.04.011⟩
DOI
DOI : 10.1016/j.dam.2007.04.011
Accès au bibtex
BibTex
auteur
Gilles Barthe, Leonor Prensa Nieto
titre
Secure Information Flow for a Concurrent Language with Scheduling
article
Journal of Computer Security, IOS Press, 2007, Formal Methods in Security Engineering Workshop (FMSE 04), 16 (6), pp.647 - 689
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00097395/file/barthe_prensa.pdf BibTex
auteur
Philippe Beaucamps
titre
Polymorphisme Viral sous Linux (Viral Polymorphism in Linux)
article
GNU/Linux Magazine France, Diamond Editions, 2007, Hors Série 32
Accès au bibtex
BibTex
auteur
Philippe Beaucamps, Eric Filiol
titre
On the possibility of practically obfuscating programs - Towards a unified perspective of code protection
article
Journal in Computer Virology, Springer Verlag, 2007, 3 (1), pp.3-21. ⟨10.1007/s11416-006-0029-6⟩
DOI
DOI : 10.1007/s11416-006-0029-6
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338074/file/beaucamps-filiol07-obfuscation.pdf BibTex
auteur
Jérôme Besombes, Jean-Yves Marion
titre
Learning tree languages from positive examples and membership queries
article
Theoretical Computer Science, Elsevier, 2007, 382 (3), pp.183-197
Accès au bibtex
BibTex
auteur
Nicolas Biri, Didier Galmiche
titre
Models and Separation Logics for Resource Trees
article
Journal of Logic and Computation, Oxford University Press (OUP), 2007, 17 (4), pp.687-726. ⟨10.1093/logcom/exm019⟩
DOI
DOI : 10.1093/logcom/exm019
Accès au bibtex
BibTex
auteur
Sandrine Blazy
titre
Comment gagner confiance en C ?
article
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2007, numéro spécial "Langages applicatifs", 26 (9), pp.1195-1200. ⟨10.3166/TSI.26.1195-1200⟩
DOI
DOI : 10.3166/TSI.26.1195-1200
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00292049/file/TSIchronique_sansentete.pdf BibTex
auteur
Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko
titre
Vérifier automatiquement les protocoles de sécurité
article
Techniques de l'Ingenieur, Techniques de l'ingénieur, 2007, pp.1-9
Accès au bibtex
BibTex
auteur
Anne Bonfante, Jean-Yves Marion
titre
On the defence notion
article
Journal in Computer Virology, Springer Verlag, 2007, 3 (4), pp.247-251. ⟨10.1007/s11416-007-0058-9⟩
DOI
DOI : 10.1007/s11416-007-0058-9
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00184985/file/bmg.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion
titre
Foreword of WTCV 06
article
Journal in Computer Virology, Springer Verlag, 2007, 3 (1), pp.1-2. ⟨10.1007/s11416-007-0038-0⟩
DOI
DOI : 10.1007/s11416-007-0038-0
Accès au bibtex
BibTex
auteur
Mohamed Salah Bouassida, Najah Chridi, Isabelle Chrisment, Olivier Festor, Laurent Vigneron
titre
Automated Verification of a Key Management Architecture for Hierarchical Group Protocols
article
Annals of Telecommunications - annales des télécommunications, Springer, 2007, 62 (11-12), pp.1365-1387
Accès au bibtex
BibTex
auteur
Olivier Bournez, Manuel L. Campagnolo, Daniel S. Graça, Emmanuel Hainry
titre
Polynomial differential equations compute all real computable functions on computable compact intervals
article
Journal of Complexity, Elsevier, 2007, 23 (3), pp.317--335
Accès au texte intégral et bibtex
https://hal-polytechnique.archives-ouvertes.fr/inria-00102947/file/JOC.pdf BibTex
auteur
Dominique Cansell, Dominique Méry
titre
Incremental Parametric Development of Greedy Algorithms
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2007, roceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006), 185, pp.47-62. ⟨10.1016/j.entcs.2007.05.028⟩
DOI
DOI : 10.1016/j.entcs.2007.05.028
Accès au bibtex
BibTex
auteur
Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
titre
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
article
Journal of Automated Reasoning, Springer Verlag, 2007, Journal of Automated Reasoning, 39 (1), pp.1-47. ⟨10.1007/s10817-006-9061-y⟩
DOI
DOI : 10.1007/s10817-006-9061-y
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01148347/file/2007-jar-07.pdf BibTex
auteur
Thierry Coquand, Arnaud Spiwack
titre
A Proof of Strong Normalisation Using Domain Theory
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2007, 16 p. ⟨10.2168/LMCS-3(4:12)2007⟩
DOI
DOI : 10.2168/LMCS-3(4:12)2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432448/file/sn4.pdf BibTex
auteur
Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu
titre
Relating two standard notions of secrecy
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2007, 3 (3, paper 2), pp.1-29. ⟨10.2168/LMCS-3(3:2)2007⟩
DOI
DOI : 10.2168/LMCS-3(3:2)2007
Accès au bibtex
BibTex
auteur
Eric Filiol, Jean-Yves Marion
titre
La virologie informatique - les virus, ennemis utiles
article
Pour la science, Pour la science, 2007, pp.60-64
Accès au bibtex
BibTex
auteur
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
titre
Decision procedures for extensions of the theory of arrays
article
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2007, 50 (3-4), pp.231-254. ⟨10.1007/s10472-007-9078-x⟩
DOI
DOI : 10.1007/s10472-007-9078-x
Accès au bibtex
BibTex
auteur
Matthieu Kaczmarek
titre
ELF et virologie informatique
article
GNU Linux Magasine France, DIAMOND EDITIONS, 2007, Septembre - Octobre, pp.12--19
Accès au bibtex
BibTex
auteur
Fairouz Kamareddine, Karim Nour
titre
A completeness result for a realisability semantics for an intersection type system
article
Annals of Pure and Applied Logic, Elsevier Masson, 2007, 146, pp.180-198
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00380177/file/general7.pdf BibTex
auteur
Eunyoung Kang, Stephan Merz
titre
Predicate Diagrams for the Verification of Real-Time Systems
article
Formal Aspects of Computing, Springer Verlag, 2007, 19 (3), pp.401-413. ⟨10.1007/s00165-007-0030-y⟩
DOI
DOI : 10.1007/s00165-007-0030-y
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00112065/file/0819.pdf BibTex
auteur
Dominique Larchey-Wendling
titre
Graph-based decision for Gödel-Dummett logics
article
Journal of Automated Reasoning, Springer Verlag, 2007, 38 (1-3), pp.201-225. ⟨10.1007/s10817-006-9047-9⟩
DOI
DOI : 10.1007/s10817-006-9047-9
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00105564/file/larchey_final.pdf BibTex
auteur
Thierry Lecomte, Dominique Méry, Dominique Cansell
titre
Patrons de conception prouvés
article
Génie Logiciel - Magazine de l'ingéniérie du logiciel et des systèmes, GL & IS - 8, rue du Parc - 92190 MEUDON, 2007, Ingénierie dirigée par les modèles, pp.14-18
Accès au bibtex
BibTex
auteur
Dominique Méry, Stephan Merz
titre
Specification and Refinement of Access Control
article
Journal of Universal Computer Science, Springer, 2007, 13 (8), pp.1073-1093
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
A complex drawing in descriptive geometry
article
Tugboat, TeX Users Group, 2007, 28 (2), pp.218-228
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Sphères, grands cercles et parallèles
article
Cahiers Gutenberg, Association GUTenberg, 2007, Avril 2007 (48), pp.7-22
Accès au bibtex
BibTex
auteur
Denis Roegel
titre
Review of ``Mathematical Illustrations: A Manual of Geometry and PostScript
article
Notices of the American Mathematical Society, American Mathematical Society, 2007, 54 (1), pp.38-42
Accès au bibtex
BibTex
auteur
Benjamin Werner
titre
Preuves formelles, preuves calculatoires
article
Interstices, INRIA, 2007, ⟨https://interstices.info/jcms/c_23115/preuves-formelles-preuves-calculatoires⟩
Accès au bibtex
BibTex

Conference papers

2007

auteur
Siva Anantharaman, Paliath Narendran, Michael Rusinowitch
titre
Intruders with Caps
article
Rewriting Techniques and Applications - RTA'07, Jun 2007, Paris, France. pp.20--35
Accès au bibtex
BibTex
auteur
Andrew W. Appel, Sandrine Blazy
titre
Separation Logic for Small-step Cminor
article
20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00165915/file/paperTPHOL.pdf BibTex
auteur
Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune
titre
Combining algorithms for deciding knowledge in security protocols
article
6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom
Accès au bibtex
BibTex
auteur
Bruno Barras, Bruno Bernardo
titre
The Implicit Calculus of Constructions as a Programming Language with Dependent Types
article
International Workshop on Type theory, proof theory, and rewriting (TPR'07), Gilles Dowek, Jun 2007, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432658/file/icc_barras_bernardo-tpr07.pdf BibTex
auteur
Dominique Barth, Olivier Bournez, Octave Boussaton, Johanne Cohen
titre
Convergences et dynamiques du routage dans les réseaux
article
Journées Pôle ResCom, Sep 2007, Toulouse, France
Accès au bibtex
BibTex
auteur
Dominique Barth, Johanne Cohen, Loubna Echabbi, Chahinez Hamlaoui
titre
Transit prices negotiation: Combined repeated game and distributed algorithmic approach
article
First EuroFGI International Conference on Network Control and Optimization - NET-COOP 2007, Jun 2007, Avignon, France. pp.266-275, ⟨10.1007/978-3-540-72709-5_28⟩
DOI
DOI : 10.1007/978-3-540-72709-5_28
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00180914/file/netcop_echabbi.pdf BibTex
auteur
Philippe Beaucamps
titre
Advanced Metamorphic Techniques in Computer Viruses
article
International Conference on Computer, Electrical, and Systems Science, and Engineering - CESSE'07, Nov 2007, Venice, Italy
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338066/file/beaucamps07-metamorphism.pdf BibTex
auteur
Boulbaba Ben Ammar, Mahamed Tahar Bhiri, Jeanine Souquières
titre
Quelques patrons de raffinement pour le développement de diagrammes de classes UML
article
6ème atelier sur les Objets, Composants et Modèles dans l'ingénierie des Systèmes d'Information, OCM-SI, couplé avec le 25ème congrès INFORSID, May 2007, Perros-Guirec, France. 12 p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00182740/file/OCM-benammar.pdf BibTex
auteur
Nazim Benaissa, Dominique Cansell, Dominique Mery
titre
Integration of Security Policy into System Modeling
article
The 7th International B Conference - B2007, Jan 2007, Besançon, France
Accès au bibtex
BibTex
auteur
Pascal Berthomé, Johanne Cohen, Thierry Mautor
titre
Optimisation du temps de broadcast dans un modèle de communication en ligne pondéré
article
Programme de la conférence conjointe Francoro V / Roadef 2007, Feb 2007, Grenoble, France
Accès au bibtex
BibTex
auteur
Sandrine Blazy
titre
Experiments in validating formal semantics for C
article
C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00292043/file/C07Blazy.pdf BibTex
auteur
Sandrine Blazy, Benoît Robillard, Eric Soutif
titre
Coloration avec préférences dans les graphes triangulés
article
Journées Graphes et algorithmes (JGA'07), Nov 2007, Paris, France. pp.32
Accès au bibtex
BibTex
auteur
Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko
titre
Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives
article
9th International Workshop on Verification of Infinite-State Systems - INFINITY'07, 2007, Lisbonnes, Portugal. pp.57-72
Accès au bibtex
BibTex
auteur
Guillaume Bonfante, Matthieu Kaczmarek, Jean-Yves Marion
titre
Control Flow Graphs as Malware Signatures
article
International Workshop on the Theory of Computer Viruses, Matthieu Kaczmarek; Guillaume Bonfante, May 2007, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00176235/file/tcv07b.pdf BibTex
auteur
Guillaume Bonfante, Matthieu Kaczmarek, Jean-Yves Marion
titre
Control Flow to Detect Malware
article
Inter-Regional Workshop on Rigorous System Development and Analysis 2007, Pascal Fontaine; Stephan Merz, Oct 2007, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00176241/file/IRWRSDA.pdf BibTex
auteur
Guillaume Bonfante, Jean-Yves Marion, Romain Péchoux
titre
Quasi-interpretation Synthesis by Decomposition : An application to higher-order programs
article
ICTAC, Sep 2007, Macao, China
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00130920/file/modu.pdf BibTex
auteur
Guillaume Bonfante, Matthieu Kaczmarek, Jean-Yves Marion
titre
A Classification of Viruses through Recursion Theorems
article
Computability in Europe, Jun 2007, Sienna, Italy. pp.73-82, ⟨10.1007/978-3-540-73001-9_8⟩
DOI
DOI : 10.1007/978-3-540-73001-9_8
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00175301/file/bonfante.a_classification_of_computer_viruses_through_recursion_theorems.pdf BibTex
auteur
Guillaume Bonfante, Yves Guiraud
titre
Intensional properties of polygraphs
article
4th International Workshop on Computing with Terms and Graphs - TERMGRAPH 2007, Mar 2007, Braga, Portugal. ⟨10.1016/j.entcs.2008.03.034⟩
DOI
DOI : 10.1016/j.entcs.2008.03.034
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00129391/file/termgraph.pdf BibTex
auteur
Richard Bonichon, David Delahaye, Damien Doligez
titre
Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs
article
LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. pp.151-165, ⟨10.1007/978-3-540-75560-9_13⟩
DOI
DOI : 10.1007/978-3-540-75560-9_13
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00315920/file/bonichon-delahaye-doligez-lpar-2007.pdf BibTex
auteur
Fabrice Bouquet, Jean-François Couchot, Frédéric Dadeau, Alain Giorgetti
titre
Instantiation of Parameterized Data Structures for Model-Based Testing
article
7th International Formal Specification and Development in B Conference, B 2007, Jan 2007, Besançon, France. pp.96--110, ⟨10.1007/11955757⟩
DOI
DOI : 10.1007/11955757
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00563282/file/bcdg07_ip.pdf BibTex
auteur
Olivier Bournez, Emmanuel Hainry
titre
On the Computational Capabilities of Several Models
article
5th International Conference on Machines, Computations and Universality - MCU 2007, Sep 2007, Orléans, France. pp.12-23
Accès au bibtex
BibTex
auteur
Dominique Cansell, Dominique Méry
titre
Proved-Patterns-Based Development for Structured Programs.
article
Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Ural State University (USU) ; Institute of Mathematics and Mechanics of Ural Branch of Russian Academy of Sciences, Sep 2007, Ekaterinburg, Russia. pp.104-114, ⟨10.1007/978-3-540-74510-5_13⟩
DOI
DOI : 10.1007/978-3-540-74510-5_13
Accès au bibtex
BibTex
auteur
Dominique Cansell, Paul Gibson, Dominique Méry
titre
Formal verification of tamper-evident storage for e-voting
article
5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007, Sep 2007, LONDON, United Kingdom. pp.329-338, ⟨10.1109/SEFM.2007.21⟩
DOI
DOI : 10.1109/SEFM.2007.21
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00184833/file/mery-e-voting.pdf BibTex
auteur
Dominique Cansell, Dominique Méry, Joris Rehm
titre
Time Constraint Patterns for Event B Development
article
7th International Conference of B Users, January 17-19, 2007, 2007, Besançon, France. pp.140-154, ⟨10.1007/11955757_13⟩
DOI
DOI : 10.1007/11955757_13
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00149163/file/B2007cansellmeryrehm.pdf BibTex
auteur
Yannick Chevalier, Denis Lugiez, Michael Rusinowitch
titre
Towards an Automatic Analysis of Web Service Security
article
6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom. pp.133-147, ⟨10.1007/978-3-540-74621-8_9⟩
DOI
DOI : 10.1007/978-3-540-74621-8_9
Accès au bibtex
BibTex
auteur
Yannick Chevalier, Denis Lugiez, Michael Rusinowitch
titre
Verifying Cryptographic Protocols with Subterms Constraints
article
14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR 2007, Oct 2007, Yerevan, Armenia. pp.181-195, ⟨10.1007/978-3-540-75560-9_15⟩
DOI
DOI : 10.1007/978-3-540-75560-9_15
Accès au bibtex
BibTex
auteur
Samuel Colin, Arnaud Lanoix, Jeanine Souquières
titre
Trustworthy interface compliancy: data model adaptation using B refinement
article
Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA), Satellite workshop of ETAPS, Mar 2007, Braga, Portugal. 13 p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00123884/file/RR-fesca.pdf BibTex
auteur
Thierry Coquand, Arnaud Spiwack
titre
Towards Constructive Homological Algebra in Type Theory
article
CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p., ⟨10.1007/978-3-540-73086-6_4⟩
DOI
DOI : 10.1007/978-3-540-73086-6_4
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432525/file/v2.pdf BibTex
auteur
Véronique Cortier, Jérémie Delaitre, Stéphanie Delaune
titre
Safely Composing Security Protocols
article
27th Conference on Foundations of Software Technology and Theoretical Computer Science - FSTTCS'07, Dec 2007, New Delhi, India
Accès au bibtex
BibTex
auteur
Véronique Cortier, Ralf Kuesters, Bogdan Warinschi
titre
A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols.
article
12th European Symposium On Research In Computer Security - ESORICS'07, Sep 2007, Dresden, Germany. pp.422-437
Accès au bibtex
BibTex
auteur
Véronique Cortier, Stéphanie Delaune, Graham Steel
titre
A Formal Theory of Key Conjuring.
article
20th IEEE Computer Security Foundations Symposium - CSF'07, Jul 2007, Venice, Italy. pp.79-96
Accès au bibtex
BibTex
auteur
Véronique Cortier, Stéphanie Delaune
titre
Deciding knowledge in security protocols for monoidal equational theories.
article
Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - FCS-ARSPA'07, Jul 2007, Wrocław, Poland
Accès au bibtex
BibTex
auteur
Véronique Cortier, Stéphanie Delaune
titre
Deciding knowledge in security protocols for monoidal equational theories.
article
14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'07, Oct 2007, Yerevan, Armenia
Accès au bibtex
BibTex
auteur
Véronique Cortier, Ralf Kuesters, Bogdan Warinschi
titre
A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols.
article
3rd Workshop on Formal and Computational Cryptography - FCC 2007, Jul 2007, Venise, Italy
Accès au bibtex
BibTex
auteur
Véronique Cortier, Bogdan Warinschi, Eugen Zalinescu
titre
Synthetizing secure protocols
article
12th European Symposium On Research In Computer Security - ESORICS'07, Sep 2007, Dresden, Germany. pp.406-421
Accès au bibtex
BibTex
auteur
Véronique Cortier, Eugen Zalinescu
titre
Deciding key cycles for security protocols.
article
3rd Workshop on Formal and Computational Cryptography - FCC 2007, Jul 2007, Venise, Italy
Accès au bibtex
BibTex
auteur
Véronique Cortier, Keighren Gavin, Graham Steel
titre
Automatic Analysis of the Security of XOR-based Key Management Schemes.
article
13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07),, Mar 2007, Braga, Portugal. pp.538-552
Accès au bibtex
BibTex
auteur
Zaynah Dargaye, Xavier Leroy
titre
Mechanized verification of CPS transformations
article
Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, Oct 2007, Erevan, Armenia. pp.211-225, ⟨10.1007/978-3-540-75560-9_17⟩
DOI
DOI : 10.1007/978-3-540-75560-9_17
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289541/file/cps-dargaye-leroy.pdf BibTex
auteur
Zaynah Dargaye
titre
Décurryfication certifiée
article
Journées Francophones des Langages Applicatifs (JFLA 2007), INRIA, Jan 2007, Aix-les-Bains, France. pp.119-134
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338974/file/dargaye.pdf BibTex
auteur
Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
titre
haRVey : satisfaisabilité et théories
article
Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. pp.287-288
Accès au bibtex
BibTex
auteur
Eric Descourvières, Stéphane Debricon, Dominique Gendreau, Philippe Lutz, Laurent Philippe, Fabrice Bouquet
titre
Towards automatic control for microfactories.
article
5th International Conference on Industrial Automation, IAIA'2007., Jun 2007, Montréal, Canada. sur CD ROM - 4 p
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00163847/file/Descourvieres2007AIAI.pdf BibTex
auteur
Loïc Fejoz, Stephan Merz
titre
Dérivation d'algorithmes sans verrou à partir d'une spécification atomique
article
Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Marie-Laure Potet (IMAG, Grenoble) ; Pierre-Yves Schobbens (Facultés Universitaires Notre-Dame de la Paix - Namur, Belgique), Jun 2007, Namur, Belgique. pp.213-226
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00162146/file/afadl07-fejoz-merz.pdf BibTex
auteur
Pascal Fontaine
titre
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class
article
4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. pp.37-54
Accès au bibtex
BibTex
auteur
Didier Galmiche, Dominique Larchey-Wendling, Yakoub Salhi
titre
Provability and Countermodels in Gödel-Dummett Logics
article
International Workshop on Disproving: Non-theorems, Non-validity, Non-Provability - DISPROVING'07, Jul 2007, Bremen, Germany. pp.35-52
Accès au bibtex
BibTex
auteur
Didier Galmiche, Daniel Mery
titre
Connection-based proof search in intuitionistic logic from transitive closure of constraints
article
International Workshop on Automated Deduction: Decidability, Complexity, Tractability - ADDCT'07, Jul 2007, Bremen, Germany. pp.15
Accès au bibtex
BibTex
auteur
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
titre
Noetherianity and Combination Problems
article
Frontiers of Combining Systems, Sep 2007, Liverpool, United Kingdom. pp.206-220, ⟨10.1007/978-3-540-74621-8_14⟩
DOI
DOI : 10.1007/978-3-540-74621-8_14
Accès au bibtex
BibTex
auteur
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
titre
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
article
Automated Deduction - CADE-21, Jul 2007, Bremen, Germany. pp.362-378, ⟨10.1007/978-3-540-73595-3_25⟩
DOI
DOI : 10.1007/978-3-540-73595-3_25
Accès au bibtex
BibTex
auteur
Alain Giorgetti, Julien Groslambert
titre
Un programme annoté en vaut deux
article
Journée Francophone des Langages Applicatifs - JFLA07, Jan 2007, Aix-les-Bains, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00181135/file/GG07.pdf BibTex
auteur
Isabelle Gnaedig
titre
Induction for Positive Almost Sure Termination
article
PPDP 2007 - 9th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming, Jul 2007, Wroclaw, Poland. pp.167-177
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00182435/file/ppdp11b-gnaedig-preprint.pdf BibTex
auteur
Isabelle Gnaedig, Hélène Kirchner
titre
Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations
article
Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Jun 2007, Paris, France. pp.44-67
Accès au bibtex
BibTex
auteur
Nawal Guermouche, Olivier Perrin, Christophe Ringeissen
titre
Timed Specification For Web Services Compatibility Analysis
article
International Workshop on Automated Specification and Verification of Web Systems - WWV 2007, Dec 2007, San Servolo island, Venice, Italy
Accès au bibtex
BibTex
auteur
Pierre-Cyrille Heam, Olga Kouchnarenko, Jérôme Voinot
titre
How to Handle QoS Aspects in Web Services Substitutivity Verification
article
16th IEEE International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises - WETICE 2007, Jun 2007, Paris, France
Accès au bibtex
BibTex
auteur
Clément Hurlin, Amine Chaib, Pascal Fontaine, Stephan Merz, Tjark Weber
titre
Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions
article
The Isabelle Workshop 2007 - Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13
Accès au bibtex
BibTex
auteur
Jean-Pierre Jacquot, Stéphane Devaux
titre
Initiation à l'enseignement des sciences à l'école
article
Les pédagogies actives : enjeux et conditions, Jan 2007, Louvain la neuve, Belgique. pp.303-311
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00170668/file/Jacquot-Devaux-32.pdf BibTex
auteur
Arnaud Lanoix, Samuel Colin, Jeanine Souquières
titre
Schémas de développement d'adaptateurs à l'aide de B
article
Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'07), Jun 2007, Namur, Belgique. pp.91-108
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00131340/file/main.pdf BibTex
auteur
Arnaud Lanoix, Denis Hatebur, Maritta Heisel, Jeanine Souquières
titre
Enhancing Dependability of Component-based Systems
article
Reliable Software Technologies Ada-Europe 2007, 2007, Genève, Switzerland. pp.41--54
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00123999/file/rst07-submitted.pdf BibTex
auteur
Dominique Larchey-Wendling
titre
Relational semantics and finite models of separation logics
article
Modèles de calcul, Modèles finis et Complexité CMF'2007, May 2007, Vandoeuvre-lès-Nancy, France
Accès au bibtex
BibTex
auteur
Christopher Lynch, Duc-Khanh Tran
titre
Automatic Decidability and Combinability Revisited
article
Automated Deduction - CADE-21, 2007, Bremen, Germany. pp.328-344, ⟨10.1007/978-3-540-73595-3_22⟩
DOI
DOI : 10.1007/978-3-540-73595-3_22
Accès au bibtex
BibTex
auteur
Jean-Yves Marion, Romain Péchoux
titre
Resource control of object-oriented programs
article
The International Workshop on Logic and Computational Complexity - LCC 2007, Jul 2007, Wroclaw/Poland, Poland
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00155288/file/objet.pdf BibTex
auteur
Jean-Yves Marion
titre
Predicative Analysis of Feasibility and Diagonalization
article
Typed Lambda Calculi and Applications, 8th International Conference - TLCA 2007, Jun 2007, Paris, France. pp.290-304
Accès au bibtex
BibTex
auteur
Virgile Mogbil, Vincent Rahli
titre
Uniform circuits, & Boolean proof nets
article
International Symposium of Logical Foundations of Computer Science (LFCS 2007), Jun 2007, New York, United States. pp. 401-421, ⟨10.1007/978-3-540-72734-7⟩
DOI
DOI : 10.1007/978-3-540-72734-7
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00122980/file/mwBN_preprintLIPN07.pdf BibTex
auteur
Olfa Mosbahi, Leila Jemni, Jacques Jaray
titre
A Formal Approach for the Development of Automated Systems
article
2nd International Conference on Software and Data Technologies - ICSOFT 2007, INSTICC - Institute for Systems and Technologies of Information, Control and Communication, Jul 2007, Barcelone, Spain. pp.304-310
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00158908/file/paper_382.pdf BibTex
auteur
Olfa Mosbahi, Jacques Jaray
titre
Specification and Proof of Liveness Properties in B Event Systems
article
2nd International Conference on Software and Data Technologies - ICSOFT 2007, INSTICC - Institute for Systems and Technologies of Information, Control and Communication, Jul 2007, Barcelone, Spain. pp.25-34
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00158906/file/mosbahi_381.pdf BibTex
auteur
Olfa Mosbahi, Jacques Jaray, Samir Ben Ahmed
titre
Spécification et vérification des propriétés de vivacité en B événementiel
article
6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs - MSR 2007, Oct 2007, Lyon, France. 16 p
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00172417/file/MSR2007.pdf BibTex
auteur
Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran
titre
Combining Proof-Producing Decision Procedures
article
6th International Symposium o Frontiers of Combining Systems - FroCoS 2007, Boris Konev and Frank Wolter, Sep 2007, Liverpool, United Kingdom. pp.237-251, ⟨10.1007/978-3-540-74621-8_16⟩
DOI
DOI : 10.1007/978-3-540-74621-8_16
Accès au bibtex
BibTex
auteur
Joris Rehm, Dominique Cansell
titre
Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method
article
ISoLA 2007 Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Dec 2007, Poitiers-Futuroscope, France. pp.179-190
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00184837/file/article.pdf BibTex
auteur
Judson Santos Santiago, Laurent Vigneron
titre
Optimistic Non-repudiation Protocol Analysis
article
Information Security Theory and Practices - Smart Cards, Mobile and Ubiquitous Computing Systems, May 2007, Heraklion, Greece. pp.90-101, ⟨10.1007/978-3-540-72354-7_8⟩
DOI
DOI : 10.1007/978-3-540-72354-7_8
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00176333/file/SantiagoV-WISTP07.pdf BibTex
auteur
Bill Stoddart, Dominique Cansell, Frank Zeyda
titre
Modelling and Proof Analysis of Interrupt Driven Scheduling
article
The 7th International B Conference - B 2007, Jacques Jullian et Olga Kouchnarenko, Jan 2007, Besançon/France, pp.155-170, ⟨10.1007/11955757_14⟩
DOI
DOI : 10.1007/11955757_14
Accès au bibtex
BibTex
auteur
Yann Zimmermann
titre
Développement formel de circuits électroniques par la méthode B
article
Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Pierre-Yves Schobbens, Jun 2007, Namur, Belgique. pp.181-198
Accès au bibtex
BibTex

Book sections

2007

auteur
Dominique Cansell, Dominique Méry
titre
Designing old and new distributed algorithms by replaying an incremental proof-based development
article
Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS
Accès au bibtex
BibTex
auteur
Michael Leuschel, Dominique Cansell, Michael Butler
titre
Validating and Animating Higher-Order Recursive Functions in B
article
Jean-Raymond Abrial and Uwe Glässer. Festschrift for Egon Börger, Springer-Verlag, 2007, LNCS
Accès au bibtex
BibTex
auteur
Laurent Vigneron, Najah Chridi
titre
Strategy for Flaws Detection based on a Services-driven Model for Group Protocols
article
Frédéric Benhamou and Narendra Jussien and Barry O\'Sullivan. Future and Trends in Constraint Programming, ISTE, pp.361-370, 2007, 1905209975
Accès au bibtex
BibTex

Directions of work or proceedings

2007

auteur
Stephan Merz, Tobias Nipkow
titre
Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006)
article
Michael Mislove. 185, Elsevier, pp.151, 2007, Electronic Notes in Theoretical Computer Science
Accès au bibtex
BibTex
auteur
Jeanine Souquières
titre
Approches formelles pour le développement de logiciels
article
Lavoisier (Hermes), pp.128, 2007
Accès au bibtex
BibTex

Other publications

2007

auteur
Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch
titre
Intruders with Caps
article
2007
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00144178/file/Lifo-RR2007-02.pdf BibTex
auteur
Boulbaba Ben Ammar, Mohamed Tahar Bhiri, Jeanine Souquières
titre
Incremental development of UML specifications using operation refinements
article
2007
Accès au bibtex
BibTex
auteur
Boulbaba Ben Ammar, Mohamed Tahar Bhiri, Jeanine Souquières
titre
Towards an incremental development of UML specifications
article
2007
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00182180/file/FP-UML-Ben-Ammar.pdf BibTex
auteur
Guillaume Bonfante, Joseph Le Roux
titre
Intersection Optimization is NP Complete
article
2007
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00146671/file/intersection.pdf BibTex
auteur
Samir Chouali, Samuel Colin, Ahmed Hammad, Olga Kouchnarenko, Arnaud Lanoix, Hassan Mountassir, Jeanine Souquières
titre
Requirements for the description of a component in order to use in a component based approach -- Livrable TACOS L2-1.0
article
2007
Accès au bibtex
BibTex
auteur
Isabelle Coté, Maritta Heisel, Jeanine Souquières
titre
On the Evolution of Component-based Software
article
2007
Accès au bibtex
BibTex
auteur
Inès Mouakher, Francis Alexandre, Jeanine Souquières
titre
Protocol verification in a software component approach
article
2007
Accès au bibtex
BibTex
auteur
Sebti Mouelhi
titre
Vérification formelle d'algorithmes distribués en +CAL
article
2007
Accès au bibtex
BibTex

Books

2007

auteur
Michel Goossens, Frank Mittelbach, Sebastian Rahtz, Denis Roegel, Herbert Voss
titre
The LaTeX Graphics Companion, Second Edition - Tools and Techniques for Computer Typesetting
article
Addison-Wesley, pp.976, 2007, ISBN-10: 0321508920 / ISBN-13: 978-0321508928
Accès au bibtex
BibTex

Reports

2007

auteur
Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune
titre
Combining algorithms for deciding knowledge in security protocols
article
[Research Report] RR-6118, INRIA. 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00129418/file/RR-6118.pdf BibTex
auteur
Guillaume Bonfante
titre
Monotone interpretations
article
[Research Report] 2007, pp.9
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00145060/file/bqi.pdf BibTex
auteur
Yannick Chevalier, Denis Lugiez, Michael Rusinowitch
titre
Toward an Automatic Analysis of Web Service Security
article
[Research Report] RR-6341, INRIA. 2007, pp.40
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00133996/file/RR-6341.pdf BibTex
auteur
Véronique Cortier, Jérémie Delaitre, Stéphanie Delaune
titre
Safely composing security protocols
article
[Research Report] RR-6234, INRIA. 2007, pp.26
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00157889/file/RR-6234.pdf BibTex
auteur
Véronique Cortier, Stéphanie Delaune, Graham Steel
titre
A Formal Theory of Key Conjuring
article
[Research Report] RR-6134, INRIA. 2007, pp.38
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00129642/file/RR-6134.pdf BibTex
auteur
Véronique Cortier, Bogdan Warinschi, Eugen Zalinescu
titre
Synthesizing secure protocols
article
[Research Report] RR-6166, INRIA. 2007, pp.32
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00140932/file/RR-6166.pdf BibTex
auteur
Zalinescu Eugen, Véronique Cortier, Bogdan Warinschi
titre
From passive to active security via a simple transformation
article
[Research Report] 2007
Accès au bibtex
BibTex
auteur
Alain Frisch, Haruo Hosoya
titre
Towards Practical Typechecking for Macro Tree Transducers
article
[Research Report] RR-6107, INRIA. 2007, pp.28
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00126895/file/RR-6107.pdf BibTex
auteur
Isabelle Gnaedig
titre
Induction for Positive Almost Sure Termination - Extended version
article
[Research Report] 2007, pp.16
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00147450/file/IPAS-termin-extended.pdf BibTex
auteur
Nawal Guermouche, Olivier Perrin, Christophe Ringeissen
titre
A Methodology For Web Services Composition
article
[Intern report] 2007
Accès au bibtex
BibTex
auteur
Pierre-Cyrille Heam, Olga Kouchnarenko, Jérôme Voinot
titre
Towards Formalizing QoS of Web Services with Weighted Automata
article
[Research Report] RR-6218, INRIA. 2007, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00154453/file/RR-6218.pdf BibTex
auteur
Pierre-Cyrille Héam
titre
Transitive Closures of Semi-commutation Relations on Regular omega-Languages
article
[Research Report] RR-6239, INRIA. 2007, pp.20
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00158285/file/RR-6239.pdf BibTex
auteur
Francis Klay, Judson Santiago, Laurent Vigneron
titre
Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder
article
[Research Report] RR-6324, INRIA. 2007, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00179550/file/RR-6324.pdf BibTex
auteur
Xavier Leroy
titre
A locally nameless solution to the POPLmark challenge
article
[Research Report] RR-6098, INRIA. 2007, pp.54
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00123945/file/RR-6098.pdf BibTex
auteur
Jean-Yves Marion, Romain Péchoux
titre
A characterization of polynomial complexity classes using dependency pairs
article
[Research Report] 2007, pp.12
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00155287/file/dependency.pdf BibTex
auteur
Denis Roegel
titre
Three dials, and a few more: a practical introduction to accurate gnomonics
article
[Technical Report] 2007, pp.70
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00172407/file/article-sundials.pdf BibTex
auteur
Olivier Simonin, Arnaud Lanoix, Samuel Colin, Alexis Scheuer, François Charpillet
titre
Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems
article
[Research Report] RR-6304, INRIA. 2007, pp.18
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00173876/file/SimoninEtalRR07.pdf BibTex

Theses

2007

auteur
Heinrich Hördegen
titre
Vérification des protocoles cryptographiques : Comparaison des modèles symboliques avec une application des résultats --- Etude des protocoles récursifs
article
Autre [cs.OH]. Université Henri Poincaré - Nancy I, 2007. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00193300/file/thesis.pdf BibTex
auteur
Eunyoung Kang
titre
Tool supported real-time system verification with combination of abstraction/deduction and model checking
article
Software Engineering [cs.SE]. Université Henri Poincaré - Nancy I, 2007. English
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00195096/file/thesis.pdf BibTex
auteur
Romain Pechoux
titre
Analyse de la complexité des programmes par interprétation sémantique
article
Informatique [cs]. Institut National Polytechnique de Lorraine - INPL, 2007. Français. ⟨NNT : 2007INPL084N⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01752904/file/manuscrit.pdf BibTex
auteur
Duc-Khanh Tran
titre
Conception de Procédures de Décision par Combinaison et Saturation
article
Génie logiciel [cs.SE]. Université Henri Poincaré - Nancy I, 2007. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00580582/file/These-DKT.pdf BibTex
auteur
Eugen Zalinescu
titre
Sécurité des protocoles cryptographiques : décidabilité et résultats de transfert
article
Génie logiciel [cs.SE]. Université Henri Poincaré - Nancy I, 2007. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00338362/file/ez-thloria.pdf BibTex

Preprints, Working Papers, ...

2007

auteur
Laurence Rideau, Bernard Serpette, Xavier Leroy
titre
Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves
article
2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00176007/file/pmov.pdf BibTex