TY - GEN
T1 - Relational logic with framing and hypotheses
AU - Banerjee, Anindya
AU - Naumann, David A.
AU - Nikouei, Mohammad
N1 - Publisher Copyright:
© Anindya Banerjee, David A. Naumann, and Mohammad Nikouei.
PY - 2016/12/1
Y1 - 2016/12/1
N2 - Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.
AB - Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.
KW - Frame conditions
KW - Product programs
KW - Program equivalence
KW - Region logic
KW - Relational Hoare logic
UR - http://www.scopus.com/inward/record.url?scp=85010792521&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85010792521&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSTTCS.2016.11
DO - 10.4230/LIPIcs.FSTTCS.2016.11
M3 - Conference contribution
AN - SCOPUS:85010792521
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 11.1-11.16
BT - 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016
A2 - Lal, Akash
A2 - Akshay, S.
A2 - Saurabh, Saket
A2 - Sen, Sandeep
A2 - Saurabh, Saket
T2 - 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016
Y2 - 13 December 2016 through 15 December 2016
ER -