PhD Student, Yale

Invariant Logics

Abstract:

I present a recent work on new semantics for Hoare Logic. Instead of using Hoare Logic to prove functional correctness, I recycle it to prove invariants true during the whole execution of a program. The pre-conditions are put forward and characterize the initial states allowing the program to execute safely (i.e. not break the invariant). The post-conditions now simply serve compositionality and allow modular reasoning. I will show on a trivial language how we define the semantic validity of Hoare triples in such a setting and how soundness and completeness of the logic are proved. Example applications of the described logic are the usual 'this program does not get stuck', but also the more interesting 'this program does not run out of memory'.

Bio:

Quentin is a fourth year PhD student working under Zhong Shao's supervision at Yale. He worked on tools and techniques for formal reasoning on the resource usage of computer programs. He does not like to talk about himself using the third person.

Principles
of Programming Seminars