Dependable Software Engineering. Theories, Tools, and Applications

s of Invited Talks General Lessons from a Rely/Guarantee Development Cliff B. Jones, Andrius Velykis, and Nisansala Yatapanage 1 School of Computing Science, Newcastle University, Newcastle upon Tyne, UK 2 School of Computer Science and Informatics, De Montfort University, Leicester, UK Abstract. Decomposing the design (or documentation) of large systems is a practical necessity; this prompts the need for a notion of compositional development methods; finding such methods for concurrent software is technically challenging because of the interference that characterises concurrency. This paper outlines the development of a difficult example in order to draw out lessons about such development methods. Although the “rely/guarantee” approach is employed in the example, the intuitions are more general. Decomposing the design (or documentation) of large systems is a practical necessity; this prompts the need for a notion of compositional development methods; finding such methods for concurrent software is technically challenging because of the interference that characterises concurrency. This paper outlines the development of a difficult example in order to draw out lessons about such development methods. Although the “rely/guarantee” approach is employed in the example, the intuitions are more general. Towards Verified Artificial Intelligence