Bibliography

Major publications by the team in recent years

• 1X. Etchevers, G. Salaün, F. Boyer, T. Coupaye, N. De Palma.
  
  Reliable Self-deployment of Distributed Cloud Applications, in: Software: Practice and Experience, 2017, vol. 47, n^o 1, pp. 3-20. [ DOI : 10.1002/spe.2400 ]
  
  https://hal.inria.fr/hal-01290465
• 2H. Evrard, F. Lang.
  
  Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous, in: Journal of Logical and Algebraic Methods in Programming, March 2017, vol. 88, 33 p. [ DOI : 10.1016/j.jlamp.2016.09.002 ]
  
  https://hal.inria.fr/hal-01412911
• 3H. Garavel.
  
  Nested-unit Petri nets, in: Journal of Logical and Algebraic Methods in Programming, April 2019, vol. 104, pp. 60-85. [ DOI : 10.1016/j.jlamp.2018.11.005 ]
  
  https://hal.inria.fr/hal-02072190
• 4H. Garavel, F. Lang, R. Mateescu.
  
  Compositional Verification of Asynchronous Concurrent Systems using CADP, in: Acta Informatica, June 2015, vol. 52, n^o 4, 56 p. [ DOI : 10.1007/s00236-015-0226-1 ]
  
  https://hal.inria.fr/hal-01247507
• 5H. Garavel, F. Lang, R. Mateescu, W. Serwe.
  
  CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes, in: International Journal on Software Tools for Technology Transfer, 2013, vol. 15, n^o 2, pp. 89-107. [ DOI : 10.1007/s10009-012-0244-z ]
  
  http://hal.inria.fr/hal-00715056
• 6H. Garavel, F. Lang, W. Serwe.
  
  From LOTOS to LNT, in: ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, J.-P. Katoen, R. Langerak, A. Rensink (editors), Lecture Notes in Computer Science, Springer, October 2017, vol. 10500, pp. 3-26. [ DOI : 10.1007/978-3-319-68270-9_1 ]
  
  https://hal.inria.fr/hal-01621670
• 7A. Krishna, P. Poizat, G. Salaün.
  
  Checking Business Process Evolution, in: Science of Computer Programming, January 2019, vol. 170, pp. 1-26. [ DOI : 10.1016/j.scico.2018.09.007 ]
  
  https://hal.inria.fr/hal-01920273
• 8R. Mateescu, W. Serwe.
  
  Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols, in: Science of Computer Programming, February 2012. [ DOI : 10.1016/j.scico.2012.01.003 ]
  
  http://hal.inria.fr/hal-00671321

Publications of the year

Doctoral Dissertations and Habilitation Theses

• 9L. Marsso.
  
  On Model-based Testing of GALS Systems, Université Grenoble Alpes, December 2019.
• 10U. Ozeer.
  
  Autonomic Resilience of Applications in a Largely Distributed Cloud Environment, Université Grenoble Alpes, December 2019.

Articles in International Peer-Reviewed Journals

• 11G. Barbon, V. Leroy, G. Salaün.
  
  Debugging of Behavioural Models using Counterexample Analysis, in: IEEE Transactions on Software Engineering, 2019, pp. 1-14, forthcoming. [ DOI : 10.1109/TSE.2019.2915303 ]
  
  https://hal.inria.fr/hal-02145610
• 12F. Durán, C. Rocha, G. Salaün.
  
  A Rewriting Logic Approach to Resource Allocation Analysis in Business Process Models, in: Science of Computer Programming, November 2019, vol. 183, pp. 1-32. [ DOI : 10.1016/j.scico.2019.102303 ]
  
  https://hal.inria.fr/hal-02345895
• 13H. Garavel.
  
  Nested-unit Petri nets, in: Journal of Logical and Algebraic Methods in Programming, April 2019, vol. 104, pp. 60-85. [ DOI : 10.1016/j.jlamp.2018.11.005 ]
  
  https://hal.inria.fr/hal-02072190
• 14A. Krishna, P. Poizat, G. Salaün.
  
  Checking Business Process Evolution, in: Science of Computer Programming, January 2019, vol. 170, pp. 1-26. [ DOI : 10.1016/j.scico.2018.09.007 ]
  
  https://hal.inria.fr/hal-01920273

International Conferences with Proceedings

