Local Temporal Reasoning

Опубликовано 21 июня 2016, 21:25

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.