[talks] Joey Dodds will present his FPO "Computation Improves Interactive Symbolic Execution" on Thursday, 9/10/2015 at 10am in CS 302

Nicki Gotsis ngotsis at CS.Princeton.EDU
Tue Sep 1 09:40:50 EDT 2015


Joey Dodds will present his FPO, "Computation Improves Interactive Symbolic Execution," on Thursday, 9/10/2015 at 10:00 AM, CS 302.

The members of his committee are: Andrew Appel (adviser); Readers: David Walker, Jesper Bengtson(IT University of Copenhagen); Nonreaders: Sharad Malik, Aarti Gupta

A copy of his thesis is available in Room 310.

Everyone is invited to attend his talk. The talk title and abstract follow below:
________________________________________________________

"Computation Improves Interactive Symbolic Execution"

As it becomes more prevalant throughout our lives, correct software is more important than it has ever
been before. Verifiable C is an expressive Hoare logic (higher-order impredicative concurrent separation
logic) for proving functional correctness of C programs. The program logic is foundational—it is proved
sound in Coq w.r.t. the operational semantics of CompCert Clight. Users apply the program logic to C
programs using semiautomated tactics in Coq, but these tactics are very slow.
This thesis shows how to make an efficient (yet still foundational) symbolic executor based on this
separation logic by using computational reflection in several different ways. Our execution engine is able to
interact gracefully with the user by reflecting application-specific proof goals back to the user for interactive
proof—necessary in functional correctness proofs where there is almost always domain-specific reasoning
to be done. We use our “mostly sound” type system, computationally efficient finite-map data structures,
and the MirrorCore framework for computationally reflected logics. Measurements show a 40× performance
improvement.


More information about the talks mailing list