Selected publications by Michel Bidoit

2010

• Sebastian S. Bauer, Rolf Hennicker and Michel Bidoit.  A Modal Interface Theory with Data Constraints.  In SBMF'10, LNCS 6527, pages 80-95. Springer, 2010. ( PDF | BibTeX + Abstract )

2008

• Michel Bidoit and Rolf Hennicker.  An Algebraic Semantics for Contract-Based Software Components.  In AMAST'08, LNCS 5140, pages 216-231. Springer, 2008. ( BibTeX + Abstract )
• Michel Bidoit, Donald Sannella and Andrzej Tarlecki.  Observational Interpretation of Casl Specifications.  Mathematical Structures in Computer Science 18(2), pages 325-371, 2008. ( PDF | BibTeX + Abstract )

2006

• Michel Bidoit and Rolf Hennicker.  Proving Behavioral Refinements of COL-Specifications.  In Algebra, Meaning and Computation, LNCS 4060, pages 333-354. Springer, 2006. ( PDF | BibTeX + Abstract )
• Michel Bidoit and Rolf Hennicker.  Constructor-Based Observational Logic.  Journal of Logic and Algebraic Programming 67(1-2), pages 3-51, 2006. ( PDF | BibTeX + Abstract )

2005

• Michel Bidoit and Rolf Hennicker.  Externalized and Internalized Notions of Behavioral Refinement.  In ICTAC'05, LNCS 3722, pages 334-350. Springer, 2005. ( PDF | BibTeX + Abstract )

2004

• Michel Bidoit and Peter D. Mosses.  CASL User Manual - Introduction to Using the Common Algebraic Specification Language, LNCS 2900. Springer, 2004. ( Web page | BibTeX )
• Michel Bidoit, Donald Sannella and Andrzej Tarlecki.  Toward Component-Oriented Formal Software Development: An Algebraic Approach.  In RISSEF'02, LNCS 2941, pages 75-90. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX )
• Michel Bidoit, Rolf Hennicker, Alexander Knapp and Hubert Baumeister.  Glass-Box and Black-Box Views on Object-Oriented Specifications.  In SEFM'04, pages 208-217. IEEE Computer Society Press, 2004. ( PDF | BibTeX )

2003

• Michel Bidoit, Rolf Hennicker and Alexander Kurz.  Observational Logic, Constructor-Based Logic, and their Duality.  Theoretical Computer Science 298(3), pages 471-510, 2003. ( PS | PS.GZ | BibTeX )

2002

• Rolf Hennicker, Heinrich Hußmann and Michel Bidoit.  On the Precise Meaning of OCL Constraints.  In Object Modeling with the OCL - The Rationale behind the Object Constraint Language, LNCS 2263, pages 69-84. Springer, 2002. ( PS | PS.GZ | BibTeX )
• Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Bernd Krieg-Brückner, Peter D. Mosses, Donald Sannella and Andrzej Tarlecki.  CASL: The Common Algebraic Specification Language.  Theoretical Computer Science 286(2), pages 153-196, 2002. ( PS | PS.GZ | BibTeX )
• Michel Bidoit, Donald Sannella and Andrzej Tarlecki.  Global Development via Local Observational Construction Steps.  In MFCS'02, LNCS 2420, pages 1-24. Springer, 2002. Invited paper. ( PS | PS.GZ | BibTeX )
• Michel Bidoit, Donald Sannella and Andrzej Tarlecki.  Architectural Specifications in CASL.  Formal Aspects of Computing 13(3-5), pages 252-273, 2002. ( PS | PS.GZ | BibTeX )
• Michel Bidoit and Rolf Hennicker.  On the Integration of Observability and Reachability Concepts.  In FoSSaCS'02, LNCS 2303, pages 21-36. Springer, 2002. ( PS | PS.GZ | BibTeX )

2001

• Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci and Philippe Schnoebelen.  Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001. ( Web page | BibTeX )
• Michel Bidoit and Alexandre Boisseau.  Algebraic Abstractions.  In WADT'01, LNCS 2267, pages 21-47. Springer, 2001. ( PS | PS.GZ | BibTeX )
• Michel Bidoit, Rolf Hennicker and Alexander Kurz.  On the Duality between Observability and Reachability.  In FoSSaCS'01, LNCS 2030, pages 72-87. Springer, 2001. ( PS | PS.GZ | BibTeX )
• Michel Bidoit and Peter D. Mosses.  A Gentle Introduction to CASL v1.0.1, Invited tutorial, CoFI Workshop at the 4th European Joint Conferences on Theory and Practice of Software (ETAPS 2001), Genova, Italy, 2001. ( Web page | BibTeX )

1999

• Michel Bidoit, María Victoria Cengarle and Rolf Hennicker.  Proof systems for structured specifications and their refinements.  In Algebraic Foundations of Systems Specification, chapter 11, pages 385-433. Springer, 1999. ( PS | PS.GZ | BibTeX )
• Michel Bidoit, Rolf Hennicker, Françoise Tort and Martin Wirsing.  Correct Realization of Interface Constraints with OCL.  In UML'99, LNCS 1723, pages 399-415. Springer, 1999. ( PS | PS.GZ | BibTeX )
• Michel Bidoit and Rolf Hennicker.  Observer Complete Definitions are Behaviourally Coherent.  In FM'99, pages 83-94. Theta, Bucharest, Romania, 1999. ( PS | PS.GZ | BibTeX )
• Philippe Schnoebelen, Béatrice Bérard, Michel Bidoit, François Laroussinie and Antoine Petit.  Vérification de logiciels : techniques et outils du model-checking. Vuibert, 1999. ( Web page | BibTeX )
• Michel Bidoit, Donald Sannella and Andrzej Tarlecki.  Architectural Specifications in CASL.  In AMAST'98, LNCS 1548, pages 341-357. Springer, 1999. ( PDF | PS | PS.GZ | BibTeX )
• Rolf Hennicker and Michel Bidoit.  Observational Logic.  In AMAST'98, LNCS 1548, pages 263-277. Springer, 1999. ( PS | PS.GZ | BibTeX )

1998

• Michel Bidoit and Rolf Hennicker.  Modular Correctness Proofs of Behavioural Implementations.  Acta Informatica 35(11), pages 951-1005, 1998. ( BibTeX )

1997

