fond
Publications by Béatrice Bérard

Books and chapters

[11] B. Bérard, M. Cabasino, A. di Febbraro, A. Giua, C. Seatzu. Petri nets with time. In C. Seatzu, M. Silva, J. van Schuppen, editors, Control of Discrete Event Systems, pages 319-342. Springer, 2012. [ bib ]
[10] B. Bérard. An introduction to timed automata. In C. Seatzu, M. Silva, J. van Schuppen, editors, Control of Discrete Event Systems, pages 169-187. Springer, 2012. [ bib ]
[9] B. Bérard. Modeling time. In S. Haddad, F. Kordon, L. Pautet, and L. Petrucci, editors, Models and Analysis in Distributed Systems, pages 63-96. Wiley, 2011. [ bib ]
[8] B. Bérard. Timed Model Checking. In C. Jard and O.(H.) Roux, editors, Communicating Embedded Systems - Software and Design. ISTE Publishing / John Wiley, October 2009. [ bib | .html ]
[7] B. Bérard. Model checking temporisé. In O.H. Roux and C. Jard, editors, Approches formelles des systèmes embarqués communicants. Hermes/Lavoisier, October 2008. [ bib | .html ]
[6] B. Bérard. Modèles temporisés. In S. Haddad, F. Kordon, and L. Petrucci, editors, Méthodes Formelles pour les Systèmes Répartis et Coopératifs. Hermes/Lavoisier, September 2006. [ bib ]
[5] B. Bérard et al. Logiciel libre et sûreté de fonctionnement: cas des systèmes critiques. Hermès, 2003. Ouvrage collectif rédigé sous la direction de Ph. David et H. Waeselynck. [ bib | http ]
[4] B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001. [ bib | http ]
[3] Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie, and A. Petit. Vérification de logiciels : techniques et outils du model-checking. Vuibert, April 1999. [ bib | .html ]
[2] A. Arnold, J. Beauquier, B. Bérard, and B. Rozoy. Programmes parallèles, modèles et validation. Armand Colin, January 1992. [ bib ]
[1] J. Beauquier and B. Bérard. Systèmes d'exploitations, concepts et algorithmes. Ediscience, 1990. [ bib ]

International Journals

