Local Temporal Reasoning

I will discuss our recent development of the first method for proving temporal logic properties of programs written in higher-order languages such as C#, F#, Haskell, Ocaml, Perl, Ruby, Python, etc. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties, for example when using dependent (refinement) types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for interprocedural programs.

Joint work with Tachio Terauchi. To appear in LICS 2014.

Speaker Details

Eric Koskinen’s research is centered around developing mathematical techniques which improve the safety and performance of software, and applying those techniques to realistic computer systems. He is currently a PhD candidate at the University of Cambridge, under the supervision of Dr. Byron Cook and Prof. Michael Gordon. Eric was awarded the Gates Cambridge Scholarship, completed an Sc.M from Brown University where he worked with Maurice Herlihy, interned thrice at Microsoft Research, and previously spent three years as a software engineer at Amazon.com.

Date:
Speakers:
Eric Koskinen
Affiliation:
New York University
    • Portrait of Jeff Running

      Jeff Running