|
2024 Book Chapter Practical rely/guarantee verification of an efficient lock for seL4 on multicore architecturesColvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa and Su, Roger C. (2024). Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures. The practice of formal methods: essays in honour of Cliff Jones, Part I. (pp. 65-87) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66676-6_4 |
|
2024 Book Chapter Reasoning about distributive laws in a concurrent refinement algebraMeinicke, Larissa A. and Hayes, Ian J. (2024). Reasoning about distributive laws in a concurrent refinement algebra. The practice of formal methods: essays in honour of Cliff Jones, part II. (pp. 1-22) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66673-5_1 |
|
2023 Book Chapter Trace Models of Concurrent Valuation AlgebrasEvangelou-Oost, Naso, Meinicke, Larissa, Bannister, Callum and Hayes, Ian J. (2023). Trace Models of Concurrent Valuation Algebras. Formal Methods and Software Engineering. (pp. 118-136) Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_8 |
|
2023 Book Chapter Specifying and reasoning about shared-variable concurrencyHayes, Ian J., Jones, Cliff B. and Meinicke, Larissa A. (2023). Specifying and reasoning about shared-variable concurrency. Theories of programming and formal methods: essays dedicated to Jifeng He on the occasion of his 80th birthday. (pp. 110-135) edited by Jonathan P. Bowen, Qin Li and Qiwen Xu. Cham, Switzerland: Springer. doi: 10.1007/978-3-031-40436-8_5 |
|
2021 Book Chapter Software specificationHayes, Ian J. and King, Steve (2021). Software specification. Theories of programming: the life and works of Tony Hoare. (pp. 251-270) edited by Cliff B. Jones and Jayadev Misra. New York, NY USA: Association for Computing Machinery. doi: 10.1145/3477355.3477367 |
|
2009 Book Chapter Dynamically detecting faults via integrity constraintsHayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. Methods, Models, and Tools for Fault Tolerance. (pp. 85-103) edited by Michael Butler, Cliff Jones, Alexander Romanovsky and Elena Troubitsyna. Berlin, Germany: Springer Verlag. doi: 10.1007/978-3-642-00867-2_5 |
|
2007 Book Chapter Deriving specifications for systems that are connected to the physical worldJones, C. B., Hayes, I. J. and Jackson, M. A. (2007). Deriving specifications for systems that are connected to the physical world. Formal Methods and Hybrid Real-Time Systems. (pp. 364-390) edited by Jones, C. B., Liu, Z. and Woodcock, J.. Berlin, Germany: Springer-Verlag. doi: 10.1007/978-3-540-75221-9_16 |
|
2004 Book Chapter Developing logic programs from specifications using stepwise refinementColvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray and Strooper, Paul (2004). Developing logic programs from specifications using stepwise refinement. Program Development in Computational Logic. (pp. 66-89) edited by Maurice Bruynooghe and Kunk-Kiu Lau. Berlin: Springer Verlag. doi: 10.1007/978-3-540-25951-0_3 |
|
2003 Book Chapter A predicative semantics for real-time refinementHayes, I. J. (2003). A predicative semantics for real-time refinement. Programming Methodology. (pp. 109-133) edited by A. McIver and C. Morgan. New York: Springer Verlag. doi: 10.1007/978-0-387-21798-7_6 |
|
1999 Book Chapter Specifications are not (necessarily) executableHayes, I. J. and Jones, C. B. (1999). Specifications are not (necessarily) executable. High-integrity system specification and design. (pp. 563-581) edited by J. P. Bowen and M. G. Hinchey. London: Springer. |
|
1998 Book Chapter Deadlines are terminationHayes, I. J. and Utting, M. (1998). Deadlines are termination. Programming Concepts and Methods PROCOMET ’98. (pp. 186-204) Boston, MA, United States: Springer. doi: 10.1007/978-0-387-35358-6_15 |