[28] B. Bérard, S. Haddad, C. Picaronny, M. Safey El Din, and M. Sassolas. Polynomial Interrupt Timed Automata: Verification and Expressiveness. Information and Computation, 2020, doi 10.1016/j.ic.2020.104580. [ bib]
[27] B. Bérard, O. Kouchnarenko, J. Mullins, M. Sassolas. Opacity for Linear Constraint Markov Chains. Discrete Event Dynamic Systems, vol. 28(1): 83-108, 2018. [ bib]
[26] B. Bérard, S. Haar, S. Schwoon, S. Schmitz. The Complexity of Diagnosability and Opacity Verification for Petri Nets. Fundam. Inform., vol. 161(4): 317-349, 2018. [ bib]
[25] B. Bérard, L. Hélouët, J. Mullins. Non-Interference in Partial Order Models. ACM Trans. Embedded Comput. Syst., vol. 16(2): 44:1-44:34, 2017. [ bib]
[24] B. Bérard, P. Lafourcade, L. Millet, M. Potop-Butucaru, Y. Thierry-Mieg, and S. Tixeuil. Formal Verification of Mobile Robot Protocols. Distributed Computing, vol. 29(6): 1-25, 2016. [ bib]
[23] B. Bérard, S. Haddad, A. Jovanovič, and D. Lime. Interrupt Timed Automata with Auxiliary Clocks and Parameters. Fundamenta Informaticae, vol. 143(3-4): 235-259, 2016. [ bib]
[22] B. Bérard, P. Courtieu, L. Millet, M. Potop-Butucaru, L. Rieg, N. Sznajder, S. Tixeuil, and X. Urbain. Formal Methods for Mobile Robots: Current Results and Open Problems. International Journal of Informatics Society, vol. 7(3): 101-104, 2015. [ bib]
[21] B. Bérard, K. Chatterjee, and N. Sznajder. Probabilistic Opacity for Markov Decision Processes. Information Processing Letters, vol. 115(1): 52-59, 2015. [ bib]
[20] B. Bérard, J. Mullins, and M. Sassolas. Quantifying Opacity. Mathematical Structures in Computer science, vol. 25(2): 361-403, 2015. [ bib]
[19] B. Bérard, and J. Mullins. Verification of Information Flow Properties under Rational Observation. ECEASST, vol. 70, 2014. [ bib]
[18] Y. Zhang, B. Bérard,L.-M. Hillah, F. Kordon, and Y. Thierry-Mieg. Controllability for discrete event systems modelled in VeriJ. Int. J. of Critical Computer-Based Systems, vol. 5(3/4): 218-240, 2014. [ bib]
[17] B. Bérard, F. Cassez, S. Haddad, D. Lime, and O.(H) Roux. The Expressive Power of Time Petri Nets. Theoretical Computer science, vol. 474:1-20, 2013. [ bib]
[16] G. Benattar, B. Bérard, D. Lime, J. Mullins, O. H. Roux, and M. Sassolas. Channel Synthesis for Finite Transducers. International Journal of Foundations of Computer science, vol. 23 (6):1241-1260, 2012. [ bib]
[15] B. Bérard, S. Haddad, and M. Sassolas. Interrupt Timed Automata : Verification and Expressiveness. Formal Methods in System Design, 40(1):41-87, February 2012. [ bib | http ]
[14] H. Bel Mokadem, B. Bérard, V. Gourcuff, J.-M. Roussel, and O. de Smet. Verification of a Timed Multitask System with Uppaal. IEEE Transactions on Automation Science and Engineering (T-ASE), 7(4):921-932, October 2010. [ bib ]
[13] B. Bérard, F. Cassez, S. Haddad, D. Lime, and O. (H.) Roux. When are timed automata weakly timed bisimilar to time Petri nets ? Theoretical Computer Science, 403(2-3):202-220, 2008. [ bib ]
[12] B. Bérard, P. Gastin, and A. Petit. Timed substitutions for regular signal-event languages. Formal Methods in System Design, 31(2):101-134, October 2007. [ bib | .pdf ]
[11] M. Ben Gaid, B. Bérard, and O. De Smet. Verification of an evaporator system with uppaal. Journal Européen des Systèmes Automatisés, 39(9-10):1079-1098, 2005. [ bib ]
[10] B. Bérard, P. Bouyer, and A. Petit. Analysing the PGM protocol with Uppaal. International Journal of Production Research, 42(14):2773-2791, July 2004. [ bib | ps.gz ]
[9] B. Bérard, L. Fribourg, F. Klay, and J.-F. Monin. A compared study of two correctness proofs for the standardized algorithm of ABR conformance. Formal Methods in System Design, 22(1):59-86, January 2003. [ bib | ps.gz ]
[8] J. Beauquier, B. Bérard, L. Fribourg, and F. Magniette. Proving convergence of self-stabilizing systems using first-order rewriting and regular languages. Distributed Computing, 14(2):83-95, 2001. [ bib | ps.gz ]
[7] B. Bérard and C. Dufourd. Timed automata and additive clock constraints. Information Processing Letters, 75(1-2):1-7, July 2000. [ bib | ps.gz ]
[6] B. Bérard and C. Picaronny. Accepting Zeno words: A way toward timed refinements. Acta Informatica, 37(1):45-81, 2000. [ bib | ps.gz ]
[5] B. Bérard, V. Diekert, P. Gastin, and A. Petit. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae, 36(2):145-182, November 1998. [ bib | ps.gz ]
[4] B. Bérard. Untiming timed languages. Information Processing Letters, 55(3):129-135, August 1995. [ bib ]
[3] B. Bérard. Global Serializability of Concurrent Programs. Theoretical Computer Science, 124(1):41-70, February 1994. [ bib ]
[2] B. Bérard. Literal shuffle. Theoretical Computer Science, 51:281-299, 1987. [ bib ]
[1] B. Bérard. Formal properties of literal shuffle. Acta Cybernetica, 8(1):17-29, 1987. [ bib ]