• 15G. Barbon, V. Leroy, G. Salaün.
  
  Debugging of Behavioural Models with CLEAR, in: TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Prague, Czech Republic, Lecture Notes in Computer Science, Springer, April 2019, vol. 11427, pp. 386-392. [ DOI : 10.1007/978-3-030-17462-0_ 26 ]
  
  https://hal.archives-ouvertes.fr/hal-02121180
• 16G. Barbon, V. Leroy, G. Salaün, E. Yah.
  
  Visual Debugging of Behavioural Models, in: ICSE 2019 - IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings, Montreal, Canada, IEEE, May 2019, pp. 107-110. [ DOI : 10.1109/ICSE-Companion.2019.00050 ]
  
  https://hal.inria.fr/hal-02145535
• 17E. Bartocci, D. Beyer, P. Black, G. Fedyukovich, H. Garavel, A. Hartmanns, M. Huisman, F. Kordon, J. Nagele, M. Sighireanu, B. Steffen, M. Suda, G. Sutcliffe, T. Weber, A. Yamada.
  
  TOOLympics 2019: An Overview of Competitions in Formal Methods, in: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 2019, pp. 3-24. [ DOI : 10.1007/978-3-030-17502-3_1 ]
  
  https://hal.sorbonne-universite.fr/hal-02094030
• 18F. Durán, H. Garavel.
  
  The Rewrite Engines Competitions: A RECtrospective, in: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), Part III: TOOLympics, Prague, Czech Republic, Lecture Notes in Computer Science, Springer, April 2019, vol. 11429, pp. 1-9. [ DOI : 10.1007/978-3-030-17502-3 ]
  
  https://hal.inria.fr/hal-02133649
• 19F. Durán, C. Rocha, G. Salaün.
  
  Analysis of Resource Allocation of BPMN Processes, in: ICSOC 2019 - 17th International Conference on Service-Oriented Computing, Toulouse, France, Springer, October 2019, pp. 452-457. [ DOI : 10.1007/978-3-030-33702-5_35 ]
  
  https://hal.inria.fr/hal-02345879
• 20F. Durán, G. Salaün, A. Krishna.
  
  Automated Composition, Analysis and Deployment of IoT Applications, in: TOOLS 2019 - 51st International Conference on Software Technology: Methods and Tools, Innopolis, Russia, Springer, October 2019, pp. 252-268. [ DOI : 10.1007/978-3-030-29852-4_21 ]
  
  https://hal.inria.fr/hal-02345865
• 21A. Krishna, M. Le Pallec, R. Mateescu, L. Noirie, G. Salaün.
  
  IoT Composer: Composition and Deployment of IoT Applications, in: ICSE 2019 - IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings, Montreal, Canada, IEEE, May 2019, pp. 19-22. [ DOI : 10.1109/ICSE-Companion.2019.00028 ]
  
  https://hal.inria.fr/hal-02146569
• 22A. Krishna, M. Le Pallec, R. Mateescu, L. Noirie, G. Salaün.
  
  Rigorous Design and Deployment of IoT Applications, in: FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, Montreal, Canada, ACM, May 2019, pp. 21-30. [ DOI : 10.1109/FormaliSE.2019.00011 ]
  
  https://hal.inria.fr/hal-02146553
• 23F. Lang, R. Mateescu, F. Mazzanti.
  
  Compositional Verification of Concurrent Systems by Combining Bisimulations, in: FM 2019 - 23rd International Conference on Formal Methods, Porto, Portugal, Lecture Notes in Computer Science, Springer Verlag, October 2019, vol. 11800, pp. 196-213. [ DOI : 10.1007/978-3-030-30942-8_13 ]
  
  https://hal.inria.fr/hal-02295459
• 24P. Ledent, A. Paigwar, A. Renzaglia, R. Mateescu, C. Laugier.
  
  Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving, in: CIS-RAM 2019 - 9th IEEE International Conference on Cybernetics and Intelligent Systems (CIS) Robotics, Automation and Mechatronics (RAM), Bangkok, Thailand, IEEE, November 2019, pp. 1-6.
  
  https://hal.inria.fr/hal-02355551
