David Chemouil
Directeur de recherches ONERA DTIS
36
Documents
Site web
- http://www.onera.fr/staff/david-chemouil
Domaines de recherche
Logique en informatique [cs.LO]
Génie logiciel [cs.SE]
Publications
- 2
- 1
- 1
- 1
- 4
- 3
- 2
- 2
- 3
- 2
- 1
- 2
- 2
- 2
- 3
- 1
- 2
- 2
- 15
- 8
- 7
- 7
- 7
- 6
- 6
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 6
- 2
|
Pardinus: A temporal relational model finderJournal of Automated Reasoning, 2022, ⟨10.1007/s10817-022-09642-2⟩
Article dans une revue
hal-03738430v1
|
|
A Decidable and Expressive Fragment of Many-Sorted First-Order Linear Temporal LogicInformation and Computation, 2020, pp.104641. ⟨10.1016/j.ic.2020.104641⟩
Article dans une revue
hal-02976675v1
|
|
A Logic with Revocable and Refinable StrategiesInformation and Computation, 2015, 242, pp.157-182. ⟨10.1016/j.ic.2015.03.015⟩
Article dans une revue
hal-00785659v3
|
|
An insertion operator preserving infinite reduction sequencesMathematical Structures in Computer Science, 2008, 18 (4), pp.693-728. ⟨10.1017/S0960129508006816⟩
Article dans une revue
hal-00782799v1
|
Isomorphisms of simple inductive types through extensional rewritingMathematical Structures in Computer Science, 2005, 15 (5), pp.875-915. ⟨10.1017/S0960129505004950⟩
Article dans une revue
hal-00782793v1
|
Verifying temporal relational models with Pardinus9th international conference on rigorous state-based methods, May 2023, Nancy, France
Communication dans un congrès
hal-04074866v1
|
|
Adding records to Alloy9th international conference on rigorous state-based methods, May 2023, Nancy, France
Communication dans un congrès
hal-04074845v1
|
|
|
Sound Verification Procedures for Temporal Properties of Infinite-State Systems33rd International Conference on Computer-Aided Verification (CAV 2021), Jul 2021, Los Angeles (Online), United States
Communication dans un congrès
hal-03243129v2
|
|
A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic26th International Symposium on Temporal Representation and Reasoning (TIME 2019), Oct 2019, Málaga, Spain. ⟨10.4230/LIPIcs.TIME.2019.15⟩
Communication dans un congrès
hal-02332521v1
|
|
Simulation under arbitrary temporal logic constraints5th Workshop on Formal Integrated Development Environment, Oct 2019, Porto, Portugal
Communication dans un congrès
hal-02332517v1
|
|
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol23rd 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⟩
Communication dans un congrès
hal-02332531v1
|
|
Proposition of an Action Layer for Electrum6th 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⟩
Communication dans un congrès
hal-01774920v1
|
|
Analyzing the Fundamental Liveness Property of the Chord ProtocolFormal Methods in Computer-Aided Design, Oct 2018, Austin, United States
Communication dans un congrès
hal-01862755v1
|
|
The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications33rd ACM/IEEE International Conference on Automated Software Engineering (ASE ’18), Sep 2018, Montpellier, France. ⟨10.1145/3238147.3240475⟩
Communication dans un congrès
hal-01846951v2
|
|
Spécification légère et analyse de systèmes dynamiques munis de configurations richesApproches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
Communication dans un congrès
hal-02077323v1
|
|
Sur l’assignation de buts comportementaux à des coalitions d’agentsApproches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
Communication dans un congrès
hal-01863437v1
|
|
On Finite Domains in First-Order Linear Temporal Logic14th International Symposium on Automated Technology for Verification and Analysis, Oct 2016, Chiba, Japan. ⟨10.1007/978-3-319-46520-3_14⟩
Communication dans un congrès
hal-01343197v1
|
|
Lightweight Specification and Analysis of Dynamic Systems with Rich ConfigurationsFoundations of Software Engineering, Nov 2016, Seattle, United States. ⟨10.1145/2950290.2950318⟩
Communication dans un congrès
hal-01355062v1
|
|
Safety and Security Assessment of Behavioral Properties Using Alloy2nd International workshop on the Integration of Safety and Security Engineering, Sep 2015, Delft, Netherlands. ⟨10.1007/978-3-319-24249-1_22⟩
Communication dans un congrès
hal-01206638v1
|
|
Evaluating the Assignment of Behavioral Goals to Coalitions of AgentsBrazilian Symposium on Formal Methods, Sep 2015, Belo Horizonte, Brazil. ⟨10.1007/978-3-319-29473-5_4⟩
Communication dans un congrès
hal-01206625v1
|
|
A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures11th Workshop on Model-Driven Engineering, Verification and Validation, Sep 2014, Spain. pp.39-48
Communication dans un congrès
hal-01070960v1
|
|
Formal Modelling and Safety Analysis of an Avionic Functional Architecture with AlloyEmbedded real-time software and systems (ERTS² 2014), Feb 2014, TOULOUSE, France
Communication dans un congrès
hal-02272135v1
|
|
Towards an Updatable Strategy Logic1st International Workshop on Strategic Reasoning, Mar 2013, Rome, France. pp.91 - 98, ⟨10.4204/EPTCS.112.14⟩
Communication dans un congrès
hal-00796962v1
|
|
Vers une sémantique des jeux pour un langage d'ingénierie des exigences par buts et agentsApproches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2012, France
Communication dans un congrès
hal-00782773v1
|
|
Une vue sûreté de fonctionnement pour la vérification d'architectures abstraitesConférence francophone sur les architectures logicielles, 2012, Montpellier, France
Communication dans un congrès
hal-00785494v1
|
|
A Formal Treatment of Agents, Goals and Operations Using Alternating-Time Temporal Logic14th Brazilian Symposium, SBMF 2011, Sep 2011, São Paulo, Brazil. pp.188-203, ⟨10.1007/978-3-642-25032-3_13⟩
Communication dans un congrès
hal-00783715v1
|
|
Towards a categorical framework to ensure correct software evolutionsWorkshop on Hot Topics in Software Upgrades, Apr 2011, Hannover, Germany. pp.139-144, ⟨10.1109/ICDEW.2011.5767625⟩
Communication dans un congrès
hal-00785433v1
|
|
Modes in Asynchronous Systems13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008), Mar 2008, Belfast, Ireland. pp.282 - 287, ⟨10.1109/ICECCS.2008.28⟩
Communication dans un congrès
hal-00784986v1
|
The Design of Spacecraft On-Board SoftwareB 2007, 2007, Besançon, France. pp.3
Communication dans un congrès
hal-00784980v1
|
|
A mapping from AADL to Java-RTSJ5th international workshop on Java technologies for real-time and embedded systems, 2007, Vienne, Austria. pp.165-174, ⟨10.1145/1288940.1288965⟩
Communication dans un congrès
hal-00784968v1
|
|
The AADL behaviour annex -- experiments and roadmapInternational Conference on Engineering Complex Computer Systems, 2007, Auckland, New Zealand. pp.377-382, ⟨10.1109/ICECCS.2007.41⟩
Communication dans un congrès
hal-00784976v1
|
|
|
Towards the verification of model transformations3rd Conference on Embedded Real Time Software and Systems (ERTS 2006), Jan 2006, Toulouse, France
Communication dans un congrès
hal-02270435v1
|
Towards formalising AADL in Proof AssistantsFormal Foundations of Embedded Software and Component-based Software Architectures 2005, 2005, Edinburgh, United Kingdom. pp.153-169, ⟨10.1016/j.entcs.2005.05.008⟩
Communication dans un congrès
hal-00784959v1
|
|
|
Remarks on isomorphisms of simple inductive typesMathematics, Logic and Computation 2003 (Satellite Event of ICALP 2003), Jun 2003, Eindhoven, Netherlands. pp.106-124, ⟨10.1016/S1571-0661(04)80760-6⟩
Communication dans un congrès
hal-00783654v1
|
Some Algebraic Structures in Lambda-Calculus with Inductive TypesInternational Workshop on Types for Proofs and Programs (TYPES 2003), Apr 2003, Torino, Italy. pp.338-354, ⟨10.1007/978-3-540-24849-1_22⟩
Communication dans un congrès
hal-00782718v1
|