Quentin Carbonneaux
PhD Student, Yale
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.
Thursday, December 3, 2015
2:00 PM
Gates
& Hillman Centers 8102
Principles
of Programming Seminars