• 25L. Marsso, R. Mateescu, I. Parissis, W. Serwe.
  
  Asynchronous Testing of Synchronous Components in GALS Systems, in: IFM'2019 - 15th International Conference on Integrated Formal Methods, Bergen, Norway, Lecture Notes in Computer Science, Springer Verlag, November 2019, vol. 11918, pp. 360-378. [ DOI : 10.1007/978-3-030-34968-4_20 ]
  
  https://hal.archives-ouvertes.fr/hal-02394989
• 26U. Ozeer, L. Letondeur, F.-G. Ottogalli, G. Salaün, J.-M. Vincent.
  
  Designing and Implementing Resilient IoT Applications in the Fog: A Smart Home Use Case, in: ICIN 2019 - 22nd Conference on Innovation in Clouds, Internet and Networks, Paris, France, IEEE, February 2019, pp. 230-232. [ DOI : 10.1109/ICIN.2019.8685909 ]
  
  https://hal.archives-ouvertes.fr/hal-01979686

Scientific Books (or Scientific Book chapters)

• 27H. Garavel, R. Mateescu.
  
  Reflections on Bernhard Steffen’s Physics of Software Tools, in: Models, Mindsets, Meta: The What, the How, and the Why Not?, Springer Verlag, June 2019, pp. 186-207. [ DOI : 10.1007/978-3-030-22348-9_12 ]
  
  https://hal.inria.fr/hal-02394588
• 28V.-A. Nguyen, W. Serwe, R. Mateescu, E. Jenn.
  
  Hunting Superfluous Locks with Model Checking, in: From Software Engineering to Formal Methods and Tools, and Back, Lecture Notes in Computer Science, Springer Verlag, October 2019, vol. 11865, pp. 416-432. [ DOI : 10.1007/978-3-030-30985-5_24 ]
  
  https://hal.inria.fr/hal-02314088

References in notes

• 29R. Ameur-Boulifa, A. Cavalli, S. Maag.
  
  Verifying Complex Software Control Systems from Test Objectives: Application to the ETCS System, in: Proceedings of the 14th International Conference on Software Technologies (ICSOFT'2019), Prague, Czech Republic, SciTePress, July 2019, pp. 397–406.
• 30S. Chabane, R. Ameur-Boulifa, M. Mohamed.
  
  Vers une conception de systèmes réactifs synchrones sûrs, in: Actes du 12ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'2019), Angers, France, November 2019.
• 31D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, G. Smeding.
  
  Reference Manual of the LNT to LOTOS Translator (Version 6.8), January 2019, Inria, Grenoble, France.
• 32E. M. Clarke, E. A. Emerson, A. P. Sistla.
  
  Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications, in: ACM Transactions on Programming Languages and Systems, April 1986, vol. 8, n^o 2, pp. 244–263.
• 33R. De Nicola, F. W. Vaandrager.
  
  Action versus State Based Logics for Transition Systems, Lecture Notes in Computer Science, Springer Verlag, 1990, vol. 469, pp. 407–419.
• 34H. Garavel.
  
  Compilation of LOTOS Abstract Data Types, in: Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89 (Vancouver B.C., Canada), S. T. Vuong (editor), North Holland, December 1989, pp. 147–162.
• 35H. Garavel.
  
  OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing, in: Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98 (Lisbon, Portugal), Berlin, B. Steffen (editor), Lecture Notes in Computer Science, Springer Verlag, March 1998, vol. 1384, pp. 68–84, Full version available as Inria Research Report RR-3352.
• 36H. Garavel, F. Lang.
  
  SVL: a Scripting Language for Compositional Verification, in: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001 (Cheju Island, Korea), M. Kim, B. Chin, S. Kang, D. Lee (editors), Kluwer Academic Publishers, August 2001, pp. 377–392, Full version available as Inria Research Report RR-4223.
• 37H. Garavel, F. Lang, R. Mateescu.
  
  Compiler Construction using LOTOS NT, in: Proceedings of the 11th International Conference on Compiler Construction CC 2002 (Grenoble, France), N. Horspool (editor), Lecture Notes in Computer Science, Springer Verlag, April 2002, vol. 2304, pp. 9–13.
• 38H. Garavel, R. Mateescu, I. Smarandache-Sturm.
  
  Parallel State Space Construction for Model-Checking, in: Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001 (Toronto, Canada), Berlin, M. B. Dwyer (editor), Lecture Notes in Computer Science, Springer Verlag, May 2001, vol. 2057, pp. 217–234, Revised version available as Inria Research Report RR-4341 (December 2001).
• 39H. Garavel, W. Serwe.
  
  State Space Reduction for Process Algebra Specifications, in: Theoretical Computer Science, February 2006, vol. 351, n^o 2, pp. 131–145.
• 40H. Garavel, J. Sifakis.
  
  Compilation and Verification of LOTOS Specifications, in: Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), L. Logrippo, R. L. Probert, H. Ural (editors), North Holland, June 1990, pp. 379–394.
