Abstract nested Hoare triples for modular specification of safety and liveness properties of the I/O behaviour of programs

Add to your list(s) Download to your calendar using vCal

• Bart Jacobs (KU Leuven)
• Wednesday 06 July 2022, 13:30-14:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

How can one assign Hoare logic specifications to I/O APIs in an abstract, composable, and scalable way? At FTfJP 2019, we proposed abstract nested Hoare triples for this purpose. Furthermore, at ISoLA 2020, we proposed a way to encode arbitrary liveness properties of I/O behavior into this specification approach. In this talk, we give an overview of this line of work.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.