Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, conditional equivalence in program transformations, etc. How might one reason about such relational properties? The talk reports on current investigations of 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.

The discussion following this talk will be moderated by Yu David Liu.

Anindya is a Program Director at the National Science Foundation in the CISE Directorate in the Division of Computing and Communication Foundations (CCF) where he focuses on the issues of Software and Hardware Foundations; Exploiting Parallelism for Scalability; Cyber-physical Systems; Research Experience for Undergraduates; CISE Research Initiation Initiatives. Banerjee’s research interests span software security, software verification, probabilistic programming, semantics and logics of programs, abstract interpretation, program analysis and program transformation. He received his Ph.D. from Kansas State University, USA, in 1995. After his Ph.D., Anindya was a postdoctoral researcher, first in the Labaratoire d’Informatique (LIX) of Ecole Polytechnique, Paris and subsequently at the University of Aarhus. He joined the IMDEA Software Institute in February 2009 as Full Professor. Immediately prior to this position, Anindya was Full Professor of Computing and Information Sciences at Kansas State University, USA. He was an Academic Visitor in the Advanced Programming Tools group, IBM T. J. Watson Research Center in 2007 and a Visiting Researcher in the Programming Languages and Methodology group at Microsoft Research in 2007–2008. He was a recipient of the Career Award of the US National Science Foundation in 2001.