• 41H. Hansson, B. Jonsson.
  
  A Logic for Reasoning about Time and Reliability, in: Formal Aspects of Computing, 1994, vol. 6, n^o 5, pp. 512–535.
• 42M. Hendriks.
  
  Can Machine Learning Automatically Choose your Best Model Checking Strategy?, EEMCS: Electrical Engineering, Mathematics and Computer Science, University of Twente, 2019.
• 43M. Hennessy, R. Milner.
  
  Algebraic Laws for Nondeterminism and Concurrency, in: Journal of the ACM, 1985, vol. 32, pp. 137–161.
• 44F. Kordon, H. Garavel, L. M. Hillah, F. Hulin-Hubard, E. Amparore, M. Beccuti, B. Berthomieu, G. Ciardo, S. Dal Zilio, T. Liebke, A. Linard, J. Meijer, A. Miner, J. Srba, Y. Thierry-Mieg, J. van de Pol, K. Wolf.
  
  Complete Results for the 2019 Edition of the Model Checking Contest, April 2019.
  
  http://mcc.lip6.fr/2019/results.php
• 45J. Magee, J. Kramer.
  
  Concurrency: State Models and Java Programs, 2006, Wiley, April 2006.
• 46F. Martinelli, F. Mercaldo, V. Nardone, A. Orlando, A. Santone, G. Vaglini.
  
  Model Checking Based Approach for Compliance Checking, in: Journal of Information Technology and Control, May 2019, vol. 48, n^o 2, pp. 278–298.
• 47R. Mateescu, D. Thivolle.
  
  A Model Checking Language for Concurrent Value-Passing Systems, in: Proceedings of the 15th International Symposium on Formal Methods FM'08 (Turku, Finland), J. Cuellar, T. Maibaum, K. Sere (editors), Lecture Notes in Computer Science, Springer Verlag, May 2008, vol. 5014, pp. 148–164.
• 48R. Mateescu, A. Wijs.
  
  Property-dependent Reductions Adequate with Divergence-sensitive Branching Bisimilarity, in: Science of Computer Programming, 2014, vol. 96, pp. 354–376.
• 49H. Mkaouar.
  
  A Formal Approach for Real-time Systems Engineering, University of Sfax, Tunisia, February 2019.
• 50J. Moerman.
  
  Nominal Techniques and Black Box Testing for Automata Learning, Radboud University, Nijmegen, The Netherlands, July 2019.
• 51L. A. Oubelli, Y. A. Ameur, J. Bedouet, B. Chausserie-Lapree, B. Larzul.
  
  Finding Conservative Schema Evolutions by Analysing API Changes, in: Proceedings of the 31st International Conference on Software Engineering and Knowledge Engineering (SEKE'2019), Lisbon, Portugal, KSI Research Inc., July 2019, pp. 748–777.
• 52N. Rosa, H. Kamal, A. Wagner.
  
  A LOTOS-based Lightweight Approach to Formally Verify MPI Applications, Universidade Federal de Pernambuco, Centro de Informática, 2015.
• 53N. Rosa, A. Wagner, H. Kamal.
  
  Towards Lightweight Formal Development of MPI Applications, in: Proceedings of 36th WoTUG Conference on Concurrent and Parallel Programming – Communicating Process Architectures (CPA'2015), Kent, UK, Concurrent Systems Engineering Series, Open Channel Publishing, August 2015, vol. 69, pp. 67–85.
• 54E. Ruijters, D. Reijsbergen, P.-T. de Boer, M. Stoelinga.
  
  Rare Event Simulation for Dynamic Fault Trees, in: Reliability Engineering & System Safety, June 2019, vol. 186, pp. 220–231.
• 55Z. Zhioua, R. Ameur-Boulifa, Y. Roudier.
  
  Framework for the Formal Specification and Verification of Security Guidelines, in: Advances in Science, Technology and Engineering Systems Journal, January 2018, vol. 3, n^o 1, pp. 38–48.