| 2025 |
S. Evangelista, L. Kristensen, L. Petrucci |
Algorithms and Evaluation of Distributed Explicit State Space Exploration with State Reconstruction for RDMA Networks |
|
| 2025 |
M. B. Dahlsen-Jensen, B. Fiévet, L. Petrucci, J. van de Pol |
Controller Synthesis for Parametric Timed Games |
|
| 2025 |
D. Catta, W. Penczek, L. Petrucci |
Formal Models are Magic |
|
| 2025 |
Y. Kim, W. Jamroga, W. Penczek, L. Petrucci |
Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems |
|
| 2025 |
W. Jamroga, M. Kwiatkowska, W. Penczek, L. Petrucci, T. Sidoruk |
Probabilistic Timed ATL |
|
| 2025 |
W. Penczek, L. Petrucci, T. Sidoruk |
Satisfiability Checking for (Strategic) Timed CTL Using IMITATOR |
|
| 2024 |
J. Arias, K. Bae, C. Olarte, P. Ölveczky, L. Petrucci |
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets |
|
| 2024 |
N. Amat, E. G. Amparore, B. Berthomieu, P. Bouvier, S. Dal Zilio, P. G. Jensen, L. Jezequel, F. Kordon, S. Li, E. Paviot-Adet, L. Petrucci, J. Srba, Y. Thierry-Mieg, K. Wolf |
Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023 |
|
| 2024 |
É. André, J. Arias, B. Barbot, F. Hulin-Hubard, F. Kordon, V.-F. Le, L. Petrucci |
CosyVerif: the Path to Formalisms Cohabitation |
|
| 2024 |
J. Arias, C. Olarte, W. Penczek, L. Petrucci, T. Sidoruk |
Model Checking and Synthesis for Strategic Timed CTL using Strategies in Rewriting Logics |
|
| 2024 |
M. B. Dahlsen-Jensen, B. Fiévet, L. Petrucci, J. van de Pol |
On-The-Fly Algorithm for Reachability in Parametric Timed Games |
|
| 2024 |
J. Arias, Lukasz Masko, C. Olarte, W. Penczek, L. Petrucci, T. Sidoruk |
Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models |
|
| 2024 |
Jörg Desel, Laure Petrucci |
Proceedings of the 1st International Workshop on Petri Net Games, Examples and Quizzes for Education, Contest and Fun (PENGE'24), Geneva, Switzerland |
|
| 2024 |
L. Bernardinello, J. Kleijn, Laure Petrucci |
Special Issue on Application and Theory of Petri Nets |
|
| 2024 |
J. Arias, K. Bae, C. Olarte, P. Ölveczky, L. Petrucci, F. R\omming |
Symbolic Analysis and Parameter Synthesis for Networks of Parametric Timed Automata with Global Variables using Maude and SMT Solving |
|
| 2024 |
V. chesneau, Laure Petrucci |
The Experience of an Interdisciplinary Course: Individual Presentation on the Internet |
|
| 2023 |
Carlos Olarte, Elaine Pimentel, Camilo Rocha |
A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems |
Lien
|
| 2023 |
Ruben Dobler Strand, Lars M Kristensen, Laure Petrucci |
Development and Verification of a Microservice Architecture for a Fire Risk Notification System |
|
| 2023 |
Étienne André, Engel Lefaucheux, Dylan Marinho |
Expiring opacity problems in parametric timed automata |
|
| 2023 |
Jaime Arias, Kyungmin Bae, Laure Petrucci, Carlos Olarte, Peter Ölveczky, Fredrik Rømming |
PITPN2Maude: Rewriting Logic Semantics for Parametric Time Petri Nets with Inhibitor Arcs |
Lien
|
| 2023 |
Laure Petrucci, Jeremy Sproston |
Proceedings of the 21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'23), Antwerp, Belgium |
|
| 2023 |
J. Arias, W. Jamroga, W. Penczek, L. Petrucci, T. Sidoruk |
Strategic (Timed) Computation Tree Logic |
|
| 2023 |
J. Arias, K. Bae, C. Olarte, P. Ölveczky, L. Petrucci, F. Rømming |
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving |
|
| 2023 |
Johan Arcile, Etienne André |
Timed Automata as a Formalism for Expressing Security: A Survey on Theory and Practice |
Lien
|
| 2023 |
Jaime Arias, Mohamed Taha Bennani, Jörg Desel, Kais Klai, Hanène Ochi |
sogMBT: Symbolic Observation Graph-Based Generation of Test Paths |
Lien
|
| 2022 |
Camille Coti, Laure Petrucci, Daniel Alberto Torres Gonzalez |
A Formal Model for Fault Tolerant Parallel Matrix Factorization |
|
| 2022 |
Bruno Xavier, Carlos Olarte, Elaine Pimentel |
A linear logic framework for multimodal logics |
|
| 2022 |
Jaime Arias, Łukasz Maśko, Carlos Olarte, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk |
ADT2Maude: A rewriting logic specification for modeling ADTree and solve the optimal scheduling problem |
Lien
|
| 2022 |
Nour Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed |
At Design-Time Approach for Supervisory Control of Opacity |
|
| 2022 |
Hanen Ochi, Kais Klai |
Checking Composition-Aware Service Substitutability |
|
| 2022 |
Jaime Arias, Laure Petrucci, Van-François Le |
CosyDraw: An Open Source Extensible Verification Environment |
Lien
|
| 2022 |
S. Evangelista, L.M. Kristensen, L. Petrucci |
Distributed Explicit State Space Exploration with State Reconstruction for RDMA Networks |
|
| 2022 |
Étienne André, Dylan Marinho, Laure Petrucci, Jaco van de Pol |
Efficient Convex Zone Merging in Parametric Timed Automata |
|
| 2022 |
Étienne André, Masaki Waga, Natsuki Urabe, Ichiro Hasuo |
Exemplifying parametric timed specifications over signals with bounded behavior |
Lien
|
| 2022 |
R. D. Strand, L. Kristensen, Laure Petrucci |
Formal Specification and Validation of a Data-driven Software System for Fire Risk Prediction |
Lien
|
| 2022 |
Étienne André, Didier Lime, Dylan Marinho, Jun Sun |
Guaranteeing Timed Opacity using Parametric Timed Model Checking |
Lien
|
| 2022 |
Kais Klai, Chiheb Ameur Abid, Jaime Arias, Sami Evangelista |
Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation |
Lien
|
| 2022 |
Nour Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed |
Hyper Symbolic Observation Graph to Enforce Opacity of Discrete Event Systems using Supervisory Control |
|
| 2022 |
Carlos Olarte, Elaine Pimentel, Camilo Rocha |
L-Framework |
Lien
|
| 2022 |
J. Arias, {\L} Ma{\' s}ko, W. Penczek, L. Petrucci, T. Sidoruk |
Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees |
|
| 2022 |
Ikram Garfatta, Ka\"{i}s Klai, Mohamed Gra\"{i}et, Walid Gaaloul |
Model checking of vulnerabilities in smart contracts: a solidity-to-CPN approach |
|
| 2022 |
Masaki Waga, Étienne André, Ichiro Hasuo |
Model-Bounded Monitoring of Hybrid Systems |
|
| 2022 |
J. Arias, M. Knapik, W. Penczek, L. Petrucci |
Modular Analysis of Tree-Topology Models |
|
| 2022 |
Bineet Ghosh, Étienne André |
Monitoring of scattered uncertain logs using uncertain linear dynamical systems |
Lien
|
| 2022 |
Nour Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed |
Optimal Supervisory Control of Opacity for Modular Systems |
|
| 2022 |
Jaime Arias, Kyungmin Bae, Laure Petrucci, Carlos Olarte, Peter Ölveczky, Fredrik Rømming |
PTA2Maude: Rewriting Logic Semantics for Parametric Timed Automata |
Lien
|
| 2022 |
Masaki Waga, Étienne André, Ichiro Hasuo |
Parametric Timed Pattern Matching |
|
| 2022 |
L. Bernardinello, L. Petrucci |
Proceedings of the 43rd International Conference on Petri Nets and other Models of Concurrency (PetriNets'22), Bergen, Norway |
|
| 2022 |
Étienne André, Didier Lime, Olivier H. Roux |
Reachability and liveness in parametric timed automata |
Lien
|
| 2022 |
J. Arias, K. Bae, C. Olarte, P. \"Olveczky, L. Petrucci, F. Rømming |
Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata |
|
| 2022 |
Johan Arcile, Étienne André |
Zone extrapolations in parametric timed automata |
|
| 2022 |
Sylvie Boldo, François Clément, Martin Vincent, Micaela Mayero, Florian Faissole, Houda Mouhcine, Louise Leclerc, Stephane Aubry |
coq-num-analysis opam package (Numerical Analysis in Coq) |
Lien
|
| 2022 |
Étienne André, Shapagat Bolat, Engel Lefaucheux, Dylan Marinho |
strategFTO: Untimed control for timed opacity |
Lien
|
| 2021 |
Étienne André, Dylan Marinho, Jaco van de Pol |
A Benchmarks Library for Extended Timed Automata |
|
| 2021 |
Étienne André |
A Benchmarks Library for Extended Timed Automata |
Lien
|
| 2021 |
Guillaume Rosinosky, Samir Youcef, François Charoy, Etienne Rivière |
A Methodology for Tenant Migration in Legacy Shared-Table Multi-tenant Applications |
Lien
|
| 2021 |
Nour Souid, Kais Klai |
A Novel Approach for Supervisor Synthesis to Enforce Opacity of Discrete Event Systems |
|
| 2021 |
Ikram Garfatta, Ka\"{i}s Klai, Mohamed Gra\"{i}et, Walid Gaaloul |
A Solidity-to-CPN Approach Towards Formal Verification of Smart Contracts |
|
| 2021 |
Ikram Garfatta, Kais Klai, Walid Gaaloul, Mohamed Graiet |
A Survey on Formal Verification for Solidity Smart Contracts |
|
| 2021 |
Amy Felty, Carlos Olarte, Bruno Xavier |
A focused linear logical framework and its application to metatheory of object logics |
Lien
|
| 2021 |
Abderraouf Boussif, Mohamed Ghazel, Kais Klai |
A semi-symbolic diagnoser for fault diagnosis of bounded labeled petri nets |
Lien
|
| 2021 |
Daniele Nantes, Carlos Olarte, Daniel Ventura |
A subexponential view of domains in session types |
Lien
|
| 2021 |
J. Arias, W. Penczek, L. Petrucci, T. Sidoruk |
ADT2AMAS: Managing Agents in Attack-Defence Scenarios |
|
| 2021 |
Jawher Jerray, Laurent Fribourg, Étienne André |
An Approximation of Minimax Control using Random Sampling and Symbolic Computation |
Lien
|
| 2021 |
Jaime Arias, Benoît Barbot, Francis Hulin-hubard, Fabrice Kordon, Laure Petrucci |
CosyVerif: an online verification platform |
Lien
|
| 2021 |
Étienne André, Hoang Gia Nguyen, Laure Petrucci, Jun Sun |
Distributed parametric model checking timed automata under non-Zenoness assumption |
Lien
|
| 2021 |
Camille Coti, Laure Petrucci, Daniel Alberto Torres Gonzalez |
Fault-tolerant LU factorisation is low cost |
|
| 2021 |
Rania Ben Halima, Kais Klai, Mohamed Sellami, Zakaria Maamar |
Formal Modeling and Verification of Property-based Resource Consumption Cycles |
|
| 2021 |
Étienne André |
IMITATOR 3: Synthesis of timing parameters beyond decidability |
|
| 2021 |
Étienne André, Jaime Arias, Laure Petrucci |
IMITATOR: Tool for Parametric Verification and Robustness Analysis of Real-Time Systems with Parameter |
Lien
|
| 2021 |
Étienne André, Jaime Arias, Laure Petrucci, Jaco van de Pol |
Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata |
Lien
|
| 2021 |
Ikram Garfatta, Ka\"{i}s Klai, Mohamed Gra\"{i}et, Walid Gaaloul |
Model Checking of Solidity Smart Contracts Adopted for Business Processes |
|
| 2021 |
Masaki Waga, Étienne André, Ichiro Hasuo |
Model-bounded monitoring of hybrid systems |
|
| 2021 |
J. van de Pol, L. Petrucci |
On Completeness of Liveness Synthesis for Parametric Timed Automata |
|
| 2021 |
Étienne André, Didier Lime, Mathias Ramparison, Mariëlle Stoelinga |
Parametric analyses of attack-fault trees |
|
| 2021 |
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray, David Lesens |
Parametric schedulability analysis of a launcher flight control system under reactivity constraints |
|
| 2021 |
Étienne André, Didier Lime, Mathias Ramparison |
Parametric updates in parametric timed automata |
Lien
|
| 2021 |
Elaine Pimentel, Carlos Olarte, Vivek Nigam |
Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk) |
Lien
|
| 2021 |
Camille Coti, Laure Petrucci, Cesar Rodriguez, Marcelo Sousa |
Quasi-Optimal Partial Order Reduction |
|
| 2021 |
Jawher Jerray, Laurent Fribourg, \'Etienne Andr\'e |
Robust optimal periodic control using guaranteed Euler's method |
|
| 2021 |
Jaime Arias, Ikram Garfatta, Kais Klai |
Solidity2CPN: Formal Verification of Solidity Smart Contracts using Coloured Petri Nets |
Lien
|
| 2021 |
Jaime Arias, Laure Petrucci |
Web user interface for IMITATOR |
Lien
|
| 2020 |
Chiheb Ameur Abid, Jaime Arias, Kais Klai |
PMC-SOG: Parallel Model Checking using the Symbolic Observation Graph |
Lien
|
| 2020 |
Linda Brodo, Carlos Olarte |
A Constraint-based Language for Multiparty Interactions |
Lien
|
| 2020 |
Carlos Olarte, Elaine Pimentel, Bruno Xavier |
A Fresh View of Linear Logic as a Logical Framework |
Lien
|
| 2020 |
Sérgio Queiroz, Carlos Olarte |
A semantic framework for PEGs |
Lien
|
| 2020 |
Jaime Arias, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk |
ADT2AMAS: Managing Agents in Attack-Defence Scenarios |
Lien
|
| 2020 |
Étienne André, Tian Huat Tan, Manman Chen, Shuang Liu, Jun Sun, Yang Liu, Jin Song Dong |
Automated Synthesis of Local Time Requirement for Service Composition |
|
| 2020 |
Ikram Garfatta, Ka\"{i}s Klai, Mahamed Gra\"{i}et, Walid Gaaloul |
Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach |
|
| 2020 |
Étienne André, Benoît Delahaye, Paulin Fournier |
Consistency in Parametric Interval Probabilistic Timed Automata |
|
| 2020 |
Moreno Falaschi, Maurizio Gabbrielli, Carlos Olarte, Catuscia Palamidessi |
Dynamic Slicing for Concurrent Constraint Languages |
Lien
|
| 2020 |
Jawher Jerray, Laurent Fribourg, Étienne André |
Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method (verification challenge) |
Lien
|
| 2020 |
Jaime Arias, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, Marielle Stoelinga |
Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems |
|
| 2020 |
Étienne André, Didier Lime, Nicolas Markey |
Language Preservation Problems in Parametric Timed Automata |
Lien
|
| 2020 |
Étienne André, Aleksander Kryukov |
Parametric non-interference in timed automata |
|
| 2020 |
Chiheb Ameur Abid, Kais Klai, Jaime Arias, Hiba Ouni |
SOG-Based Multi-Core LTL Model Checking |
Lien
|
| 2020 |
Daniel Schemmel, Julian Büning, Cesar Rodriguez, David Laprell, Klaus Wehrle |
Symbolic Partial-Order Execution for Testing Multi-Threaded Programs |
Lien
|
| 2020 |
Linda Brodo, Carlos Olarte |
Verification Techniques for a Network Algebra |
Lien
|
| 2019 |
Timo Lang, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller |
A Game Model for Proofs with Costs |
Lien
|
| 2019 |
Amina Ahmed Nacer, Claude Godart, Guillaume Rosinosky, Abdelkamel Tari, Samir Youcef |
Business process outsourcing to the cloud: Balancing costs with security risks |
Lien
|
| 2019 |
C. Coti, L. Petrucci, Daniel Alberto Torres Gonzalez |
Fault-tolerant matrix factorisation: a formal model and proof |
|
| 2019 |
Rakesh Jain, Kais Klai, Samir Tata |
Formal Modeling and Verification of Scalable Process-Aware Distributed IoT Applications |
|
| 2019 |
Étienne André |
Formalizing Time4sys using parametric timed automata |
|
| 2019 |
Kaustuv Chaudhuri, Joëlle Despeyroux, Carlos Olarte, Elaine Pimentel |
Hybrid linear logic, revisited |
Lien
|
| 2019 |
Amina Bourouis, Kais Klai, Nejib Ben |
Measuring Opacity for Non-Probabilistic DES: a SOG-Based Approach |
|
| 2019 |
Étienne André, Vincent Bloemen, Laure Petrucci, Jaco van de Pol |
Minimal-Time Synthesis for Parametric Timed Automata |
|
| 2019 |
Étienne André, Didier Lime, Mathias Ramparison |
On the expressive power of invariants in parametric timed automata |
|
| 2019 |
Masaki Waga, Étienne André |
Online Parametric Timed Pattern Matching with Automata-Based Skipping |
|
| 2019 |
Hiba Ouni, Kais Klai, Belhassen Zouari |
Parallel construction of the Symbolic Observation Graph |
|
| 2019 |
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray, David Lesens |
Parametric Schedulability Analysis of a Launcher Flight Control System Under Reactivity Constraints |
|
| 2019 |
Étienne André, Benoît Delahaye, Paulin Fournier, Didier Lime |
Parametric Timed Broadcast Protocols |
|
| 2019 |
Étienne André, Jun Sun |
Parametric Timed Model Checking for Guaranteeing Timed Opacity |
|
| 2019 |
Étienne André, M Knapik, D Lime, W Penczek, L Petrucci |
Parametric Verification: An Introduction |
|
| 2019 |
Étienne André, Didier Lime, Mathias Ramparison, Mariëlle Stoelinga |
Parametric analyses of attack-fault trees |
|
| 2019 |
Étienne André, Didier Lime, Mathias Ramparison |
Parametric updates in parametric timed automata |
|
| 2019 |
C. Coti, L. Petrucci, Daniel Alberto Torres Gonzalez |
Process scheduling on volatile nodes for fault-tolerant linear algebra |
|
| 2019 |
L. Petrucci, J. van de Pol |
Pruning NDFS for Parametric Timed Automata |
|
| 2019 |
Étienne André, Paolo Arcaini, Angelo Gargantini, Marco Radavelli |
Repairing Timed Automata Clock Guards through Abstraction and Testing |
|
| 2019 |
M. Knapik, W. Penczek, L. Petrucci, T. Sidoruk |
Squeezing State Spaces of (Attack-Defence) Trees |
|
| 2019 |
Masaki Waga, Étienne André, Ichiro Hasuo |
Symbolic Monitoring against Specifications Parametric in Time and Data |
|
| 2019 |
L. Petrucci, J. van de Pol |
Taming NDFS for Parametric Timed Automata |
|
| 2019 |
Étienne André, Mariëlle Stoelinga |
The 17th International Conference Formal Modeling and Analysis of Timed Systems (FORMATS 2019), Amsterdam, The Netherlands, August 27-29, 2019 |
Lien
|
| 2019 |
Étienne André, Jawher Jerray, Sahar Mhiri |
Time4sys2imi: A tool to formalize real-time system models under uncertainty |
|
| 2019 |
Michal Jozef Knapik, Étienne André, L Petrucci, W Jamroga, W Penczek |
Timed ATL: Forget Memory, Just Count |
Lien
|
| 2019 |
Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari |
Towards Parallel Verification of Concurrent Systems Using the Symbolic Observation Graph |
|
| 2019 |
Étienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat |
Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking |
|
| 2019 |
Étienne André |
What's decidable about parametric timed automata? |
|
| 2018 |
Étienne André |
A Benchmark Library for Parametric Timed Model Checking |
|
| 2018 |
Amina r Ahmed Nace, Elio Goettelmann, Samir Youcef, Abdelkamel Tari, Claude Godart |
A Design-Time Semi-Automatic Approach for Obfuscating a Business Process Model in a Trusted Multi-Cloud Deployment: A Design-Time Approach for BP Obfuscation |
Lien
|
| 2018 |
Souha Boubaker, Kais Klai, Hedi Kortas, Walid Gaaloul |
A Formal Model for Business Process Configuration Verification Supporting OR-Join Semantics |
|
| 2018 |
Guillaume Rosinosky, Samir Youcef, François Charoy |
A Genetic Algorithm for Cost-Aware Business Processes Execution in the Cloud |
Lien
|
| 2018 |
Joëlle Despeyroux, Amy P., Pietro Liò, Carlos Olarte |
A Logical Framework for Modelling Breast Cancer Progression |
Lien
|
| 2018 |
Carlos Olarte, Elaine Pimentel, Camilo Rueda |
A concurrent constraint programming interpretation of access permissions |
Lien
|
| 2018 |
Moreno Falaschi, Carlos Olarte |
An Assertion Language for Slicing Constraint Logic Languages |
Lien
|
| 2018 |
Étienne André |
Contributions to parametric timed model checking: Theory and algorithms |
|
| 2018 |
Dhriti Khanna, Subodh Sharma, Cesar Rodriguez, Rahul Purandare |
Dynamic Symbolic Verification of MPI Programs |
Lien
|
| 2018 |
Guillaume Rosinosky, Chahrazed Labba, Vincenzo Ferme, Samir Youcef, François Charoy, Cesare Pautasso |
Evaluating Multi-tenant Live Migrations Effects on Performance |
Lien
|
| 2018 |
Abderraouf Boussif, Mohamed Ghazel, Kais Klai |
Fault Diagnosis of Discrete-Event systems Based on the Symbolic Observation Graph |
|
| 2018 |
Ikram Garfatta, Kais Klai, Mohamed Graiet, Walid Gaaloul |
Formal Modelling and Verification of Cloud Resource Allocation in Business Processes |
|
| 2018 |
H. G. Nguyen, L. Petrucci, J. van de Pol |
Layered and Collecting NDFS with Subsumption for Parametric Timed Automata |
|
| 2018 |
Étienne André, Ichiro Hasuo, Masaki Waga |
Offline Timed Pattern Matching under Uncertainty |
|
| 2018 |
C. Coti, S. Evangelista, L. Petrucci |
One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters |
|
| 2018 |
J Barnat, V Bloemen, A Duret-Lutz, A Laarman, L Petrucci, J van de Pol, E Renault |
Parallel Model Checking Algorithms for Linear-Time Temporal Logic |
Lien
|
| 2018 |
L. Petrucci, J. van de Pol |
Parameter Synthesis Algorithms for Parametric Interval Markov Chains |
|
| 2018 |
Carlos Olarte, Elaine Pimentel, Camilo Rocha |
Proving Structural Properties of Sequent Systems in Rewriting Logic |
Lien
|
| 2018 |
Thi Thanh Huyen Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti, Laure Petrucci |
Quasi-Optimal Partial Order Reduction |
|
| 2018 |
Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari |
Reducing Time and/or Memory Consumption of The SOG construction in a Parallel Context |
|
| 2018 |
Mauricio Cano, Jaime Arias, Jorge A. Pérez |
Refined Encodings of Sessions in ReactiveML |
|
| 2018 |
C Choppy, J Desel, L Petrucci |
Specialisation and Generalisation of Processes |
Lien
|
| 2018 |
C. Coti, S. Evangelista, L. Petrucci |
State Compression Based on One-Sided Communications for Distributed Model Checking |
|
| 2018 |
Étienne André, Didier Lime, Mathias Ramparison |
TCTL model checking lower/upper-bound parametric timed automata without invariants |
|
| 2018 |
Carlos Olarte, Valeria de, Elaine Pimentel, Giselle Reis |
The ILLTP Library for Intuitionistic Linear Logic |
Lien
|
| 2018 |
Étienne André, Shang-Wei Lin |
The language preservation problem is undecidable for parametric event-recording automata |
|
| 2018 |
Jaime Arias, Raphaël Marczak, Myriam Desainte-Catherine |
Timed Automata for Video Games and Interaction |
|
| 2018 |
Étienne André, Didier Lime, Mathias Ramparison |
Timed automata with parametric updates |
|
| 2018 |
Étienne André, Giuseppe Lipari |
Tutorial on Schedulability Analysis under Uncertainty using Formal Methods |
Lien
|
| 2018 |
Ikram Garfatta, Kais Klai, Mohamed Graiet, Walid Gaaloul |
[WiP] Formal Modelling of IT Resource Allocation in Business Processes |
|
| 2017 |
Amina Ahmed Nacer, Claude Godart, Samir Youcef, Abdelkamel Tari |
A Metric for Evaluating the Privacy Level of a Business Process Logic in a Multi-cloud Deployment |
Lien
|
| 2017 |
Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari |
A Parallel Construction of the Symbolic Observation Graph: the Basis for Efficient Model Checking of Concurrent Systems |
|
| 2017 |
Étienne André |
A Unified Formalism for Monoprocessor Schedulability Analysis under Uncertainty |
|
| 2017 |
Marcelo Sousa, César Rodriguez, Vijay D'Silva, Daniel Kroening |
Abstract Interpretation with Unfoldings |
|
| 2017 |
Jiaying Li, Jun Sun, Bo Gao, Étienne André |
Classification based Parameter Synthesis for Parametric Timed Automata |
|
| 2017 |
Amina Burouis, Nejib Ben, Kais Klai |
Computing Quantified Opacity for SOG-Abstracted Web Services |
|
| 2017 |
Abderraouf Boussif, Mohamed Ghazel, Kais Klai |
DPN-SOG: A Software Tool for Fault Diagnosis of Labeled Petri Nets Using the Semi-Symbolic Diagnoser |
|
| 2017 |
Souha Boubaker, Kais Klai, Katia Schmitz, Mohamed Graiet, Walid Gaaloul |
Deadlock-Freeness Verification of Business Process Configuration Using SOG |
|
| 2017 |
Guillaume Rosinosky, Samir Youcef, François Charoy |
Efficient Migration-Aware Algorithms for Elastic BPMaaS |
Lien
|
| 2017 |
Étienne André, Hoang Gia Nguyen, Laure Petrucci |
Efficient parameter synthesis using optimized state exploration strategies |
|
| 2017 |
Samir Tata, Kais Klai, Rakesh Jain |
Formal Model and Method to Decompose Process-Aware IoT Applications |
|
| 2017 |
Etienne André |
IMITATOR Web page |
Lien
|
| 2017 |
Étienne André, Shang-Wei Lin |
Learning-based compositional parameter synthesis for event-recording automata |
|
| 2017 |
Étienne André, Didier Lime |
Liveness in L/U-Parametric Timed Automata |
|
| 2017 |
Amina Bourouis, Kais Klai, Nejib Ben |
Measuring opacity in web services |
|
| 2017 |
Amina Bourouis, Kais Klai, Nejib Ben Hadj{-}Alouane, Yamen El Touati |
On the Verification of Opacity in Web Services and Their Composition |
|
| 2017 |
Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari |
Parallel Symbolic Observation Graph |
|
| 2017 |
Étienne André, D. Lime, W. Penczek, L. Petrucci |
Parametric Verification |
Lien
|
| 2017 |
Étienne André, Hoang Gia Nguyen, Laure Petrucci, Jun Sun |
Parametric model checking timed automata under non-Zenoness assumption |
|
| 2017 |
Étienne André, Thomas Chatain, Cesar Rodriguez |
Preserving Partial-Order Runs in Parametric Time Petri Nets |
Lien
|
| 2017 |
Jaime Arias, Philippe Ciuciu, Michel Dojat, Florence Forbes, Aina Frau-Pascual, Thomas Perret, Jan M. Warnking |
PyHRF: A Python Library for the Analysis of fMRI Data Based on Local Estimation of Hemodynamic Response Function |
|
| 2017 |
Mauricio Cano, Jaime Arias, Jorge A. Pérez |
Session-based Concurrency, Reactively |
|
| 2017 |
Laure Petrucci, Cristina Seceleanu, Ana Cavalcanti |
The Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20, 2017 |
|
| 2017 |
Étienne André, W. Jamroga, M. Knapik, W. Penczek, Laure Petrucci |
Timed ATL: Forget Memory, Just Count |
|
| 2017 |
Thi Thanh Huyen Nguyen, César Rodríguez, Camille Coti |
Tool DPU |
Lien
|
| 2017 |
Mohamed Graiet, Kais Klai |
Track Report for Formal Verification of Service Based Systems: FVSBS 2017 |
Lien
|
| 2016 |
Kais Klai, Hanen Ochi |
A Formal Approach for Service Composition in a Cloud Resources Sharing Context |
|
| 2016 |
K. Le, T. Bui, T. Quan, L. Petrucci |
A Framework for Fast Congestion Detection in Wireless Sensor Networks Using Clustering and Petri Net-based Verification |
|
| 2016 |
Jaime Arias, Mauricio Cano, Jorge A Pérez |
A Reactive Interpretation of Session-Based Concurrency |
Lien
|
| 2016 |
Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier H. Roux, Didier Lime, Etienne André |
Applying parametric model-checking techniques for reusing real-time critical systems |
|
| 2016 |
Jaime Arias, Jean-Michaël Celerier, Myriam Desiante-Catherine |
Authoring and Automatic Verification of Interactive Multimedia Scores |
|
| 2016 |
Jaime Arias, Myriam Desainte-Catherine, Shlomo Dubnov |
Automatic Construction of Interactive Machine Improvisation Scenarios from Audio Recordings |
|
| 2016 |
K. Le, T. Bui, T. Quan, L. Petrucci |
COCA: Congestion-Oriented Clustering Algorithm for Wireless Sensor Networks |
|
| 2016 |
K. Le, T. Bui, T. Quan, L. Petrucci, E. André |
Congestion Verification on Abstracted Wireless Sensor Networks with WSN-PN Tool |
|
| 2016 |
Etienne André, Benoit Delahaye |
Consistency in Parametric Interval Probabilistic Timed Automata |
|
| 2016 |
E. André, M. Knapik, W. Penczek, L. Petrucci |
Controlling Actions and Time in Parametric Timed Automata |
|
| 2016 |
Etienne André, Didier Lime, Olivier H. Roux |
Decision Problems for Parametric Timed Automata |
|
| 2016 |
Rania Ben Halima, Slim Kallel, Kais Klai, Walid Gaaloul, Mohamed Jmaiel |
Formal Verification of Time-Aware Cloud Resource Allocation in Business Process |
|
| 2016 |
Etienne André, Mohamed Mahdi Benmoussa, Christine Choppy |
Formalising concurrent UML state machines using coloured Petri nets |
Lien
|
| 2016 |
Camille Coti, Charles Lakos, Laure Petrucci |
Formally Proving and Enhancing a Self-Stabilising Algorithm |
|
| 2016 |
Simon Archipoff, Jaime Arias, Edwin Buger, David Janin |
Interpolations : Écriture de Contraintes Réactives pour Improvisations Pianistiques |
|
| 2016 |
Fabrice Kordon, Hubert Garavel, Lom-Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, César Rodríguez, Francis Hulin-Hubard |
MCC'2015 - The Fifth Model Checking Contest 64 Petri Nets 2015 |
|
| 2016 |
Kais Klai, Hanen Ochi |
Model Checking of Composite Cloud Services |
|
| 2016 |
Etienne André, Didier Lime, Olivier H. Roux |
On the Expressiveness of Parametric Timed Automata |
|
| 2016 |
Tian Huat Tan, Manman Chen, Jun Sun, Yang Liu, Etienne André, Jin Song Dong, Yinxing Xue |
Optimizing Selection of Competing Services with Probabilistic Hierarchical Refinement |
|
| 2016 |
B. Delahaye, D. Lime, L. Petrucci |
Parameter Synthesis for Parametric Interval Markov Chains |
|
| 2016 |
Etienne André |
Parametric Deadlock-Freeness Checking Timed Automata |
|
| 2016 |
L. Petrucci, J. van de Pol |
Parametric Interval Markov Chains: Synthesis Revisited |
|
| 2016 |
E. André, D. Lime, W. Penczek, L. Petrucci |
Parametric Verification |
Lien
|
| 2016 |
Etienne André, Thomas Chatain, César Rodríguez |
Preserving Partial Order Runs in Parametric Time Petri Nets |
|
| 2016 |
Jaime Arias, Mauricio Cano, Jorge A Pérez |
Towards a Practical Model of Reactive Communication-Centric Software |
Lien
|
| 2016 |
Etienne André |
What's decidable about parametric timed automata? |
|
| 2015 |
Etienne André, Goran Frehse |
2nd International Workshop on the Synthesis of Complex Parameters (SynCoP 2015), London, UK |
Lien
|
| 2015 |
Kais Klai, Hanen Ochi |
A Bottom-Up Approach to Check the Correctness of Interorganisational Workflows |
|
| 2015 |
Jaime Arias, Myriam Desainte-Catherine, Camilo Rueda |
A Framework for Composition, Verification and Real-Time Performance of Multimedia Interactive Scenarios |
|
| 2015 |
Gianna Reggio, Egidio Astesiano, Christine Choppy |
A Framework for Defining and Comparing Modelling Methods |
Lien
|
| 2015 |
Jaime Arias, Michell Gúzman, Carlos Olarte |
A Symbolic Model for Timed Concurrent Constraint Programming |
|
| 2015 |
H Ochi |
Abstraction and Modular Verification of Inter-Enterprise Business Processes |
|
| 2015 |
Amina Bourouis, Kais Klai, Yamen El Touati, Nejib Ben Hadj-Alouane |
Checking Opacity of Vulnerable Critical Systems On-The-Fly |
|
| 2015 |
Abderraouf Boussif, Mohamed Ghazel, Kais Klai |
Combining Enumerative and Symbolic - Techniques for Diagnosis of Discrete-Event Systems |
|
| 2015 |
Khanh Le, Thang Bui, Tho Quan, Laure Petrucci, étienne André |
Component-Based Abstraction of Petri Net Models: An Application for Congestion Verification of Wireless Sensor Networks |
|
| 2015 |
K. Le, T. Bui, T. Quan, L. Petrucci, E. André |
Congestion Verification on Abstracted Wireless Sensor Networks with WSN-PN Tool |
|
| 2015 |
E. André, L. Petrucci |
Decrypting Cryptography |
|
| 2015 |
Étienne André, Camille Coti, Hoang Gia Nguyen |
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata |
Lien
|
| 2015 |
Jaime Arias, Myriam Desainte-Catherine, Camilo Rueda |
Exploiting Parallelism in FPGAs for the Real-Time Interpretation of Interactive Multimedia Scores |
Lien
|
| 2015 |
Jaime Arias |
Formal Semantics and Automatic Verification of Hierarchical Multimedia Scenarios with Interactive Choices. (Sémantique Formelle et Vérification Automatique de Scénarios Hiérarchiques Multimédia avec des Choix Interactifs) |
Lien
|
| 2015 |
Jaime Arias, Myriam Desainte-Catherine, Carlos Olarte, Camilo Rueda |
Foundations for Reliable and Flexible Interactive Multimedia Scores |
|
| 2015 |
S Baarir, F Kordon, L Petrucci |
From Symmetric Nets to Symmetric Nets with Bags |
Lien
|
| 2015 |
Etienne André, Giuseppe Lipari, Youcheng Sun |
IMITATOR: Formal Verification of Real-Time Systems Under Uncertainty |
Lien
|
| 2015 |
Etienne André, Didier Lime, Olivier H. Roux |
Integer-Complete Synthesis for Bounded Parametric Timed Automata |
|
| 2015 |
Kais Klai, Hanen Ochi |
LTL Model Cheking of Service-Based Business Processes in the Cloud |
|
| 2015 |
Etienne André, Nicolas Markey |
Language Preservation Problems in Parametric Timed Automata |
|
| 2015 |
Jaime Arias, Jean-Michaël Celerier |
Le Séquenceur Interactif Multimédia i-score |
Lien
|
| 2015 |
Amina Bourouis, Kais Klai, Yamen El Touati, Nejib Ben Hadj-Alouane |
Opacity Preserving Abstraction for Web Services and Their Composition Using SOGs |
|
| 2015 |
Hernán Ponce de León, César Rodríguez, Josep Carmona |
POD - A Tool For Process Discovery Using Partial Orders and Independence Information |
|
| 2015 |
Étienne André, Thomas Chatain, César Rodríguez |
Preserving Partial Order Runs in Parametric Time Petri Nets |
|
| 2015 |
Camille Coti, Sami Evangelista, Kais Klai |
Queuless, Uncentralized Resource Discovery: Formal Specification and Verification |
|
| 2015 |
Etienne André, Giuseppe Lipari, Hoang Gia Nguyen, Youcheng Sun |
Reachability Preservation Based Parameter Synthesis for Timed Automata |
|
| 2015 |
Camille Coti, Sami Evangelista, Kais Klai |
Time Petri Net Models for a New Queueless and Uncentralized Resource Discovery System |
|
| 2015 |
Kais Klai |
Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets |
|
| 2015 |
César Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening |
Unfolding-based Partial Order Reduction |
|
| 2015 |
Hernan Ponce de León, César Rodríguez, Josep Carmona, Stefan Haar, Keijo Heljanko |
Unfolding-based Process Discovery |
|
| 2015 |
E. André, L. Petrucci |
Unifying Patterns for Modelling Timed Relationships in Systems and Properties |
Lien
|
| 2015 |
Etienne André, Giuseppe Lipari, Youcheng Sun |
Verification of Two Real-Time Systems Using Parametric Timed Automata |
|
| 2014 |
Sami Evangelista, Lars M Kristensen |
A Sweep-Line Method for Büchi Automata-based Model Checking |
|
| 2014 |
Kais Klai, Nawel Hamdi, Nejib Ben Hadj-Alouane |
An On-the-Fly Approach for the Verification of Opacity in Critical Systems |
|
| 2014 |
Tian Huat Tan, Manman Chen, Étienne André, Jun Sun, Yang Liu, Jin Song Dong |
Automated Runtime Recovery for QoS-based Service Composition |
Lien
|
| 2014 |
E. André, B. Delahaye, P. Habermehl, C. Jard, D. Lime, L. Petrucci, O.H. Roux, T. Touili |
Beyond Model-Checking: Parameters Everywhere |
|
| 2014 |
Sami Yangui, Kais Klai, Samir Tata |
Deployment of Service-Based Processes in the Cloud Using Petri Net Decomposition |
|
| 2014 |
Etienne André, Camille Coti, Sami Evangelista |
Distributed Behavioral Cartography of Timed Automata |
Lien
|
| 2014 |
Jaime Arias, Myriam Desainte-Catherine, Sylvain Salvati, Camilo Rueda |
Executing Hierarchical Interactive Scores in ReactiveML |
Lien
|
| 2014 |
Etienne André, Mohamed Mahdi Benmoussa, Christine Choppy |
Formalising Concurrent UML State Machines Using Coloured Petri Nets |
Lien
|
| 2014 |
S Baarir, F Kordon, L Petrucci |
From Symmetric Nets to Symmetric Nets with Bags |
Lien
|
| 2014 |
Etienne André, Laure Petrucci |
La cryptographie décryptée |
Lien
|
| 2014 |
Shang-Wei Lin, Etienne André, Yang Liu, Jun Sun, Jin Song Dong |
Learning Assumptions for Compositional Verification of Timed Systems |
Lien
|
| 2014 |
Jaime Arias, Myriam Desainte-Catherine, Camilo Rueda |
Modelling Data Processing for Interactive Scores Using Coloured Petri Nets |
|
| 2014 |
Etienne André, Christine Choppy, Thierry Noulamo |
Modelling Timed Concurrent Systems Using Activity Diagram Patterns |
Lien
|
| 2014 |
E. Viennet, L. Petrucci |
Monitoring Students Performances in French Institutes of Technology using the ScoDoc Software |
|
| 2014 |
D. Genon-Catalot, L. Petrucci, M. Tabouret |
Nationwide Industrial Cooperation for Long-Life Learning and Apprenticeships |
|
| 2014 |
Kais Klai |
On-The-Fly Model Checking of Timed Properties on Time Petri Nets |
|
| 2014 |
Azadeh Alebrahim, Christine Choppy, Stephan Faêssbender, Maritta Heisel |
Optimizing functional and quality requirements according to stakeholders' goals |
Lien
|
| 2014 |
Etienne André, Yang Liu, Jun Sun, Jin Song Dong |
Parameter Synthesis for Hierarchical Concurrent Real-Time Systems |
Lien
|
| 2014 |
Dinh-Thuan Le, Huu-Vu Nguyen, Van-Tinh Nguyen, Phuong-Nam Mai, Thanh-Tho Quan, Etienne André, Laure Petrucci, Yang Liu |
PeCAn: Compositional Verification of Petri Nets Made Easy |
Lien
|
| 2014 |
Etienne André, Fabrice Kordon, Laure Petrucci |
Teaching formal methods: Experience at UPMC and UP13 with CosyVerif |
Lien
|
| 2014 |
Giuseppe Lipari, Youcheng Sun, Étienne André, Laurent Fribourg |
Toward Parametric Timed Interfaces for Real-Time Components |
Lien
|
| 2014 |
Étienne André, Mohamed Mahdi Benmoussa, Christine Choppy |
Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report |
Lien
|
| 2013 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
A Formal Coloured Petri Net Model for Hazard Detection in Large Event Flows |
|
| 2013 |
Shuang Liu, Yang Liu, Etienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa, Jin Song Dong |
A Formal Semantics for the Complete Syntax of UML State Machines with Communications |
Lien
|
| 2013 |
E André, B Barbot, C Démoulins, L Hillah, F Hulin-Hubard, F Kordon, A Linard, L Petrucci |
A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems |
Lien
|
| 2013 |
K Klai, N Aber, L Petrucci |
A New Approach To Abstract Reachability State Space of Time Petri Nets |
|
| 2013 |
Kais Klai, Naim Aber, Laure Petrucci |
A New Approach to Abstract Reachability State Space of Time Petri Nets |
|
| 2013 |
Étienne André, Christine Choppy, Gianna Reggio |
Activity Diagrams Patterns for Modeling Business Processes |
Lien
|
| 2013 |
Etienne André, Laurent Fribourg, Jeremy Sproston |
An Extension of the Inverse Method to Probabilistic Timed Automata |
Lien
|
| 2013 |
César Rodríguez, Stefan Schwoon |
An Improved Construction of Petri Net Unfoldings |
|
| 2013 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
Behaviour recognition for complex systems |
|
| 2013 |
Kais Klai, Hanen Ochi |
Checking Compatibility of Web Services Behaviorally |
|
| 2013 |
C. Choppy, L. Petrucci, A. Sanogo |
Coloured Petri Nets Refinements |
Lien
|
| 2013 |
César Rodríguez, Stefan Schwoon, Victor Khomenko |
Contextual Merged Processes |
|
| 2013 |
E. André, L. Hillah, F. Hulin-Hubard, F. Kordon, Y. Lembachar, A. Linard, L. Petrucci |
CosyVerif: An Open Source Extensible Verification Environment |
Lien
|
| 2013 |
César Rodríguez, Stefan Schwoon |
Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs |
|
| 2013 |
Etienne André |
Dynamic Clock Elimination in Parametric Timed Automata |
Lien
|
| 2013 |
Sami Evangelista, Lars M Kristensen |
Dynamic State Space Partitioning for External Memory State Space Exploration |
|
| 2013 |
Tian Huat Tan, Etienne André, Jun Sun, Yang Liu, Jin Song Dong, Manman Chen |
Dynamic Synthesis of Local Time Requirement for Service Composition |
Lien
|
| 2013 |
Kais Klai, Hanen Ochi, Samir Tata |
Formal Abstraction and Compatibility Checking of Web Services |
|
| 2013 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
Formal Behaviour Detection for Distributed Simulations |
|
| 2013 |
Kais Klai, Samir Tata |
Formal Modeling of Elastic Service-based Business Processes |
|
| 2013 |
Etienne André, Mohamed Mahdi Benmoussa, Christine Choppy |
Formalisation des diagrammes états-transitions UML concurrents |
Lien
|
| 2013 |
A Dedova, L Petrucci |
From Code to Coloured Petri Nets: Modelling Guidelines |
|
| 2013 |
Kais Klai |
Hybrid techniques for the verification of complex systems : abstraction and composition-based approach |
|
| 2013 |
Fabrice Kordon, Alban Linard, Marco Beccuti, Didier Buchs, Lukasz Fronc, Lom-Messan Hillah, Francis Hulin-Hubard, Fabrice Legond-Aubry, Niels Lohmann, Alexis Marechal, Emmanuel Paviot-Adet, Franck Pommereau, César Rodríguez, Christian Rohr, Yann Thierry-M |
MCC'2013 - The 3rd Model Checking Contest 64 Petri Nets 2013 |
|
| 2013 |
Etienne André, Laurent Fribourg, Romain Soulat |
Merge and Conquer: State Merging in Parametric Timed Automata |
Lien
|
| 2013 |
Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Etienne André |
Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP |
|
| 2013 |
S Evangelista, L M Kristensen, L Petrucci |
Multi-threaded Explicit State Space Exploration with State Reconstruction |
|
| 2013 |
Etienne André |
Observer Patterns for Real-Time Systems |
Lien
|
| 2013 |
Etienne André, Yang Liu, Jun Sun, Jin Song Dong, Shang-Wei Lin |
PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems |
Lien
|
| 2013 |
Youcheng Sun, Romain Soulat, Giuseppe Lipari, Étienne André, Laurent Fribourg |
Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems |
Lien
|
| 2013 |
E. André, G. Pellegrino, L. Petrucci |
Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs |
Lien
|
| 2013 |
D. Genon-Catalot, L. Petrucci, M. Tabouret |
Professional Experience Validation Process at a National Level |
|
| 2013 |
Stefan Haar, César Rodríguez, Stefan Schwoon |
Reveal Your Faults: It's Only Fair! |
|
| 2013 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
Safety of unmanned aircraft systems facing multiple breakdowns |
|
| 2013 |
Etienne André, Romain Soulat |
The Inverse Method |
|
| 2013 |
Mourad Amziani, Kais Klai, Tarek Melliti, Samir Tata |
Time-Based Evaluation of Service-Based Business Process Elasticity in the Cloud |
|
| 2013 |
César Rodríguez |
Verification Based on Unfoldings of Petri Nets with Read Arcs |
|
| 2013 |
K Klai, N Aber, L Petrucci |
Verification of Reachability Properties for Time Petri Nets |
|
| 2013 |
K Klai, N Aber, L Petrucci |
Verification of Reachability Properties for Time {Petri} Nets |
|
| 2012 |
Etienne André, Hanen Ochi, Kais Klai, Laure Petrucci |
A Counterexample-Based Incremental and Modular Verification Approach |
Lien
|
| 2012 |
E Andr?and K Klai, H Ochi, L Petrucci |
A Counterexample-Based Incremental and Modular Verification Approach |
|
| 2012 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
A Formal Behaviour Representation for the Analysis of Distributed Simulations of Unmanned Aircraft Systems |
|
| 2012 |
Etienne André, Laurent Fribourg, Jeremy Sproston |
An~Extension of the Inverse Method to Probabilistic Timed Automata |
Lien
|
| 2012 |
Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong, Etienne André |
Automatic Compositional Verification of Timed Systems |
Lien
|
| 2012 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
Behavioural analysis for distributed simulations |
|
| 2012 |
Christine Choppy, Gianna Reggio |
CASL-MDL, modelling dynamic system with a formal foundation and a UML-like notation |
|
| 2012 |
C Choppy, G Reggio |
CASL-MDL, modelling dynamic systems with a formal foundation and a UML-like notation |
|
| 2012 |
Kais Klai, Hanen Ochi |
Checking Compatibility of Web Services Using SOGs |
|
| 2012 |
Kais Klai, Jörg Desel |
Checking Soundness of Business Processes Compositionally Using Symbolic Observation Graphs |
|
| 2012 |
Sami Evangelista, Lars Michael Kristensen |
Combining the Sweep-Line Method with the use of an External-memory Priority Queue |
|
| 2012 |
Sami Evangelista, Lars M Kristensen |
Combining the Sweep-Line Method with the use of an External-memory Priority Queue |
|
| 2012 |
Leila Abidi, Christophe Cérin, Kais Klai |
Design, Verification and Prototyping the Next Generation of Desktop Grid Middleware |
|
| 2012 |
Leila Abidi, Christophe Cérin, Kais Klai |
Design, Verification and Prototyping the Next Generation of Desktop Grid Middleware |
|
| 2012 |
Leila Abidi, Christophe Cérin, Kais Klai |
Design, Verification and Prototyping the Next Generation of Desktop Grid Middleware |
|
| 2012 |
Azadeh Alebrahim, Isabelle Côté, Maritta Heisel, Christine Choppy, Denis Hatebur |
Designing architectures from problem descriptions by interactive model transformation |
|
| 2012 |
P Carle, C Choppy, R Kervarc |
Detecting behaviours within HLA distributed simulations with added analysis components. |
|
| 2012 |
C Boukala, L Petrucci |
Distributed CTL Model-Checking and counterexample search |
|
| 2012 |
S Evangelista, L M Kristensen |
Dynamic State Space Partitioning for External Memory State Space Exploration |
|
| 2012 |
Paolo Baldan, Alessandro Bruni, Andrea Corradini, Barbara König, César Rodríguez, Stefan Schwoon |
Efficient unfolding of contextual Petri nets |
|
| 2012 |
Etienne André, Laurent Fribourg, Romain Soulat |
Enhancing the Inverse Method with State Merging |
Lien
|
| 2012 |
C Choppy, G Reggio, D Hatebur, M Heisel |
Enterprise Applications: From Requirements to Design |
|
| 2012 |
L Hillah, C Lakos, F Kordon, L Petrucci |
Extending PNML Scope: a Framework to Combine Petri Nets Types |
|
| 2012 |
Christine Choppy, Gianna Reggio, Khanh-Dung Tran |
Formal or Not, but Precise Modelling of Services with CASL4SOA and SoaML |
|
| 2012 |
Etienne André, Christine Choppy, Kais Klai |
Formalizing Non-Concurrent UML State Machines Using Colored Petri Nets |
Lien
|
| 2012 |
Étienne André, Christine Choppy, Kais Klai |
Formalizing non-concurrent UML state machines using colored Petri nets |
|
| 2012 |
A Dedova, L Petrucci |
From Code to Coloured Petri Nets: Modelling Guidelines |
|
| 2012 |
Kais Klai, Samir Tata, Hanen Ochi |
Generic and Specific Compatibility Criteria for Web Service Composition: Formal Abstraction and Modular Verification Approach |
|
| 2012 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel |
Handling Breakdowns in Unmanned Aircraft Systems |
|
| 2012 |
Sami Evangelista, Lars M Kristensen |
Hybrid On-the-Fly Model Checking with the Sweep-line Method |
|
| 2012 |
Sami Evangelista, Lars M Kristensen |
Hybrid On-the-Fly Model Checking with the Sweep-line Method |
|
| 2012 |
Etienne André, Laurent Fribourg, Ulrich Kühne, Romain Soulat |
IMITATOR~2.5: A~Tool for Analyzing Robustness in Scheduling Problems |
Lien
|
| 2012 |
Etienne André |
Imitator~II |
Lien
|
| 2012 |
S. Evangelista, A. Laarman, L. Petrucci, J. van de Pol |
Improved Multi-Core Nested Depth-First Search |
|
| 2012 |
Jaime Arias |
Model Checking for TCC Calculus |
Lien
|
| 2012 |
Jun Sun, Jin-Song Dong, Yan Liu, Shi Ling, Etienne André |
Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP |
|
| 2012 |
C Choppy, A Dedova, S Evangelista, K Klai, L Petrucci, S Youcef |
Modelling and formal verification of the NEO protocol |
|
| 2012 |
K Klai, H Ochi |
Modular verification of inter-enterprise Business Processes |
|
| 2012 |
Kais Klai, Hanen Ochi |
Modular verification of inter-enterprise Business Processes |
|
| 2012 |
Etienne André, Yang Liu, Jun Sun, Jin Song Dong |
Parameter Synthesis for Hierarchical Concurrent Real-Time Systems |
Lien
|
| 2012 |
Etienne André, Ulrich Kühne |
Parametric Analysis of Hybrid Systems Using HyMITATOR |
Lien
|
| 2012 |
Patrice Carle, Christine Choppy, Romain Kervarc, Ariane Piel, Claude Le Tallec |
Pilot's Information Understanding for Traffic Situation Awareness and Avoidance Manoeuvre Decision |
|
| 2012 |
Etienne André, Shweta Garg |
Robustness Analysis of Time Petri Nets |
|
| 2012 |
C Choppy, L Petrucci |
Specification and Design Approaches |
|
| 2012 |
César Rodríguez, Stefan Schwoon |
Verification of Petri Nets with Read Arcs |
|
| 2011 |
L Abidi, C Cérin, S Evangelista |
A Petri-Net Model for the Publish-Subscribe Paradigm and its Application for the Verification of the Bonjourgrid Middleware |
|
| 2011 |
Shang-Wei Lin, Etienne André, Jin Song Dong, Jun Sun, Yang Liu |
An Efficient Algorithm for Learning Event-Recording Automata |
Lien
|
| 2011 |
Shang-Wei Lin, Etienne André, Jin Song Dong, Jun Sun, Yang Liu |
An Efficient Algorithm for Learning Event-Recording Automata |
|
| 2011 |
P Carle, C Choppy, R Kervarc |
Behaviour recognition using chronicles |
|
| 2011 |
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg |
Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking |
|
| 2011 |
Etienne André, Abdelrezzak Bara, Pirouz Bazargan-Sabet, Rémy Chevallier, Dominique Le Dû, Emmanuelle Encrenaz, Laurent Fribourg, Patricia Renault |
Compte-rendu de fin du projet ANR VALMEM |
Lien
|
| 2011 |
Stefan Schwoon, César Rodríguez |
Construction and SAT-based verification of Contextual Unfoldings |
|
| 2011 |
S Haddad, F Kordon, L Pautet, L Petrucci |
Distributed Systems: Design and Algorithms |
Lien
|
| 2011 |
C Boukala, L Petrucci |
Distributed Verification of Modular Systems |
Lien
|
| 2011 |
César Rodríguez, Stefan Schwoon, Paolo Baldan |
Efficient contextual unfolding |
|
| 2011 |
L Hillah, C Lakos, F Kordon, L Petrucci |
Extending PNML Scope: the Prioritised Petri Nets Experience |
Lien
|
| 2011 |
Christine Choppy, Kais Klai, Hacene Zidani |
Formal verification of UML state diagrams: a Petri net based approach |
|
| 2011 |
L Petrucci |
Introduction to Formal Models |
|
| 2011 |
L Petrucci |
Introduction to Security Issues in Distributed Systems |
|
| 2011 |
S Haddad, F Kordon, L Pautet, L Petrucci |
Models and Analysis in Distributed Systems |
Lien
|
| 2011 |
C Lakos, L Petrucci |
Modular State Spaces for Prioritised Petri nets |
|
| 2011 |
S Evangelista, L Petrucci, S Youcef |
Parallel Nested Depth-First Searches for LTL Model Checking |
|
| 2011 |
Kais Klai, Walid Gaaloul |
Petri Net Modeling and Verification of Transactional Workflows |
|
| 2011 |
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg |
Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking |
|
| 2011 |
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg |
Self-Loop Aggregation Product -- A New Hybrid Approach to On-the-Fly LTL Model Checking |
|
| 2011 |
C Choppy, J Desel, L Petrucci |
Specialisation and Generalisation of Processes |
Lien
|
| 2011 |
C Choppy, L Petrucci |
Specification and Design Approaches |
|
| 2011 |
Kais Klai, Samir Tata, Jörg Desel |
Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes |
|
| 2011 |
Etienne André, Romain Soulat |
Synthesis of Timing Parameters Satisfying Safety Properties |
Lien
|
| 2011 |
Etienne André, Romain Soulat |
Synthesis of Timing Parameters Satisfying Safety Properties (full version) |
Lien
|
| 2011 |
C Choppy, D Hatebur, M Heisel |
Systematic Architectural Design based on Problem Patterns |
|
| 2010 |
Etienne André |
An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems |
Lien
|
| 2010 |
Etienne André, Laurent Fribourg |
Behavioral Cartography of Timed Automata |
Lien
|
| 2010 |
R Kervarc, P Carle, C Choppy |
Chronicles : a temporal logic framework for the study of large simulations |
|
| 2010 |
C Choppy, M Mayero, L Petrucci |
Coloured Petri net refinement specification and correctness proof with Coq |
|
| 2010 |
Etienne André, Abdelrezzak Bara, Pirouz Bazargan-Sabet, Rémy Chevallier, Dominique Le Dû, Emmanuelle Encrenaz, Laurent Fribourg, Patricia Renault |
Experiments of Prototype Tools on Case Studies, Comparison of obtained results and Conclusion |
Lien
|
| 2010 |
K. van Hee, L. M. Kristensen, L. Petrucci |
Guidelines for Application Papers submitted to PETRI NETS |
|
| 2010 |
Etienne André |
IMITATOR~II User Manual |
Lien
|
| 2010 |
Etienne André |
IMITATOR~II: A~Tool for Solving the Good Parameters Problem in Timed Automata |
Lien
|
| 2010 |
C Lakos, L Petrucci |
Modular State Spaces for Prioritised Petri nets |
|
| 2010 |
L Hillah, F Kordon, L Petrucci, N Trèves |
PNML Framework: an extendable reference implementation of the Petri Net Markup Language |
|
| 2010 |
S Evangelista, L M Kristensen |
Search-Order Independent State Caching |
|
| 2010 |
C Choppy, G Reggio |
Service Modelling with Casl4Soa: A Well-Founded Approach - Part 1 (Service in isolation) |
|
| 2010 |
S Evangelista, C Pajault |
Solving the Ignoring Problem for Partial Order Reduction |
|
| 2010 |
L Hillah, L Petrucci |
Standardisation des r?eaux de Petri : ?at de l'art et enjeux futurs |
|
| 2010 |
Etienne André |
Synthesizing Parametric Constraints on Various Case Studies Using IMITATOR~II |
Lien
|
| 2010 |
C Choppy, A Dedova, S Evangelista, S Hong, K Klai, L Petrucci |
The NEO Protocol for Large-Scale Distributed Database Systems: Modelling and Initial Verification |
|
| 2009 |
F Bonnefoi, C Choppy, F Kordon |
A Discretization Method from Coloured to Symmetric Nets: Application to an Industrial Example |
|
| 2009 |
E Kindler, L Petrucci |
A framework for the definition of variants of high-level Petri nets |
|
| 2009 |
L Hillah, E Kindler, F Kordon, L Petrucci, N Trèves |
A primer on the Petri Net Markup Language and ISO/IEC 15909-2 |
|
| 2009 |
M Westergaard, S Evangelista, Lars M Kristensen |
ASAP: An Extensible Platform for State Space Analysis |
|
| 2009 |
Etienne André, Laurent Fribourg, Jeremy Sproston |
An Extension of the Inverse Method to Probabilistic Timed Automata |
Lien
|
| 2009 |
Etienne André, _ Thomas Chatain, Emmanuelle Encrenaz, Laurent Fribourg |
An Inverse Method for Parametric Timed Automata |
Lien
|
| 2009 |
Etienne André, Laurent Fribourg |
An Inverse Method for Policy-Iteration Based Algorithms |
Lien
|
| 2009 |
C Choppy, M Mayero, L Petrucci |
Coloured Petri net refinement and correctness proof with Coq |
|
| 2009 |
C Boukala, L Petrucci |
Distributed CTL Model-Checking and counterexample search |
|
| 2009 |
S Evangelista, L M Kristensen |
Dynamic State Space Partitioning for External Memory Model Checking |
|
| 2009 |
S Haddad, F Kordon, L Petrucci, J F Pradat-Peyre, N Trèves |
Efficient state-based analysis by introducing bags in Petri nets colour domains |
|
| 2009 |
Etienne André |
Everything You Always Wanted to Know About IMITATOR (But~Were Afraid to~Ask) |
Lien
|
| 2009 |
Etienne André |
IMITATOR: A~Tool for Synthesizing Constraints on Timing Bounds of Timed Automata |
Lien
|
| 2009 |
Kais Klai, Samir Tata, Jörg Desel |
Symbolic Abstraction and Deadlock-Freeness Verification of Inter-enterprise Processes |
|
| 2009 |
Etienne André, Emmanuelle Encrenaz, Laurent Fribourg |
Synthesizing Parametric Constraints on Various Case Studies Using IMITATOR |
Lien
|
| 2009 |
Etienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg, Silvain Ruel |
Synthèse de contraintes temporisées pour une architecture d'automatisation en réseau |
Lien
|
| 2009 |
S Evangelista, M Westergaard, L M Kristensen |
The ComBack Method Revisited: Caching Strategies and Extension with Delayed Duplicate Detection |
|
| 2009 |
E Kindler, L Petrucci |
Towards a Standard for Modular Petri Nets: A Formalisation |
|
| 2009 |
Etienne André |
Une méthode inverse pour les plus courts chemins |
Lien
|
| 2009 |
O Bertrand, A Calonne, C Choppy, S Hong, K Klai, F Kordon, Y Okuji, E Paviot-Adet, L Petrucci, J -P Smets |
Verification of large-scale distributed database systems in the NEOPPOD project |
|
| 2008 |
F Bonnefoi, C Choppy, F Kordon |
A Discretization Method from Coloured to Symmetric Nets: Application to an Industrial Example |
|
| 2008 |
C Choppy, L Petrucci, G Reggio |
A modelling approach with coloured Petri nets |
|
| 2008 |
J Desel, L Petrucci |
Aggregating views for Petri net model construction |
|
| 2008 |
Etienne André, _ Thomas Chatain, Emmanuelle Encrenaz, Laurent Fribourg |
An Inverse Method for Parametric Timed Automata |
Lien
|
| 2008 |
L Hillah, F Kordon, L Petrucci |
Application des méthodes formelles à la robotique modulaire --- Méthodes formelles pour l'analyse des robots autonomes et modulaires |
|
| 2008 |
A Hamez, L Hillah, K Klai, F Kordon, L Petrucci, D Poitrenaud, Y Thierry-Mieg |
CoSyVerif: Complex Systems Verification |
|
| 2008 |
Samir Tata, Kais Klai, Nomane Ould Ahmed M'Bareck |
CoopFlow: A Bottom-Up Approach to Workflow Cooperation for Short-Term Virtual Enterprises |
|
| 2008 |
H Karoui, R Kanawati, L Petrucci |
Cooperative CBR System for Peer Agent Committee Formation |
|
| 2008 |
S Evangelista |
Dynamic Delayed Duplicate Detection for External Memory Model Checking |
|
| 2008 |
Pablo Parra, Aitor Viana, Martín Knoblauch, César Rodríguez, Óscar Polo, Sebastián Sánchez |
Evaluation of a Minimal POSIX Tracing Service Profile for Real Time Embedded Systems |
|
| 2008 |
C Choppy, M Mayero, L Petrucci |
Experimenting Formal Proofs of Petri Nets Refinements |
|
| 2008 |
S Bardin, A Finkel, J Leroux, L Petrucci |
FAST: Acceleration from theory to practice |
|
| 2008 |
L Petrucci |
Introduction ?la s?urit?dans les syst?es r?artis |
|
| 2008 |
Kais Klai, Denis Poitrenaud |
MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs |
|
| 2008 |
Kais Klai, Denis Poitrenaud |
MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs |
|
| 2008 |
K Klai, L Petrucci |
Modular Construction of the Symbolic Observation Graph |
|
| 2008 |
E Badouel, P Darondeau, L Petrucci |
Modular Synthesis of Petri Nets from Regular Languages |
|
| 2008 |
O Bertrand, P Carle, C Choppy |
Reusing simulation through processing tools |
|
| 2008 |
F Kordon, L Pautet, L Petrucci |
Systèmes répartis en action : de l'embarqué aux systèmes large échelle |
Lien
|
| 2008 |
O Bertrand, P Carle, C Choppy |
Towards a coloured Petri nets semantics of a chronicle language for distributed simulation processing |
|
| 2007 |
S Evangelista, C Pajault, J -F Pradat-Peyre |
A Simple Positive Flows Computation Algorithm for a Large Subclass of Colored Nets |
|
| 2007 |
F Kordon, L Petrucci |
A formal approach to designing autonomous systems: from Intelligent Transport Systems to Robots |
|
| 2007 |
K Klai, L Petrucci, M Reniers |
An Incremental and Modular Technique for Checking LTL$êsetminus$X Properties of Petri Nets |
|
| 2007 |
O Bertrand, P Carle, C Choppy |
Chronicle modelling using automata and colored Petri nets |
|
| 2007 |
C Choppy, L Petrucci, G Reggio |
Designing coloured Petri net models: a method |
|
| 2007 |
S Bardin, A Finkel, J Leroux, L Petrucci |
FAST: Acceleration from theory to practice |
Lien
|
| 2007 |
Etienne André |
Handling Theories in Logic Functors for Recomposing Description Logics |
Lien
|
| 2007 |
L Petrucci |
ISO/IEC 15909 --- Part 3: Extensions |
|
| 2007 |
L Petrucci |
ISO/IEC 15909-2, concepts of high-level nets and CPN |
|
| 2007 |
P Darondeau, L Petrucci |
Modular Automata 2 Distributed Petri Nets 4 Synthesis |
Lien
|
| 2007 |
K Klai, L Petrucci |
Modular Construction of the Symbolic Observation Graph |
|
| 2007 |
C Lakos, L Petrucci |
Modular State Space Exploration for Timed Petri Nets |
|
| 2007 |
C Lakos, L Petrucci |
Modular State Spaces and Place Fusion |
|
| 2007 |
S Evangelista, C Pajault |
Some Solutions to the Ignoring Problem |
|
| 2007 |
C Boukala, L Petrucci |
Towards Distributed Verification of Petri Nets properties |
|
| 2007 |
O Bertrand, P Carle, C Choppy |
Vers une exploitation des simulations distribuées par les chroniques |
|
| 2006 |
Kais Klai, Samir Tata, Issam Chebbi |
An Observation-based Algorithm for Workflow Matching |
|
| 2006 |
Kais Klai, Samir Tata, Issam Chebbi |
An Observation-based Algorithm for Workflow Matching |
|
| 2006 |
H Karoui, R Kanawati, L Petrucci |
An intelligent peer-to-peer multi-agent system for collaborative management of bibliographic databases |
|
| 2006 |
Kais Klai, Nomane Ould Ahmed M'Bareck, Samir Tata |
Behavioral Technique for Workflow Abstraction and Matching |
|
| 2006 |
Kais Klai, Nomane Ould Ahmed M'Bareck, Samir Tata |
Behavioral Technique for Workflow Abstraction and Matching |
|
| 2006 |
H Karoui, R Kanawati, L Petrucci |
COBRAS: Cooperative CBR System for Bibliographical Reference Recommendation |
|
| 2006 |
H Karoui, R Kanawati, L Petrucci |
Cooperative CBR System for Peer Agent Committee Formation |
|
| 2006 |
C Choppy, L Petrucci |
Démarches de spécification |
|
| 2006 |
S Mazouz, L Petrucci |
Modular Discrete Pseudo-State Graphs for Time Petri Nets |
|
| 2006 |
S Haddad, F Kordon, L Petrucci |
Méthodes formelles pour les systèmes répartis et coopératifs |
Lien
|
| 2006 |
L Hillah, F Kordon, L Petrucci, N Trèves |
PN standardisation: a survey |
|
| 2006 |
L Petrucci |
Panorama des modèles et langages de spécification |
|
| 2006 |
F Kordon, L Petrucci |
Toward Formal Methods Oecumenism? |
|
| 2006 |
C Choppy, S Haddad, H Klaudel, F Kordon, L Petrucci, Y Thierry-Mieg |
Tutorial on Formal Methods for Distributed and Cooperative Systems |
|
| 2006 |
H Karoui, R Kanawati, L Petrucci |
Une approche R?C pour la formation d'un comité d'agents dans un système de recommandation d'?al-??al |
|
| 2006 |
Kais Klai, Samir Tata, Issam Chebbi |
Workflow interconnection using symbolic observation graph |
|
| 2005 |
Kais Klai, Samir Tata |
Abstraction-based Workflow Cooperation Using Petri Net Theory |
|
| 2005 |
Kais Klai, Samir Tata |
Abstraction-basedWorkflow Cooperation Using Petri Net Theory |
|
| 2005 |
L Petrucci |
Cover Picture Story: Experiments with Modular State Spaces |
|
| 2005 |
C Lakos, L Petrucci |
Distributed and Modular State Space Exploration for Timed Petri Nets |
|
| 2005 |
J Billington, G E Gallasch, L Petrucci |
FAST Verification of the Class of Stop-and-Wait Protocols Modelled by Coloured Petri Nets |
|
| 2005 |
S Bardin, A Finkel, J Leroux, L Petrucci |
FAST: Fast Acceleration of Symbolic Transition systems |
|
| 2005 |
Kais Klai, Serge Haddad, Jean-Michel Ilié |
Modular Verification of Petri Nets Properties: A Structure-Based Approach |
|
| 2005 |
Kais Klai, Serge Haddad, Jean-Michel Ilié |
Modular Verification of Petri Nets Properties: A Structure-Based Approach |
|
| 2005 |
L Petrucci |
Modularity and Petri nets |
|
| 2005 |
Kamel Barkaoui, Jean-Michel Couvreur, Kais Klai |
On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets |
|
| 2005 |
Kamel Barkaoui, Jean-Michel Couvreur, Kais Klai |
On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets |
|
| 2005 |
J Billington, G E Gallasch, L Petrucci |
Transforming Couloured Petri Nets to Counter Systems for Parametric Verification: A Stop-and-Wait Protocol Case Study |
|
| 2004 |
L Kristensen, L Petrucci |
An Approach to Distributed State Space Exploration for Coloured Petri Nets |
|
| 2004 |
S Bardin, L Petrucci |
COAST : des réseaux de Petri à la planification assistée |
|
| 2004 |
Serge Haddad, Jean-Michel Ilié, Kais Klai |
Design and Evaluation of a Symbolic and Abstraction-Based Model Checker |
|
| 2004 |
Serge Haddad, Jean-Michel Ilié, Kais Klai |
Design and Evaluation of a Symbolic and Abstraction-Based Model Checker |
|
| 2004 |
S Bardin, L Petrucci |
From PNML to counter systems for accelerating Petri Nets with Fast |
|
| 2004 |
C Lakos, L Petrucci |
Modular Analysis of Systems Composed of Semiautonomous Subsystems |
|
| 2004 |
F Kordon, L Petrucci |
Proposal for an addendum to ISO/IEC 15909-1 |
|
| 2004 |
Serge Haddad, Jean-Michel Ilié, Kais Klai |
Symbolic observation graph: An efficient structure for on-the-fly action-based linear time logic model checking |
|
| 2004 |
C Choppy, L Petrucci |
Towards a methodology for modelling with Petri nets |
|
| 2003 |
Jean-michel Ilie, Kais Klai, Belhassen Zouari |
A modular verification methodology for D-NRI Petri nets |
|
| 2003 |
Jean-Michel Ilié, Kais Klai, Belhassen Zouari |
A modular verification methodology for D-NRI Petri nets |
|
| 2003 |
L Petrucci, L M Kristensen, J Billington, Z H Qureshi |
Developing a Formal Specification for the Mission System of a Maritime Surveillance Aircraft |
|
| 2003 |
S Bardin, A Finkel, J Leroux, L Petrucci |
FAST: Fast Acceleration of Symbolic Transition systems |
|
| 2003 |
J Billington, S Christensen, K van Hee, E Kindler, O Kummer, L Petrucci, R Post, C Stehno, M Weber |
The Petri Net Markup Language: Concepts, Technology and Tools |
|
| 2002 |
Serge Haddad, Jean-michel Ilie, Kais Klai |
An Incremental Verification Technique Using Decomposition of Petri Nets |
|
| 2002 |
Kais Klai, Serge Haddad, Ilié |
An incremental verification technique using decomposition of Petri nets. |
|
| 2002 |
L M Kristensen, J Billington, L Petrucci, Z Qureshi, R Kiefer |
Formal specification and analysis of airborne mission systems |
Lien
|
| 2002 |
L Petrucci |
Modélisation, vérification et applications |
Lien
|
| 2002 |
L Petrucci, L M Kristensen, J Billington, Z Qureshi |
Towards formal specification and analysis of avionics mission systems |
Lien
|
| 2001 |
G Berthelot, L Petrucci |
Specification and Validation of a Concurrent System: An Educational Project |
Lien
|
| 2001 |
B Bérard, M Bidoit, A Finkel, F Laroussinie, A Petit, L Petrucci, _ Ph Schnoebelen |
Systems and Software Verification. Model-Checking Techniques and Tools |
Lien
|
| 2000 |
J-M Ilié, Kais Klai |
A Modular Verification Methodology for D-NRI Petri Nets |
|
| 2000 |
F Belala, M Bettaz, L Petrucci |
Concurrent systems analysis using ECATNets |
Lien
|
| 2000 |
L Petrucci |
Design and validation of a controller |
Lien
|
| 2000 |
S Christensen, L Petrucci |
Modular analysis of Petri nets |
Lien
|
| 2000 |
G Berthelot, L Petrucci |
Specification and Validation of a Concurrent System: An Educational Project |
Lien
|
| 1998 |
S Christensen, L Petrucci |
How to determine and use place flows in coloured Petri nets |
|
| 1998 |
K Barkaoui, L Petrucci |
Structural analysis of workflow nets with shared resources |
Lien
|
| 1997 |
M Maouche, M Bettaz, G Berthelot, L Petrucci |
Du vrai parallélisme dans les réseaux algébriques et de son application dans les systèmes de production |
|
| 1997 |
F Belala, L Petrucci |
Sémantique des ECATNets en termes de CPNets : application à un exemple de production |
|
| 1995 |
S Christensen, L Petrucci |
Modular state space analysis of coloured Petri nets |
Lien
|
| 1995 |
A Finkel, O Marcé, L Petrucci |
Un algorithme en $n^3/2$ pour le problème de la borne des bonnes places d'un réseau de Petri |
|
| 1994 |
A Finkel, L Petrucci |
Propriétés de la composition/décomposition de réseaux de Petri et de leurs graphes de couverture |
|
| 1992 |
A Finkel, L Petrucci |
Avoiding state explosion by composition of minimal covering graphs |
|
| 1992 |
G Berthelot, C Johnen, L Petrucci |
PAPETRI : environment for the analysis of Petri nets |
|
| 1992 |
C Dimitrovici, U Hummert, L Petrucci |
Semantics, composition and net properties of algebraic high-level nets |
|
| 1992 |
S Christensen, L Petrucci |
Towards a modular analysis of coloured Petri nets |
|
| 1991 |
L Petrucci |
Techniques d'analyse des réseaux de Petri algébriques |
|
| 1990 |
G Berthelot, A Finkel, C Johnen, L Petrucci |
A generic example for testing performance of reachability and covering graphs construction algorithms |
|
| 1990 |
L Petrucci |
Combining Finkel's and Jensen's reduction techniques to build covering trees for coloured nets |
|
| 1990 |
C Dimitrovici, U Hummert, L Petrucci |
The properties of algebraic nets schemes in some semantics |
|