Publications HAL

2018

Conference papers

titre
Analyzing the Fundamental Liveness Property of the Chord Protocol
auteur
Julien Brunel, David Chemouil, Jeanne Tawa
article
Formal Methods in Computer-Aided Design, Oct 2018, Austin, United States
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01862755/file/final.pdf BibTex
titre
The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications
auteur
Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo
article
33rd ACM/IEEE International Conference on Automated Software Engineering (ASE ’18), Sep 2018, Montpellier, France. ⟨10.1145/3238147.3240475⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01846951/file/reprint.pdf BibTex
titre
Proposition of an Action Layer for Electrum
auteur
Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo, Jeanne Tawa
article
6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, Jun 2018, Southampton, United Kingdom. pp.397-402, ⟨10.1007/978-3-319-91271-4_30⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01774920/file/final.pdf BibTex

2017

Conference papers

titre
Sur l’assignation de buts comportementaux à des coalitions d’agents
auteur
Christophe Chareton, Julien Brunel, David Chemouil
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01863437/file/finale.pdf BibTex
titre
Spécification légère et analyse de systèmes dynamiques munis de configurations riches
auteur
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, Denis Kuperberg
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02077323/file/finale.pdf BibTex

2016

Conference papers

titre
Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations
auteur
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, Denis Kuperberg
article
Foundations of Software Engineering, Nov 2016, Seattle, United States. ⟨10.1145/2950290.2950318⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01355062/file/electrum.pdf BibTex
titre
On Finite Domains in First-Order Linear Temporal Logic
auteur
Denis Kuperberg, Julien Brunel, David Chemouil
article
14th International Symposium on Automated Technology for Verification and Analysis, Oct 2016, Chiba, Japan. ⟨10.1007/978-3-319-46520-3_14⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01343197/file/atva16-long.pdf BibTex

2015

Journal articles

titre
A Logic with Revocable and Refinable Strategies
auteur
Christophe Chareton, Julien Brunel, David Chemouil
article
Information and Computation, Elsevier, 2015, 242, pp.157-182. ⟨http://www.sciencedirect.com/science/article/pii/S0890540115000309⟩. ⟨10.1016/j.ic.2015.03.015⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00785659/file/20150409-preprint-HAL.pdf BibTex

Conference papers

titre
Safety and Security Assessment of Behavioral Properties Using Alloy
auteur
Julien Brunel, David Chemouil
article
2nd International workshop on the Integration of Safety and Security Engineering, Sep 2015, Delft, Netherlands. ⟨10.1007/978-3-319-24249-1_22⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01206638/file/main.pdf BibTex
titre
Evaluating the Assignment of Behavioral Goals to Coalitions of Agents
auteur
Christophe Chareton, Julien Brunel, David Chemouil
article
Brazilian Symposium on Formal Methods, Sep 2015, Belo Horizonte, Brazil. ⟨10.1007/978-3-319-29473-5_4⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01206625/file/main.pdf BibTex

2014

Conference papers

titre
A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures
auteur
Julien Brunel, David Chemouil, Laurent Rioux, Mohamed Bakkali, Frédérique Vallée
article
11th Workshop on Model-Driven Engineering, Verification and Validation, Sep 2014, Spain. pp.39-48
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01070960/file/main.pdf BibTex
titre
Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy
auteur
Julien Brunel, David Chemouil, Vincent Ibanez, Nicolas Meledo
article
Embedded real-time software and systems (ERTS² 2014), Feb 2014, TOULOUSE, France
Accès au texte intégral et bibtex
https://hal-onera.archives-ouvertes.fr/hal-02272135/file/ERTS_2014_submission_60.pdf BibTex

2013

Conference papers

titre
Towards an Updatable Strategy Logic
auteur
Christophe Chareton, Julien Brunel, David Chemouil
article
1st International Workshop on Strategic Reasoning, Mar 2013, Rome, France. pp.91 - 98, ⟨10.4204/EPTCS.112.14⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00796962/file/main.pdf BibTex

2012

Conference papers

