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. 〈https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/〉
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. ACM Press, 2018, Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering 〈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. 〈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

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. 1235, pp.39-48, 2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01070960/file/main.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. 112, pp.91 - 98, 2013, Proceedings 1st International Workshop on Strategic Reasoning: Preface. 〈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
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. 2012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00782773/file/main.pdf BibTex
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. 2012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00785494/file/cal2012.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, 2011, 〈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, 2011, 〈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, 2008, 〈10.1109/ICECCS.2008.28〉
Accès au bibtex
BibTex

2007

Conference papers

titre
A mapping from AADL to Java-RTSJ
auteur
Jean-Paul Bodeveix, Raphaël Cavallero, David Chemouil, Mamoun Filali, Jean-François Rolland
article
ACM. 5th international workshop on Java technologies for real-time and embedded systems, 2007, Austria. pp.165-174, 2007, 〈10.1145/1288940.1288965〉
Accès au bibtex
BibTex
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, 2007, 〈10.1109/ICECCS.2007.41〉
Accès au bibtex
BibTex
titre
The Design of Spacecraft On-Board Software
auteur
David Chemouil
article
B 2007, 2007, Besançon, France. 4355, pp.3, 2006
Accès au bibtex
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. 141 (3), pp.153-169, 2005, 〈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. 85 (7), pp.106-124, 2003, 〈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, 2004, 〈10.1007/978-3-540-24849-1_22〉
Accès au bibtex
BibTex