Paper Info
Title
Product programs and relational program logics.
Abstract
A common theme in program verification is to relate two programs, for instance to show that they are equivalent, or that one refines the other. Such relationships can be formally established using relational program logics, which are tailored to reason about relations between two programs, or product constructions which allow to build from two programs a product program that emulates the behavior of both input programs. Similarly, product programs and relational program logics can be used to reason about 2-safety properties, an important class of properties that reason about two executions of the same program, and includes as instances non-interference, continuity, and determinism. In this paper, we consider several notions of product programs and explore their relationship with different relational program logics. Moreover, we present applications of product programs to program robustness, non-interference, translation validation, and differential privacy.
Year
DOI
Venue
2016
10.1016/j.jlamp.2016.05.004
Journal of Logical and Algebraic Methods in Programming
Field
DocType
Volume
Programming language,Differential privacy,Determinism,Program logic,Theoretical computer science,Robustness (computer science),Program analysis,Mathematics
Journal
85
Issue
ISSN
Citations 
5
2352-2208
8
PageRank 
References 
Authors
0.49
26
3
Name
Order
Citations
PageRank
Gilles Barthe12337152.36
Juan Manuel Crespo21647.25
César Kunz316710.81