Publications HAL

2023

Conference papers

titre
Adding records to Alloy
auteur
Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo
article
9th international conference on rigorous state-based methods, May 2023, Nancy, France
Accès au bibtex
BibTex
titre
Verifying temporal relational models with Pardinus
auteur
Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo
article
9th international conference on rigorous state-based methods, May 2023, Nancy, France
Accès au bibtex
BibTex

2022

Journal articles

titre
Pardinus: A temporal relational model finder
auteur
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha
article
Journal of Automated Reasoning, 2022, ⟨10.1007/s10817-022-09642-2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03738430/file/main.pdf BibTex

2021

Conference papers

titre
Sound Verification Procedures for Temporal Properties of Infinite-State Systems
auteur
Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil
article
33rd International Conference on Computer-Aided Verification (CAV 2021), Jul 2021, Los Angeles (Online), United States
Accès au texte intégral et bibtex
https://hal.science/hal-03243129/file/main.pdf BibTex

2020

Journal articles

titre
A Decidable and Expressive Fragment of Many-Sorted First-Order Linear Temporal Logic
auteur
Quentin Peyras, Julien Brunel, David Chemouil
article
Information and Computation, 2020, pp.104641. ⟨10.1016/j.ic.2020.104641⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02976675/file/20201002-camera-ready.pdf BibTex

2019

Conference papers

titre
A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic
auteur
Quentin Peyras, Julien Brunel, David Chemouil
article
26th International Symposium on Temporal Representation and Reasoning (TIME 2019), Oct 2019, Málaga, Spain. ⟨10.4230/LIPIcs.TIME.2019.15⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02332521/file/reprint.pdf BibTex
titre
Simulation under arbitrary temporal logic constraints
auteur
Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo
article
5th Workshop on Formal Integrated Development Environment, Oct 2019, Porto, Portugal
Accès au texte intégral et bibtex
https://hal.science/hal-02332517/file/main.pdf BibTex
titre
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol
auteur
Jean-Paul Bodeveix, Julien Brunel, David Chemouil, M Filali
article
23rd International Symposium on Formal Methods (FM 2019), FME: Formal Methods Europe, Oct 2019, Porto, Portugal. pp.45-63, ⟨10.1007/978-3-030-30942-8_5⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02332531/file/final-fixed2.pdf BibTex

Books

titre
AFADL 2019 - Actes des 18e journées sur les Approches Formelles dans l’Assistance au Développement de Logiciels
auteur
David Chemouil, Thomas Lambolais
article
, 2019
Accès au bibtex
BibTex

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.science/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.science/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.science/hal-01774920/file/final.pdf BibTex

2017

Conference papers

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.science/hal-02077323/file/finale.pdf BibTex
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.science/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.science/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.science/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, 2015, 242, pp.157-182. ⟨10.1016/j.ic.2015.03.015⟩
Accès au texte intégral et bibtex
https://hal.science/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.science/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.science/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.science/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://onera.hal.science/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.science/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
Accès au texte intégral et bibtex
https://hal.science/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
Accès au texte intégral et bibtex
https://hal.science/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, ⟨10.1007/978-3-642-25032-3_13⟩
Accès au texte intégral et bibtex
https://hal.science/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.science/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, 2008, 18 (4), pp.693-728. ⟨10.1017/S0960129508006816⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00782799/file/v-hal.pdf BibTex

Conference papers

titre
Modes in Asynchronous Systems
auteur
Jean-François Rolland, Jean-Paul Bodeveix, M Filali, David Chemouil, Dave Thomas
article
13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008), Mar 2008, Belfast, Ireland. pp.282 - 287, ⟨10.1109/ICECCS.2008.28⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00784986/file/Modes%20in%20Asynchronous%20Systems.pdf BibTex

2007

Conference papers

titre
The AADL behaviour annex -- experiments and roadmap
auteur
Ricardo Bedin França, Jean-Paul Bodeveix, David Chemouil, M 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, M Filali, Jean-François Rolland
article
5th international workshop on Java technologies for real-time and embedded systems, 2007, Vienne, 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, Martin Strecker
article
3rd Conference on Embedded Real Time Software and Systems (ERTS 2006), Jan 2006, Toulouse, France
Accès au texte intégral et bibtex
https://hal.science/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, 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, M 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 2003 (Satellite Event of ICALP 2003), Jun 2003, Eindhoven, Netherlands. pp.106-124, ⟨10.1016/S1571-0661(04)80760-6⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00783654/file/mlc2003.pdf BibTex
titre
Some Algebraic Structures in Lambda-Calculus with Inductive Types
auteur
Sergei Soloviev, David Chemouil
article
International Workshop on Types for Proofs and Programs (TYPES 2003), Apr 2003, Torino, Italy. pp.338-354, ⟨10.1007/978-3-540-24849-1_22⟩
Accès au bibtex
BibTex