ANR PACS

ANR PACS

Parametric Analyses of Concurrent Systems

ANR-14-CE28-0002

PACS

Publications

[ADF19] Étienne André, Benoît Delahaye, Paulin Fournier: Consistency in Parametric Interval Probabilistic Timed Automata. JLAMP. To appear. [doi] [arXiv]
[AKLPP19] Étienne André, Michał Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci: Parametric verification: An introduction. ToPNoC. To appear. [arXiv]
[And19S] Étienne André: What’s decidable about parametric timed automata?. STTT 21(2), pp.203-219. 2019. [doi] [arXiv]
[JLR19] Aleksandra Jovanović, Didier Lime, Olivier H. Roux: A Game Approach to the Parametric Control of Real-time Systems. International Journal of Control 92(9), pp.2025-2036. 2019. [doi]
[ADL19] Mohamed Amine Aouadhi, Benoît Delahaye, Arnaud Lanoix: Introducing probabilistic reasoning within Event-B. Software, System Modeling 18(3), pp.1953-1984. 2019. [doi]
[ALM19] Mohamed Amine Aouadhi, Benoît Delahaye, Arnaud Lanoix: Language Preservation Problems in Parametric Timed Automata. LMCS. To appear. [arXiv]
[AAGR19] Étienne André, Arcaini, Paolo, Gargantini, Angelo, Radavelli, Marco: Repairing Timed Automata Clock Guards through Abstraction, Testing. TAP, LNCS 11823, pp.129-146. 2019. [doi] [arXiv]
[ABPV19] Étienne André, Bloemen, Vincent, Laure Petrucci, Jaco van de Pol: Minimal-Time Synthesis for Parametric Timed Automata. TACAS, Part II, LNCS 11428, pp.211-228. 2019. [doi]
[ACFJL19] Étienne André, Coquard, Emmanuel, Laurent Fribourg, Jawher Jerray, Lesens, David: Scheduling synthesis for a launcher flight control using parametric stopwatch automata. ACSD, IEEE, pp.13-22. 2019. [doi] [arXiv]
[ADFL19] Étienne André, Benoît Delahaye, Paulin Fournier, Didier Lime: Parametric Timed Broadcast Protocols. VMCAI, LNCS 11388, pp.409-424. 2019. [doi] [arXiv]
[AFMS19] Étienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat: Verification of an industrial asynchronous leader election algorithm using abstractions, parametric model checking. VMCAI, LNCS 11388, pp.409-424. 2019. [doi] [arXiv]
[AJS19] Étienne André, Jawher Jerray, Sahar Mhiri: Time4sys2imi: A tool to formalize real-time system models under uncertainty. ICTAC, LNCS. To appear. [arXiv]
[ALR19F] Étienne André, Didier Lime, Mathias Ramparison: Parametric updates in parametric timed automata. FORTE, LNCS 11535, pp.39-56. 2019. [doi] [arXiv]
[ALR19I] Étienne André, Didier Lime, Mathias Ramparison: On the expressive power of invariants in parametric timed automata. ICECCS, IEEE. To appear. [arXiv]
[ALRS19] Étienne André, Didier Lime, Mathias Ramparison, Mariëlle Stoelinga: Parametric analyses of attack-fault trees. ACSD, IEEE, pp.33-42. 2019. [doi] [arXiv]
[Andre19T] Étienne André: Formalizing Time4sys using parametric timed automata. TASE, IEEE, pp.176-183. 2019. [doi] [arXiv]
[AS19] Étienne André, Sun, Jun: Parametric Timed Model Checking for Guaranteeing Timed Opacity. ATVA, Springer LNCS. To appear. [arXiv]
[BADFL19] Ran Bao, Christian Attiogbe, Benoît Delahaye, Paulin Fournier, Didier Lime: Parametric Statistical Model-checking of UAV Flight Plan. FORTE, LNCS 11535, pp.57-74. 2019. [doi]
[LRS19] Didier Lime, Olivier H. Roux, Seidner, Charlotte: Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets. Petri Nets, LNCS 11522, pp.406-425. 2019. [doi]
[WA19] Masaki Waga, Étienne André: Online Parametric Timed Pattern Matching with Automata-Based Skipping. NFM, LNCS 1146O, pp.371-389. 2019. [doi] [arXiv]
[WAH19] Masaki Waga, Étienne André, Ichiro Hasuo: Symbolic Monitoring against Specifications Parametric in Time, Data. CAV, LNCS 11561, pp.520-539. 2019. [doi] [arXiv]
[CNRS19] CNRS: Une nouvelle méthode pour déterminer la périodicité des logs. Résultats scientifiques Informatique. 2019. [URL]
[GKQT18] Aarti Gupta, Vineet Kahlon, Shaz Qadeer, Tayssir Touili: Model Checking Concurrent Programs. Handbook of Model Checking, Springer, pp.573-611. 2018. [doi]
[BDFLMT18] Anicet Bart, Benoît Delahaye, Paulin Fournier, Didier Lime, Éric Monfroy, Charlotte Truchet: Reachability in Parametric Interval Markov Chains using Constraints. TCS 747, pp.48-74. 2018. [doi]
[AL18] Étienne André, Lin, Shang-Wei: The language preservation problem is undecidable for parametric event-recording automata. IPL 136, pp.17-20, Elsevier. 2018. [doi] [arXiv]
[And18F] Étienne André: A benchmark library for parametric timed model checking. FTSCS, Springer CCIS 1008, pp.75-83. 2018. [doi] [arXiv]
[AHW18] Étienne André, Ichiro Hasuo, Masaki Waga: Offline timed pattern matching under uncertainty. ICECCS, IEEE, pp.10-20. 2018. 🏆 Best paper award. [doi] [arXiv]
[ALR18A] Étienne André, Didier Lime, Mathias Ramparison: Timed automata with parametric updates. ACSD, IEEE, pp.21--29. 2018. [URL] [doi]
[ALR18F] Étienne André, Didier Lime, Mathias Ramparison: TCTL model checking lower/upper-bound parametric timed automata without invariants. FORMATS, Springer LNCS 11022, pp.1-17. 2018. [URL] [doi]
[BLRS18] Hanifa Boucheneb, Didier Lime, Olivier H. Roux, Charlotte Seidner: Optimal-cost Reachability Analysis based on Time Petri Nets. ACSD, IEEE, pp.30--39. 2018. [doi]
[PVdP18] Laure Petrucci and Jaco van de Pol: Parameter Synthesis Algorithms for Parametric Interval Markov Chains. FORTE, Springer LNCS 10854, pp.121-140. 2018. [doi]
[NPVdP18] Nguyễn Hoàng Gia, Laure Petrucci, Jaco van de Pol: Layered, Collecting NDFS with Subsumption for Parametric Timed Automata. ICECCS, IEEE, pp.1-9. 2018. [doi]
[DT18] Marcio Diaz, Tayssir Touili: Model Checking Dynamic Pushdown Networks with Locks, Priorities. NETYS, Springer LNCS 11028, pp.240--251. 2018. [doi]
[AL18E] Étienne André, Lipari, Giuseppe: Tutorial on Schedulability Analysis under Uncertainty using Formal Methods. Tutorial at ESWEEK 2018. 2018. [URL]
[Andre18HDR] Étienne André: Contributions to parametric timed model checking: Theory, algorithms. Habilitation à diriger les recherches, Université Paris 13, France. 2018. [URL]
[AKLPP17] Étienne André, Michał Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci: Tutorial on parametric verification. Advanced tutorial at Petri Nets 2017. 2017. [URL]
[AKLPP17v] Étienne André, Michał Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci: Parametric verification. Online course. 2017. [URL]
[DEB17] Benoît Delahaye, Eveillard, Damien, Bouskill, Nicholas: On the Power of Uncertainties in Microbial System Modeling: No Need To Hide Them Anymore. mSystems 6(2). 2017. [doi]
[ANP17] Étienne André, Nguyễn Hoàng Gia, Laure Petrucci: Efficient parameter synthesis using optimized state exploration strategies. ICECCS, IEEE, pp.1-10. 2017. [doi]
[Andre17F] Étienne André: A unified formalism for monoprocessor schedulability analysis under uncertainty. FMICS-AVoCS, Springer LNCS 10471, pp.100-115. 2017. 🏆 Best paper award. [doi]
[BQS17] Benedikt Bollig, Karin Quaas, Arnaud Sangnier: The Complexity of Flat Freeze LTL. CONCUR, LIPIcs 85, 33:1--33:16, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2017. [doi]
[DT17a] Marcio Diaz, Tayssir Touili: Dealing with priorities, locks for concurrent programs. ATVA, Springer LNCS 10482, pp.208-224. 2017. [doi]
[DT17b] Marcio Diaz et Tayssir Touili: Reachability Analysis of Dynamic Pushdown Networks with Priorities. NETYS, Springer LNCS 10299, pp.288-303. 2017. [doi]
[LSGA17] Li, Jiaying, Sun, Jun, Gao, Bo, Étienne André: Classification based Parameter Synthesis for Parametric Timed Automata. ICFEM, Springer LNCS 10610, pp.243--261. 2017. [doi]
[BLPRS17] Hanifa Boucheneb, Didier Lime, Baptiste Parquier, Olivier H. Roux, Charlotte Seidner: Optimal Reachability in Cost Time Petri Nets. FORMATS, Springer LNCS 10419, pp.58-73. 2017. [doi]
[ANPS17] Étienne André, Nguyễn Hoàng Gia, Laure Petrucci, Sun Jun.: Parametric model checking timed automata under non-Zenoness assumption. NFM, Springer LNCS 10227, pages 35-51. 2017. [doi]
[AL17F] Étienne André, Lin Shang-Wei: Learning-based compositional parameter synthesis for event-recording automata. FORTE, Springer LNCS 10321, pp.17-32. 2017. 🏆 Best FORTE paper award, best DisCoTec paper award. [URL] [doi]
[DJLR17] Nicolas David, Claude Jard, Didier Lime, Olivier H. Roux: Coverability Synthesis in Parametric Petri Nets. CONCUR, LIPIcs. 2017. [doi]
[AL17b] Étienne André, Didier Lime: Liveness in L/U-Parametric Timed Automata. ACSD, IEEE, pp.9-18. 2017. [doi]
[AKJPP17] Étienne André, Michał Knapik, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci: Timed ATL: Forget Memory, Just Count. AAMAS, IFAAMAS, pages 1460–1462. 2017. [URL] [doi]
[ADL17] Mohamed Amine Aouadhi, Benoît Delahaye, Arnaud Lanoix: Moving from Event-B to Probabilistic Event-B. SAC-SVT, ACM, pp.1348-1355. 2017. [doi]
[BDLMT17] Anicet Bart, Benoît Delahaye, Didier Lime, Éric Monfroy, Charlotte Truchet: Reachability in Parametric Interval Markov Chains using Constraints. QEST, Springer LNCS 10503, pp.173-189. 2017. 🏆 Best paper award. [doi]
[DHLST17] Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, Daniel Thoma: Model-Checking Counting Temporal Logics on Flat Structures. CONCUR, LIPIcs 85, pp.29:1--29:17, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 2017. [doi]
[NT17] Nguyen, Huu-Vu, Tayssir Touili: CARET Analysis of Multithreaded Programs. LOPSTR, Springer LNCS, 10855, pp.73-90. 2017. [doi]
[PT17] Adrien Pommellet, Tayssir Touili: Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous. APLAS, Springer LNCS 10695, pp.235-254. 2017. [doi]
[SSPT17] Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, Sébastien Tixeuil: Parameterized verification of algorithms for oblivious robots on a ring. FMCAD, IEEE, pp.212-219. 2017. [doi]
[DJS16] Benoît Delahaye, Loïg Jézéquel, Jiří Srba: Proceedings of the 3rd International Workshop on the Synthesis of Complex Parameters (SynCoP 2016). Electronic Proceedings in Theoretical Computer Science 220. 2016. [doi]
[AKLPP16] Étienne André, Michał Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci: Tutorial on parametric verification. Advanced tutorial at Petri Nets 2016. 2017. [URL]
[ACR16] Étienne André, Chatain, Thomas, Rodríguez, César: Preserving Partial Order Runs in Parametric Time Petri Nets. Transactions on Embedded Computing Systems 16(2), ACM, pp.43:1-43:26. 2016. [doi]
[ADRST16] Parosh A. Abdulla, Giorgio Delzanno, Othmane Rezine, Arnaud Sangnier, Riccardo Traverso: Parameterized verification of time-sensitive models of ad hoc network protocols. TCS 612, pp.1-22. 2016. [doi]
[BHJL16] Bérard, Béatrice, Haddad, Serge, Aleksandra Jovanović, Didier Lime: Interrupt Timed Automata with Auxiliary Clocks, Parameters. Fundamenta Informaticae, 143(3-4), pp.235-259. 2016. [doi]
[DST16] Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso: Adding Data Registers to Parameterized Networks with Broadcast. Fundamenta Informaticae 143(3-4), pp.287-316. 2016. [doi]
[ACR16] Étienne André, Thomas Chatain, César Rodríguez: Preserving Partial Order Runs in Parametric Time Petri Nets. Transactions on Embedded Computing Systems 16(2), pages 43:1–43:26. 2017. [doi]
[AD16] Étienne André, Benoît Delahaye: Consistency in Parametric Interval Probabilistic Timed Automata. TIME, IEEE, pp.110-119. 2016. [doi]
[ADRS16] Parosh Abulla, Giorgio Delzanno, O. Rezine, Arnaud Sangnier, R. Traverso: Parameterized verification of time-sensitive models of ad hoc network protocols. Theoretical Computer Science 612, pages 1--22. Elsevier Science Publishers, 2016. 2016. [URL] [doi]
[AKPP16] Étienne André, Michał Knapik, Wojciech Penczek, Laure Petrucci: Controlling Actions, Time in Parametric Timed Automata. Proceedings of the 16th International Conference on Application of Concurrency to System Design (ACSD), IEEE, pp.45-54. 2016. [URL] [doi]
[ALR16I] Étienne André, Didier Lime, Olivier H. Roux: Decision Problems for Parametric Timed Automata. In Kazuhiro Ogata, Mark Lawford (eds.), ICFEM’16, Springer LNCS, November 2016.. 2016. [doi]
[ALR16b] Étienne André, Didier Lime, Olivier H. Roux: On the Expressiveness of Parametric Timed Automata. In Martin Fränzle, Nicolas Markey (eds.), FORMATS’16, LNCS 9884, Springer, pages 19–34, August 2016. 2016. [URL] [doi]
[And16] Étienne André: Parametric Deadlock-Freeness Checking Timed Automata. ICTAC, Springer LNCS 9965, pp.469-478. 2016. [doi]
[BHJL16] Béatrice Bérard, Serge Haddad, Aleksandra Jovanović, Didier Lime: Interrupt Timed Automata with Auxiliary Clocks, Parameters. Fundamenta Informaticae, IOS Press, volume 143:3–4, pages 235–239. 2016. [URL] [doi]
[BMRSS16] Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, Daniel Stan: Reachability in Networks of Register Protocols under Stochastic Schedulers. ICALP, LIPIcs 55, pages 106:1-106:14, Leibniz-Zentrum für Informatik. 2016. [URL] [doi]
[DH16] Durand-Gasselin, Peter Habermehl: Regular Transformations of Data Words Through Origin Information. FoSSaCS, Springer LNCS 9634, pp.285-300. 2016. [URL] [doi]
[DLP16] Benoît Delahaye, Didier Lime, Laure Petrucci: Parameter Synthesis for Parametric Interval Markov Chains. VMCAI, LNCS volume 9583, pages 372–390. 2016. [URL] [doi]
[DST16] G. Delzanno, Arnaud Sangnier, R. Traverso: Adding Data Registers to Parameterized Networks with Broadcast. Fundamenta Informaticae 143(3-4), pages 287-316.2016. 2016. [URL] [doi]
[PP16] Laure Petrucci, Jaco van de Pol: Parametric Interval Markov Chains: Synthesis Revisited. FMICS-AVoCS Research Ideas, Research Report, Istituto di Scienza e Tecnologie dell’Informazione, Consiglio Nazionale delle Ricerche. 2016. [URL]
[PRHSRLA16] Parquier, Baptiste, Rioux, Laurent, Henia, Rafik, Romain Soulat, Olivier H. Roux, Didier Lime, Étienne André: Applying parametric model-checking techniques for reusing real-time critical systems. FTSCS, Springer CCIS 694, pp.129-144. 2016. [doi]
[AG15] Étienne André, Goran Frehse: Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters (SynCoP 2015). Volume 44 of OASIcs, Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH. 2015. [URL] [doi]
[JLR15] Aleksandra Jovanović, Didier Lime, Olivier H. Roux: Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering (TSE), IEEE Computer Society Press, volume 41:5, pages 445–461. 2015. [URL] [doi]
[ST15] Song, Tayssir Touili: Model checking dynamic pushdown networks. FAC 27(2), pp.397-421. 2015. [URL] [doi]
[DJLR15] Nicolas David, Claude Jard, Didier Lime, Olivier H. Roux: Discrete Parameters in Petri Nets. In proceedings of the 36th International Conference on Application, Theory of Petri Nets, Concurrency (Petri Nets 2015), Springer LNCS volume 9115, pages 137–156. 2016. [URL] [doi]
[BFS15] Nathalie Bertrand, Paulin Fournier, Arnaud Sangnier: Distributed Local Strategies in Broadcast Networks. In CONCUR’15, LIPIcs 42, pages 44-57. Leibniz-Zentrum für Informatik, 2015. . 2016. [URL] [doi]
[ACN15] Étienne André, Camille Coti, Nguyễn Hoàng Gia: Enhanced Distributed Behavioral Cartography of Parametric Timed Automata. ICFEM’15, Springer LNCS 9407, pages 319–335. 2015. [URL] [doi]
[ACR15] Étienne André, Thomas Chatain, César Rodríguez: Preserving Partial Order Runs in Parametric Time Petri Nets. ACSD’15, IEEE, pages 120–129. 2015. [URL] [doi]
[ALNS15] Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia, Sun Youcheng: Reachability Preservation Based Parameter Synthesis for Timed Automata. NFM’15, LNCS 9058, Springer, pages 50–65. 2015. [URL] [doi]
[ALR15] Étienne André, Didier Lime, Olivier H. Roux: Integer-Complete Synthesis for Bounded Parametric Timed Automata. RP’15, LNCS 9328, Springer, pages 7–19. 2015. [URL] [doi]
[AM15] Étienne André, Nicolas Markey: Language Preservation Problems in Parametric Timed Automata. FORMATS’15, Springer LNCS 9268, pages 27–43. 2015. [URL] [doi]
[And16] Étienne André: What’s decidable about parametric timed automata?. FTSCS’15, Springer CCIS 596, pages 1–17. 2016. [URL] [doi]
[AP15] Étienne André, Laure Petrucci: Unifying Patterns for Modelling Timed Relationships in Systems, Properties. PNSE’15, CEUR-WS volume 1372, pages 25–40. 2015. [URL]
[Del15] Benoît Delahaye: Consistency for Parametric Interval Markov Chains. In the proceedings of the 2nd International Workshop on Synthesis of Complex Parameters (SynCoP 2015), volume 44 of OASIcs, pages 17–32. 2015. [URL] [doi]
[SAL15] Sun Youcheng, Étienne André, Giuseppe Lipari: Verification of Two Real-Time Systems Using Parametric Timed Automata. In the informal proceedings of WATERS’15. 2015. [URL]
[ALSD14] Étienne André, Liu Yang, Sun Jun, Dong Jin Song: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. Real-Time Systems Journal 50(5–6), pages 620–679. 2014. [URL] [doi]
[ABHJLPRT14] Étienne André, Benoît Delahaye, Peter Habermehl, Claude Jard, Didier Lime, Laure Petrucci, Olivier H. Roux, Tayssir Touili: Beyond Model Checking: Parameters Everywhere. Actes des Sixièmes journées nationales du Groupement de Recherche CNRS du Génie de la Programmation et du Logiciel (GDR-GPL). 2014. [URL]