Michel Bidoit, María Victoria Cengarle, and Rolf Hennicker. Proof systems for structured specifications and their refinements. In Egidio Astesiano, Hans-Jörg Kreowski, and Bernd Krieg-Brückner, editors, Algebraic Foundations of Systems Specification, pages 385–433. Springer, Berlin, 1999.
M. Bidoit and R. Hennicker. Observer complete definitions are behaviourally coherent. Technical report, Ludwig-Maximilians-Universität München, Institut für Informatik, 1999.
M. Bidoit, R. Hennicker, F. Tort, and M. Wirsing. Correct realizations of interface constraints with ocl. In R. B. France and B. Rumpe, editors, UML'99, The Unified Modeling Language - Beyond the Standard, volume 1723 of Lecture Notes in Computer Science, pages 399–415, Berlin, 1999. Springer-Verlag.
R. Hennicker and M. Bidoit. Observational logic. In Proc. AMAST '98, 7th International Conference on Algebraic Methodology and Software Technology, volume 1548 of Lecture Notes in Computer Science, pages 263–277, Berlin, 1999. Springer.
R. Hennicker and A. Kurz. /omega-/xsi logic: On the algebraic extension of coalgebraic specifications. In Proc. CMCS '99, Coalgabraic Methods in Computer Science, volume 19 of Electronic Notes in Theoretical Computer Science, pages 195–212. Elsevier Science B.V., 1999.
M. Bidoit and R. Hennicker. Modular correctness proofs of behavioural implementations. Acta Informatica, 35:951–1005, 1998.
R. Hennicker. Structured specifications with behavioural operators: semantics, proof methods and applications. Habilitation thesis, Computer Science Institute, LMU Munich, 1997.
R. Hennicker and M. Wirsing. Proof systems for structured algebraic specifications: An overview. In Proc. FCT '97, Fundamentals of Computation Theory, volume 1279 of Lecture Notes in Computer Science, pages 19–37, Berlin, 1997. Springer.
Michel Bidoit and Rolf Hennicker. Behavioural Theories and The Proof of Behavioural Properties. Theoretical Computer Science, 165 (1):3–55, 1996.
Rolf Hennicker, Martin Wirsing, and Michel Bidoit. Proof systems for structured specifications with observability operators. Theoretical Computer Science, 1996. to appear.