Logic Summer School 2022

Some useful resources:

Hoare Logic and Rely/Guarantee Reasoning

1. de Roever, W.-P. Concurrency. Introduction to Compositional and Non-compositional Methods, Cambridge University Press, (2001). Chapter 9 introduces Hoare logic along with some good problems to work on. Rely/guarantee is also covered. This book is very useful.


2. Hayes, I.J. and Jones, C.B. A Guide to Rely/Guarantee Thinking, Engineering Trustworthy Software Systems (SETSS 2017), Lecture Notes in Computer Science, Vol.11174, pp.1-38, Springer, Cham., (2018). Download from Springer.


3. Jones, C. B. and Yatapanage, N. Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example, Formal Aspects of Computing. 31(3): 353-374. (2019). Download from Springer.


4. Jones, C.B. and Yatapanage, N. Reasoning about Separation using Abstraction and Reification, 13th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2015), Lecture Notes in Computer Science, Vol.9276, pp.3-19, Springer-Verlag, (2015). Download from Springer.

Also take a look at the references on Cliff B. Jones' page.

Model checking for automating failure analysis and related topics

1. Baier, C. and Katoen, J.-P. Principles of model checking. MIT Press. (2008).


2. Huth, M. and Ryan, M. D. Logic in computer science - modelling and reasoning about systems. Cambridge University Press. (2000).


3. Grunske, L., Winter, K., Yatapanage, N., Zafar, S. and Lindsay, P.A. Experience with Fault Injection Experiments for FMEA, Journal of Software: Practice and Experience. 41(11):1233-1258. (2011). Download from Wiley. See the tech reports and model checking results.


4. Grunske, L., Winter, K. and Yatapanage, N. Defining the Abstract Syntax of Visual Languages with Advanced Graph Grammars - A Case Study Based on Behavior Trees, Journal of Visual Languages and Computing. 19(3):343-379. (2008). Download from ScienceDirect.


5. Grunske, L., Lindsay, P., Yatapanage, N. and Winter, K. An Automated Failure Mode and Effect Analysis based on High-Level Design Specification with Behavior Trees, Integrated Formal Methods: 5th International Conference (IFM 2005), Proceedings. LNCS. Springer-Verlag, Vol.3771, pp.129-149, 2005. Download from Springer


6. Lindsay, P., Winter, K. and Yatapanage, N. Safety Assessment Using Behavior Trees and Model Checking, 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010), Proceedings. IEEE Computer Society, pp.181-190, 2010. Download from IEEE

Slides

1. Wednesday lecture 1 (Hoare logic).


2. Wednesday lecture 2 (Intro to Concurrency).


3. Thursday lectures. The slides cover three interesting applications where rely/guarantee was used. We'll also go through a simple example on the board. You'll also need references (3) and (4) above.


4. Friday lectures. To see the moving demonstration of the industrial metal press, look at the Powerpoint version in Slideshow view: Powerpoint version. These lectures were on LTL, CTL*, using model checking to automate failure analysis, using graph grammar rules to create a translator between a specification language and a model checker, and next-preserving branching bisimulation. Note that the graph grammar part is not on the slides; look at reference (4) in the model checking section above. We also looked at a demonstration of a tool which translates Behavior Tree specifications to a model checking language.