• Michel Bidoit, Christine Pellen and Jérôme Ryckbosch.  Plan de Défense - Formalisation du cahier des charges du Point Central à l'aide de spécifications algébriques.  In Application des techniques formelles au logiciel, ARAGO 20, chapter 7, pages 123-132. Observatoire Français des Techniques Avancées, 1997. ( BibTeX )
• Michel Bidoit and Max Dauchet (eds.).  Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development (TAPSOFT'97), Lille, France, April 1997, LNCS 1214. Springer. ( Web page | BibTeX )
• Rolf Hennicker, Martin Wirsing and Michel Bidoit.  Proof Systems for Structured Specifications with Observability Operators.  Theoretical Computer Science 173(2), pages 393-443, 1997. ( BibTeX )

1996

• Michel Bidoit, Christine Choppy and Frédéric Voisin.  Interchange Format for Inter-Operability of Tools and Translation, The SALSA and ASSPEGIQUE⁺/LP Experience.  In ADT'95, LNCS 1130, pages 102-124. Springer, 1996. ( PS | PS.GZ | BibTeX )
• Frédéric Voisin and Michel Bidoit.  Modular Algebraic Specifications and the Orientation of Equations into Rewrite Rules.  In ADT'95, LNCS 1130, pages 503-521. Springer, 1996. ( PS | PS.GZ | BibTeX )
• Michel Bidoit, Claude Chevenier, Christine Pellen and Jérôme Ryckbosch.  An Algebraic Specification of the Steam-Boiler Control System.  In Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, pages 79-108. Springer, 1996. ( PS | PS.GZ | BibTeX )
• Michel Bidoit and Rolf Hennicker.  Behavioural Theories and the Proof of Behavioural Properties.  Theoretical Computer Science 165(1), pages 3-55, 1996. ( PS | PS.GZ | BibTeX )
• Michel Bidoit and Andrzej Tarlecki.  Behavioural Satisfaction and Equivalence in Concrete Model Categories.  In CAAP'96, LNCS 1059, pages 241-256. Springer, 1996. ( PS | PS.GZ | BibTeX )

1995

• Michel Bidoit and Rolf Hennicker.  Behavioural Theories.  In ADT'94, LNCS 906, pages 153-169. Springer, 1995. ( PS | PS.GZ | BibTeX )
• Michel Bidoit, Rolf Hennicker and Martin Wirsing.  Behavioural and Abstractor Specifications.  Science of Computer Programming 25(2-3), pages 149-186, 1995. ( BibTeX )
• Michel Bidoit and Rolf Hennicker.  Proving the Correctness of Behavioural Implementations.  In AMAST'95, LNCS 936, pages 152-168. Springer, 1995. ( BibTeX )
• Michel Bidoit and Andrzej Tarlecki.  Regular Algebras: A Framework for Observational Specifications with Recursive Definitions.  Report LIENS-95-12, École Normale Supérieure, Paris, France, May 1995. ( BibTeX )
• Gilles Bernot, Michel Bidoit and Teodor Knapik.  Observational Specifications and the Indistinguishability Assumption.  Theoretical Computer Science 139(1-2), pages 275-314, 1995. ( BibTeX )

1994

• Gilles Bernot, Michel Bidoit and Teodor Knapik.  Behavioural Approaches to Algebraic Specifications: A Comparative Study.  Acta Informatica 31(7), pages 651-671, 1994. ( BibTeX )
• Michel Bidoit and Rolf Hennicker.  Proving Behavioural Theorems with Standard First-Order Logic.  In ALP'94, LNCS 850, pages 41-58. Springer, 1994. ( BibTeX )
• Michel Bidoit, Rolf Hennicker and Martin Wirsing.  Characterizing Behavioural Semantics and Abstractor Semantics.  In ESOP'94, LNCS 788, pages 105-119. Springer, 1994. ( BibTeX )

1993

• Michel Bidoit and Christine Choppy (eds.).  Recent Trends in Data Type Specification - Selected Papers of the 8th Workshop on Specification of Abstract Data Types (ADT'91), joint with the 3rd COMPASS Workshop, Dourdan, France, August 1991, LNCS 655. Springer-Verlag, 1993. ( Web page | BibTeX )
• Michel Bidoit and Rolf Hennicker.  How to Prove Observational Theorems with LP.  In Proceedings of the 1st International Workshop on Larch, Dedham, Massachusetts, USA, July 1992, Workshops in Computing, pages 18-35. Springer-Verlag, 1993. ( BibTeX )
• Christine Choppy and Michel Bidoit.  Integrating ASSPEGIQUE and LP.  In Proceedings of the 1st International Workshop on Larch, Dedham, Massachusetts, USA, July 1992, Workshops in Computing, pages 69-85. Springer-Verlag, 1993. ( BibTeX )
• Michel Bidoit and Rolf Hennicker.  A General Framework for Modular Implementations of Modular Systems.  In TAPSOFT'93, LNCS 668, pages 199-214. Springer, 1993. ( BibTeX )

1992

• Gilles Bernot and Michel Bidoit.  Proving the Correctness of Algebraically Specified Software: Modularity and Observability Issues.  In AMAST'91, Workshops in Computing, pages 216-242. Springer-Verlag, 1992. Invited paper. ( BibTeX )
• Michel Bidoit.  Development of Modular Specifications by Stepwise Refinements Using the PLUSS Specification Language.  In Proceedings of the IMA Conference on the Unified Computation Laboratory, Stirling, Scotland, UK, July 1990, pages 171-192. Oxford University Press, 1992. Invited paper. ( BibTeX )
• Gilles Bernot, Michel Bidoit and Teodor Knapik.  Towards an Adequate Notion of Observation.  In ESOP'92, LNCS 582, pages 39-55. Springer, 1992. ( BibTeX )

1991

• Michel Bidoit, Hans-Jörg Kreowski, Pierre Lescanne, Fernando Orejas and Donald Sannella (eds.).  Algebraic System Specification and Development, a Survey and Annotated Bibliography, LNCS 501. Springer-Verlag, 1991. ( Web page | BibTeX )

About LSV

• News
• People
• Research
• Seminars
• Teaching
• Contact

• École Normale Supérieure de Cachan
• Centre National de la Recherche Scientifique