titre
Une vue sûreté de fonctionnement pour la vérification d'architectures abstraites
auteur
Maria Piriquito, Pierre Bieber, Julien Brunel, David Chemouil
article
Conférence francophone sur les architectures logicielles, 2012, Montpellier, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00785494/file/cal2012.pdf BibTex
titre
Vers une sémantique des jeux pour un langage d'ingénierie des exigences par buts et agents
auteur
Christophe Chareton, Julien Brunel, David Chemouil
article
Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2012, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00782773/file/main.pdf BibTex

2011

Conference papers

titre
A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic
auteur
Christophe Chareton, Julien Brunel, David Chemouil
article
14th Brazilian Symposium, SBMF 2011, Sep 2011, São Paulo, Brazil. pp.188-203, ⟨10.1007/978-3-642-25032-3_13⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00783715/file/main.pdf BibTex
titre
Towards a categorical framework to ensure correct software evolutions
auteur
Sylvain Bouveret, Julien Brunel, David Chemouil, Fabien Dagnat
article
Workshop on Hot Topics in Software Upgrades, Apr 2011, Hannover, Germany. pp.139-144, ⟨10.1109/ICDEW.2011.5767625⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00785433/file/main.pdf BibTex

2008

Journal articles

titre
An insertion operator preserving infinite reduction sequences
auteur
David Chemouil
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2008, 18 (4), pp.693-728. ⟨10.1017/S0960129508006816⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00782799/file/v-hal.pdf BibTex

Conference papers

titre
Modes in Asynchronous Systems
auteur
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Dave Thomas
article
13th IEEE International Conference on Engineering of Complex Computer Systems, 2008, Belfast, Ireland. pp.282 - 287, ⟨10.1109/ICECCS.2008.28⟩
Accès au bibtex
BibTex

2007

Conference papers

titre
The AADL behaviour annex -- experiments and roadmap
auteur
Ricardo Bedin França, Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Jean-François Rolland, Dave Thomas
article
International Conference on Engineering Complex Computer Systems, 2007, Auckland, New Zealand. pp.377-382, ⟨10.1109/ICECCS.2007.41⟩
Accès au bibtex
BibTex
titre
A mapping from AADL to Java-RTSJ
auteur
Jean-Paul Bodeveix, Raphaël Cavallero, David Chemouil, Mamoun Filali, Jean-François Rolland
article
5th international workshop on Java technologies for real-time and embedded systems, 2007, Austria. pp.165-174, ⟨10.1145/1288940.1288965⟩
Accès au bibtex
BibTex
titre
The Design of Spacecraft On-Board Software
auteur
David Chemouil
article
B 2007, 2007, Besançon, France. pp.3
Accès au bibtex
BibTex

2006

Conference papers

titre
Towards the verification of model transformations
auteur
Jean-Paul Bodeveix, David Chemouil, M Filali, Nathalie Lalevee, M Strecker
article
Conference ERTS'06, Jan 2006, Toulouse, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02270435/file/5A1_M.Strecker_Feria.pdf BibTex

2005

Journal articles

titre
Isomorphisms of simple inductive types through extensional rewriting
auteur
David Chemouil
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2005, 15 (5), pp.875-915. ⟨10.1017/S0960129505004950⟩
Accès au bibtex
BibTex

Conference papers

titre
Towards formalising AADL in Proof Assistants
auteur
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker
article
Formal Foundations of Embedded Software and Component-based Software Architectures 2005, 2005, Edinburgh, United Kingdom. pp.153-169, ⟨10.1016/j.entcs.2005.05.008⟩
Accès au bibtex
BibTex

2003

Conference papers

titre
Remarks on isomorphisms of simple inductive types
auteur
David Chemouil, Sergei Soloviev
article
Mathematics, Logic and Computation (Satellite Event of ICALP 2003, in honor of N. G. de Bruijn's 85th birthday), Jun 2003, Eindhoven, Netherlands. pp.106-124, ⟨10.1016/S1571-0661(04)80760-6⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00783654/file/mlc2003.pdf BibTex
titre
Some Algebraic Structures in Lambda-Calculus with Inductive Types
auteur
Sergei Soloviev, David Chemouil
article
TYPES, Apr 2003, Italy. pp.338-354, ⟨10.1007/978-3-540-24849-1_22⟩
Accès au bibtex
BibTex