Prof. Dines Bjørner was made an ACM Fellow in 2005 "for contributions to formal methods and for international leadership". And he was made an IEEE Fellow in 2005 "for contributions to formal methods software development and its applications in industry". Prof. Bjørner was Professor of Computing Science at the Technical University of Denmark from 1976 to 2007. He worked at IBM R & D from 1962 to 1976, with pioneers such as Gene Amdahl, John Backus, E.F. Codd, et al., and at the IBM Laboratory in Vienna he was on the team that developed the Vienna Development Method (VDM), the first ISO standardised formal method. He was the cofounder and scientific director of the Dansk Datamatik Center (1979–1989), and led many European R & D projects, including work on the formal specification of a semantics for Ada, compilers for CHILL and Ada, and the RAISE Specification Language. During 1991–1997 he was the founding and first director of the UNU-IIST, the United Nations University International Institute for Software Technology in Macau. He has held guest professorships at Berkeley, Kiel University, Copenhagen University, the National University of Singapore, and JAIST (Japan Advanced Institute of Science and Technology). Among many honours, Prof. Bjørner is a member of the Academia Europaea, and a member of the Russian Academy of Natural Sciences; he has received the Masaryk Gold Medal (Masaryk University, Brno, Czech Republic) and the John von Neumann Medal (Hungarian Computer Society); and he is a Knight of the Danish Flag.

The basic principles and techniques of abstraction and modelling. This volume is suitable for university undergraduate students and college lecturers. First this volume provides a sound, but simple basis of insight into discrete mathematics: numbers, sets, Cartesians, types, functions, the Lambda Calculus, algebras, and mathematical logic. Then it teaches and trains its readers in basic property- and model-oriented specification principles and techniques. The model-oriented concepts that are common to such specification languages as B, VDM-SL, and Z are propagated here through the use of the RAISE specification language (RSL). Finally this volume covers the basic principles of functional, imperative, and parallel specification programming, the latter based on the use of CSP, Hoare's language of communicating sequential processes.

The basic principles and techniques of specifying systems and languages. [Vol. 1 of this series is a prerequisite text.] This volume is suitable for late undergraduate to early graduate university students, college lecturers, and researchers of programming methodologies.First this volume teaches and trains its readers in basic and advanced principles and techniques: hierarchical vs. compositional, denotational vs. computational, and configurational (abstracting and modelling contexts and states). Then it covers the basic principles and techniques of modelling the semiotics: pragmatics, semantics, and syntax of systems and languages. It then covers principles and techniques of modelling spatial and simple temporal phenomena, and such specialized topics as modularity (incl. UML class diagrams), Petri nets, live sequence charts, statecharts, and temporal logics, including the Duration Calculus. Finally this volume presents principles and techniques for developing the basis for sound, efficient interpreter and compiler development of functional, imperative, modular, and parallel programming languages.

The basic principles and techniques of overall software development, from domains via requirements to software designs, advocating a novel approach to software engineering based on the adage “Before requirements can be formulated one must understand the application domain.” There are two reading paths: focusing only on the informal parts, this volume targets undergraduate students in courses on software engineering and college lecturers in that field, while the full version of the volume targets advanced students, lecturers, and researchers. This volume is structured thus: from the principles and techniques for the development of domain descriptions, via principles and techniques for the derivation of requirements prescriptions from domain models, to principles and techniques for the refinement of requirements into software designs, i.e., architectures and component design. Emphasis in the coverage of domain and requirements engineering is on what goes into a proper domain description (resp., requirements prescription), how one acquires and analyzes the domain knowledge (resp., requirements expectations), and how one validates and verifies domain (resp., requirements) models.

The volumes are supported with comprehensive teaching slides, available to lecturers only. Please find the downloads attached to this page.

Please find here the author's guide to using Vols. 1-3.

Slides Volume 1

Slides Volume 2

Slides Volume 3

Title: Logics of Specification LanguagesSeries: EATCS Monographs in Theoretical Computer ScienceEditors: Dines Bjørner, Martin Henson Notes: 2008, 624 pp., ISBN 978-3-540-74106-0By a specification language we understand a formal system of syntax, semantics and proof rules. The syntax and semantics define a language; the proof rules define a proof system. Specifications are expressions in the language, and reasoning over properties of these specifications is done within the proof system. This book presents comprehensive studies on nine specification languages and their logics of reasoning.The editors and authors are authorities on these specification languages and their application. Dedicated chapters address: the use of ASM (Abstract State Machines) in the classroom; the Event-B modelling method; a methodological guide to CafeOBJ logic; CASL, the Common Algebraic Specification Language; the Duration Calculus; the logic of the RAISE specification language (RSL); the specification language TLA+; the typed logic of partial functions and the Vienna Development Method (VDM); and Z logic and its applications. Each chapter is self-contained, with references, and symbol and concept indexes. Finally, in a unique feature, the book closes with short commentaries on the specification languages written by researchers closely associated with their original development.With extensive references and pointers to future developments, this book will be of interest to researchers and graduate students engaged with formal specification languages.

Title: Formal Methods and Hybrid Real-Time Systems - Essays in Honour of Dines Bjørner and Zhou Chaochen on the Occasion of Their 70th BirthdaysSeries: Lecture Notes in Computer Science (LNCS 4700)Editors: Cliff Jones, Zhiming Liu, Jim Woodcock Notes: 2007, 539 pp., ISBN 978-3-540-75220-2This Festschrift volume honours both Dines Bjørner and Zhou Chaochen on the occasion of their 70th birthdays in October and November 2007. The volume includes 25 refereed papers by leading researchers, current and former colleagues who congregated at a celebratory symposium held in Macao, China during the Int. Colloq. on Theoretical Aspects of Computing (ICTAC 2007).

Dines Bjorner; Software Engineering; Abstraction and Modelling; Specification of Systems and Languages; Domains, Requirements, and Software Design; Formal Methods; Specification Languages; Event-B; CafeOBJ; CASL; Duration Calculus; RAISE; RSL; TLA+; VDM; Z Logic