Ib Holm Sørensen

Ib Holm Sørensen (29 January 1949 – 17 January 2012) was a Danish computer scientist who contributed to the early development and use of formal methods for specifying software systems and modules, especially around the Z notation and the B-Method. He worked in both academia and industry.

Sørensen was born in Aabenraa, Denmark, and started his academic career in the 1970s at Aarhus University, where he worked on Rikke-Mathilda micro-assemblers and simulators on a DECSystem-10 computer.

Career

In 1979, Sørensen joined the Programming Research Group (PRG), part of the Oxford University Computing Laboratory (now Oxford University's Department of Computer Science) in England, under the direction of Prof. Tony Hoare. There he worked with Jean-Raymond Abrial, Bernard Sufrin, and others in the early development of the formal specification language Z. He received a DPhil degree from Oxford University in 1981. He taught early courses in Z notation at Oxford.

Ib Sørensen was the head of the Transaction Processing Project at Oxford from its inception in 1982 (later renamed the "CICS Project"), in collaboration with IBM Hursley. The project formally specified parts of IBM's CICS transaction processing software using Z notation. This won a UK national Queen's Award for Technological Achievement in 1992. As part of the CICS project, he extended Edsger Dijkstra's Guarded Command Language by allowing the use of Z-schema notation as abstract commands. These IDeaS were later formalized by Carroll Morgan in his refinement calculus.

In 1985 Sørensen established the Z Users Meeting series at Rewley House in Oxford, which has continued to this day as the international ABZ Conference. He also co-authored the seminal Specification Case Studies book on the use of Z, first published in 1987 (second edition published in 1993).

From the late 1980s, Sørensen was central to the development of the B-Method, one of the leading formal methods. He left Oxford University to lead a team for BP Research to develop the B-toolkit to provide tool support for the B-method. He then founded the company B-Core (UK) Limited (now defunct) to support the B-Toolkit, which is a collection of programming tools designed to support the use of the B notation, and he helped to complete a number of B-related projects.

Later, Sørensen returned to Oxford University. From 1999, he worked on the B-based Booster models of requirements. He died in 2012 before he could retire.

Selected publications

Ib Holm Sørensen co-authored the following:

• Ib Holm Sørensen, Eric Kressel (1975). A proposal for a multi-programming BCPL system on RIKKE-1 (in Danish). Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Eric Kressel, Ib Holm Sørensen (1975). The first BCPL system on RIKKE-1. Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Eric Kressel, Ib Holm Sørensen (1975). The Mathilda driver, a software tool for hardware testing (in Danish). Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Ib Holm Sørensen, Eric Kressel (1977). DAIMI MD: RIKKE-MATHILDA microassemblers and simulators on the DECsystem 10. Vol. 28. Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Ib Holm Sørensen (1978). DAIMI PB: System Modelling: a Methodology for Describing the Structure of Complex Software, Firmware and Hardware Systems Consisting of Independent Process Components. Vol. 87. Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Jens Kristian Kjærgård, Ib Holm Sørensen (1980). DAIMI MD: BCPL on RIKKE (in Danish). Vol. 36. Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Jens Kristian Kjærgård, Ib Holm Sørensen (1980). DAIMI MD: The RIKKE Editor (in Danish). Vol. 37. Denmark: Department of Mathematics. Department of Computer Science, Aarhus University.
• Ib Holm Sørensen (1981). DAIMI PB: Specification and Design of Distributed Systems. Denmark: Aarhus University.
• Ib Holm Sørensen (1981). Topics in program specification and design: specification and design of distributed systems. DPhil thesis. UK: Wolfson College, University of Oxford.
• Bill Flinn, Ib Holm Sørensen (1985). CAVIAR: A Case Study in Specification. UK: Programming Research Group, Oxford University Computing Laboratory.
• C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sørensen, J. M. Spivey, B. A. Sufrin (August 1987). "Laws of programming". Communications of the ACM. 30 (8): 672–686. .
• Steve King, Ib Holm Sørensen, J. C. P. Woodcock (1988). Z: Grammar and Concrete and Abstract Syntaxes (Version 2.0). UK: Programming Research Group, Oxford University Computing Laboratory.
• J.-R. Abrial, M. K. O. Lee, D. S. Neilson, P. N. Scharbach, I. H. Sørensen (1991). "The B-method". In S. Prehn, H. Toetenel (ed.). VDM '91 Formal Software Development Methods. Lecture Notes in Computer Science. Vol. 552. Berlin, Heidelberg: Springer. pp. 398–405. . .
• Bill Flynn, Roger Gimon, Steve King, Carroll Morgan, Ib Holm Sørensen, Bernard Surfrin (1993). Ian Hayes (ed.). Specification Case Studies . International Series in Computer Science (2nd ed.). Prentice Hall. . (1st ed., 1987.)

External links

• Oxford home page
• Ib Holm Sørensen on the DBLP Bibliography Server

• Ib Holm Sørensen on ResearchGate