International Conferences

[39] B. Bérard, B. Bollig, P. Bouyer, M. Függer, N. Sznajder. Synthesis in Presence of Dynamic Links. In Proceedings of GandALF 2020. [ bib ]
[38] B. Bérard, B. Bollig, M. Lehaut, N. Sznajder. Parameterized Synthesis for Fragments of First-Order Logic Over Data Words. In Proceedings of FoSSaCS 2020, pages 97-118, 2020. [ bib ]
[37] B. Barbot, B. Bérard, Y. Duplouy and S. Haddad. Integrating Simulink Models into the Model Checker Cosmos. In Proceedings of Petri Nets 2018, LNCS 10877, pages 363-373, Springer, 2018. [ bib ]
[36] B. Bérard, P. Bouyer and V. Jugé. Finite Bisimulations for Dynamical Systems with Overlapping Trajectories. In Proceedings of CSL 2018, LIPIcs 119, pages 26:1-26:17, 2018. [ bib ]
[35] B. Bérard, S. Haar and L. Hélouët. Hyper Partial Order Logic. In Proceedings of the 38th IARS Conf. on Foundations of Software and Theoretical Computer Science (FSTTCS 18), LIPIcs 122, pages 20:1-20:21, 2018. [ bib ]
[34] B. Bérard, S. Haddad and E. Lefaucheux. Probabilistic Disclosure: Maximisation vs. Minimisation. In Proceedings of the 37th IARS Conf. on Foundations of Software and Theoretical Computer Science (FSTTCS 17), LIPIcs 93, pages 13:1-13:14, 2017. [ bib ]
[33] B. Bérard, S. Haar, S. Schwoon and S. Schmitz. The Complexity of Diagnosability and Opacity Verification for Petri Nets. In Proceedings of the 38th Int. Conf. on Applications and Theory of Petri Nets and Concurrency (Petri Nets 17), LNCS 10258, pages 200-220, 2017. [ bib ]
[32] B. Bérard, O. Kouchnarenko, J. Mullins, and M. Sassolas. Preserving Opacity on Interval Markov Chains under simulation. In Proceedings of the 13th Workshop on Discrete Event Systems (WODES'16), IEEE, pages 319-324, 2016. [ bib |
[31] B. Bérard, S. Haddad, C. Picaronny, M. Safey El Din, and M. Sassolas. Polynomial Interrupt Timed Automata. In Proceedings of the 9th Workshop on Reachability Problems in Computational Models (RP'15), LNCS 9328, pages 20-32, 2015. [ bib ]
[30] B. Bérard, L. Hélouët, and J. Mullins. Non-interference in partial order models. In Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD'15), pages 80-89, 2015. [ bib ]
[29] M. Benabdelafid, B. Bérard, and M. Boufaida. Analyzing Behavioral Compatibility for Web Service Choreography Using Colored Petri Nets and ASK-CTL. In Proceedings of the 6th International Conference on Advanced Service Computing, pages 32-39, Xpert Publishing Services, 2014. [ bib ]
[28] B. Bérard, and O. Carton. Channel Synthesis Revisited. In Proceedings of the 8th International Conference on Languages and Automata Theory (LATA'14), volume 8370 of Lecture Notes in Computer Science, pages 149-160. Springer, 2014. [ bib ]
[27] B. Bérard, S. Haddad, A. Jovanovič and D. Lime. Parametric Interrupt Timed Automata. In Proceedings of the 7th Workshop on Reachability Problems in Computational Models (RP'13), volume 8169 of Lecture Notes in Computer Science, pages 56-69, Uppsala, Sweden, September 2013. Springer. [ bib | pdf ]
[26] B. Bérard, S. Haddad, M. Sassolas, and N. Sznajder. Concurrent Games on VASS with Inhibition. In Proceedings of the 23rd Int. Conf. on Concurrency Theory (CONCUR'12), volume 5504 of Lecture Notes in Computer Science, pages 39-52, Newcastle, England, September 2012. Springer. [ bib |  pdf (long version)  | pdf ]
[25] G. Benattar, B. Bérard, D. Lime, J. Mullins, O. H. Roux, and M. Sassolas. Channel Synthesis for Finite Transducers. In Proceedings of the 13th Int. Conf. on Automata and Formal Languages (AFL'11), pages 79-92, Debrecen, Hungary, August 2011. [ bib | pdf ]
[24] Y. Thierry-Mieg, B. Bérard, F. Kordon, D. Lime, and O. H. Roux. Compositional Analysis of Discrete Time Petri nets. In 1st Workshop on Petri Nets Compositions (CompoNet 2011), volume 726, pages 17-31, Newcastle, UK, June 2011. CEUR. [ bib | pdf ]
[23] B. Bérard, J. Mullins, and M. Sassolas. Quantifying Opacity. In Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST'10), pages 263-272, September 2010. [ bib | pdf ]
[22] B. Bérard, S. Haddad, and M. Sassolas. Real Time Properties for Interrupt Timed Automata. In Proceedings of the 17th International Symposium on Temporal Representation (TIME'10), pages 69-76. IEEE Computer Society Press, September 2010. [ bib | pdf ]
[21] Y. Zhang, B. Bérard, F. Kordon, and Y. Thierry-Mieg. Automated Controllability and Synthesis with Hierarchical Set Decision Diagrams. In Proceedings of the 10th International Workshop on Discrete Event Systems (WODES'10), pages 291-296, August 2010. [ bib ]
[20] B. Bérard and S. Haddad. Interrupt Timed Automata. In Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), volume 5504 of Lecture Notes in Computer Science, pages 197-211, York, GB, March 2009. Springer. [ bib | pdf ]
[19] B. Bérard, S. Haddad, L. M. Hillah, F. Kordon, and Y. Thierry-Mieg. Collision Avoidance in Intelligent Transport Systems: towards an Application of Control Theory. In Proceedings of the 9th International Workshop on Discrete Event Systems (WODES'08), pages 346-351, Göteborg, Sweden, May 2008. IEEE Press. [ bib ]
[18] H. Bel mokadem, B. Bérard, P. Bouyer, and F. Laroussinie. Timed temporal logics for abstracting transient states. In Susanne Graf and Wenhui Zhang, editors, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of Lecture Notes in Computer Science, pages 337-351, Beijing, ROC, October 2006. Springer. [ bib | pdf ]
[17] B. Bérard, P. Gastin, and A. Petit. Refinements and abstractions of signal-event (timed) languages. In E. Asarin and P. Bouyer, editors, Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06), volume 4202 of Lecture Notes in Computer Science, pages 67-81, Paris, France, September 2006. Springer. [ bib | pdf ]
[16] B. Bérard, P. Gastin, and A. Petit. Intersection of regular signal-event (timed) languages. In E. Asarin and P. Bouyer, editors, Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06), volume 4202 of Lecture Notes in Computer Science, pages 52-66, Paris, France, September 2006. Springer. [ bib | pdf ]
[15] B. Bérard, F. Cassez, S. Haddad, D. Lime, and O.H. Roux. When are timed automata weakly timed bisimilar to time Petri nets ? In 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005), volume 3821 of Lecture Notes in Computer Science, Hyderabad, India, December 2005. Springer. [ bib | pdf ]
[14] B. Bérard, F. Cassez, S. Haddad, D. Lime, and O.H. Roux. Comparison of different semantics for time Petri nets. In Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 293-307, Taipei, Taiwan, October 2005. Springer. [ bib | pdf ]
[13] B. Bérard, F. Cassez, S. Haddad, O.H. Roux, and D. Lime. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In P. Pettersson and W. Yi, editors, Proceedings of the third International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'05), volume 3829 of Lecture Notes in Computer Science, pages 211-225, Uppsala, Sweden, September 2005. Springer. [ bib | pdf ]
[12] H. Bel Mokadem, B. Bérard, V. Gourcuff, J.-M. Roussel, and O. de Smet. Verification of a timed multitask system with Uppaal. In Proceedings of the 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'05), pages 347-354, Catania, Italy, September 2005. IEEE Industrial Electronics Society. [ bib | pdf ]
[11] H. Bel Mokadem, B. Bérard, P. Bouyer, and F. Laroussinie. A new modality for almost everywhere properties in timed automata. In M. Abadi and L. de Alfaro, editors, Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science, pages 110-124, San Francisco, CA, USA, August 2005. Springer. [ bib | pdf ]
[10] B. Bérard, A. Labroue, and Ph. Schnoebelen. Verifying performance equivalence for Timed Basic Parallel Processes. In J. Tiuryn, editor, Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2000), volume 1784 of Lecture Notes in Computer Science, pages 35-47, Berlin, Germany, March 2000. Springer. [ bib | ps.gz ]
[9] J. Beauquier, B. Bérard, and L. Fribourg. A new rewrite method for proving convergence of self-stabilizing systems. In P. Jayanti, editor, Proceedings of the 13th International Symposium on Distributed Computing (DISC'99), volume 1693 of Lecture Notes in Computer Science, pages 240-253, Bratislava, Slovak republic, September 1999. Springer. [ bib | ps.gz ]
[8] B. Bérard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In Jos C. M. Baeten and Sjouke Mauw, editors, Proceedings of the 10th International Conference on Concurrency Theory (CONCUR'99), volume 1664 of Lecture Notes in Computer Science, pages 178-193, Eindhoven, The Netherlands, August 1999. Springer. [ bib | ps.gz ]
[7] B. Bérard and L. Fribourg. Automated verification of a parametric real-time program: The ABR conformance protocol. In N. Halbwachs and D. Peled, editors, Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science, pages 96-107, Trento, Italy, July 1999. Springer. [ bib | ps.gz ]
[6] B. Bérard and C. Picaronny. Accepting Zeno words without making time stand still. In I. Prívara and P. Ruzicka, editors, Proceedings of the 22nd International Symposium on Mathematical Fundations of Computer Science (MFCS'97), volume 1295 of Lecture Notes in Computer Science, pages 149-158, Bratislava, Slovakia, August 1997. Springer. [ bib | ps.gz ]
[5] B. Bérard, P. Gastin, and A. Petit. On the power of non-observable actions in timed automata. In C. Puech and R. Reischuk, editors, Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science (STACS'96), volume 1046 of Lecture Notes in Computer Science, pages 257-268, Grenoble, France, February 1996. Springer. [ bib | ps.gz ]
[4] B. Bérard. Static control through the serializability of concurrent programs. In Proceedings IMACS, Symp. on Modelling and Control of Technological Systems, Lille, pages 653-658, 1991. [ bib ]
[3] B. Bérard and L. Thimonier. On a concurrency measure. In Proceedings of the 2nd Int. Symp. on Computer and Information Science, Istanbul, pages 211-225, 1987. [ bib ]
[2] B. Bérard and J. Beauquier. On the equivalence of synchronization sets. In Proceedings of CAAP'86, Nice, volume 214 of Lecture Notes in Computer Science, pages 17-29. Springer, 1986. [ bib ]
[1] B. Bérard. Closure properties of some families of languages under literal shuffle. In Proceedings of the 4th Hungarian Computer Science Conf., Györ, pages 3-13, 1985. [ bib ]

Miscellanous

[18] B. Bérard, and O. Carton. Channel Synthesis Revisited, Research Report, October 2013. [ bib | .pdf ]
[17] B. Bérard, J. Mullins, and M. Sassolas. Research Report on Quantifying Opacity, December 2010. [ bib | .pdf ]
[16] G. Benattar, B. Bérard, D. Lime, J. Mullins, O. (H.) Roux, and M. Sassolas. Covert Channels with Transducers. In Proceedings of the LICS Workshop on Foundations of Computer Security (FCS'09), Los Angeles, California, USA, August 2009. [ bib | .pdf ]
[15] B. Bérard and S. Haddad. Interrupt Timed Automata: a step further. Technical Report LSV-09-1, Lab. Specification and Verification, ENS de Cachan, Cachan, France, January 2009. 24 pages. [ bib | .pdf ]
[14] M. Ben Gaid, B. Bérard, and O. De Smet. Modélisation et vérification d'un évaporateur en Uppaal. In J. Julliand, editor, Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 223-238, Besançon, France, June 2004. [ bib | .ps.gz ]
[13] B. Bérard and F. Laroussinie. Vérification compositionnelle des p-automates. Contract Report (Lot 4.1 fourniture 1), Projet RNTL Averroes, November 2003. 16 pages. [ bib ]
[12] B. Bérard, P. Bouyer, and A. Petit. Une analyse du protocole PGM avec UPPAAL. In D. Méry, N. Rezg, and X. Xie, editors, Actes du 4ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'03), pages 415-430, Metz, France, October 2003. Hermès. [ bib | .ps.gz ]
[11] B. Bérard, P. Bouyer, and A. Petit. Analysing the PGM protocol with UPPAAL. In P. Petterson and W. Yi, editors, Proceedings of the 2nd Workshop on Real-Time Tools (RT-TOOLS'02), Copenhagen, Denmark, August 2002. Uppsala University. [ bib | .ps.gz ]
[10] B. Bérard. Vérification de modèles temporisés. Mémoire d'habilitation, Université Paris 7, Paris, France, April 2002. [ bib | .ps.gz ]
[9] B. Bérard, P. Bouyer, and A. Petit. Modélisation du protocole PGM et de certaines de ses propriétés en UPPAAL. Contract Report 4.4, projet RNRT Calife, November 2001. 18 pages. [ bib ]
[8] B. Bérard, P. Castéran, E. Fleury, L. Fribourg, J.-F. Monin, Christine P., A. Petit, and D. Rouillard. Document de spécification du modèle commun. Fourniture 1.1 du projet RNRT Calife, April 2000. [ bib ]
[7] B. Bérard and L. Sierra. Comparing verification with HyTech, Kronos and Uppaal on the railroad crossing example. Research Report LSV-00-2, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2000. [ bib | .ps ]
[6] B. Bérard, G. Cécé, C. Dufourd, A. Finkel, F. Laroussinie, A. Petit, Ph. Schnoebelen, and G. Sutre. Le model-checking, une technique de vérification en plein essor. II - Quelques outils. Contract report, EDF/DER/MOS - LSV, October 1998. [ bib ]
[5] B. Bérard, M. Bidoit, and A. Petit. Recommandations sur le cahier des charges SRC. Contract report, EDF/DER/MOS - LSV, 1998. [ bib ]
[4] B. Bérard and M. Bidoit. Contribution du LSV à l'opération 2 « étude de cas SRIC ». Contract report, Action FORMA, October 1997. [ bib ]
[3] B. Bérard, P. Gastin, and A. Petit. Refinement and abstraction for timed languages. Research Report LSV-97-3, Laboratoire Spécification et Vérification, ENS Cachan, France, April 1997. [ bib | .ps ]
[2] B. Bérard. Sérialisabilité de programmes parallèles avec boucles. In Fondements du Parallélisme : Actes du 1er Congrès Biennal de l'AFCET, pages 121-130, Versailles, France, June 1993. AFCET. [ bib ]
[1] B. Bérard. Shuffle littéral, étude formelle et applications. Thèse de troisième cycle, Université Paris 7, May 1985. [ bib ]