TY - GEN
T1 - Local temporal reasoning
AU - Koskinen, Eric
AU - Terauchi, Tachio
PY - 2014
Y1 - 2014
N2 - We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. 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 using 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 procedural programs.
AB - We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. 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 using 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 procedural programs.
KW - Formal verification
KW - Higher-order programs
KW - Model checking
KW - Program analysis
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=84905977424&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84905977424&partnerID=8YFLogxK
U2 - 10.1145/2603088.2603138
DO - 10.1145/2603088.2603138
M3 - Conference contribution
AN - SCOPUS:84905977424
SN - 9781450328869
T3 - Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
BT - Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014
T2 - Joint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014
Y2 - 14 July 2014 through 18 July 2014
ER -