@InProceedings{BeckertKlebanovUlbrich2015,
author = {Bernhard Beckert and Vladimir Klebanov and Mattias Ulbrich},
title = {Regression Verification for {J}ava Using a Secure
Information Flow Calculus},
booktitle = {17th Workshop on Formal Techniques for
Java-like Programs ({FTfJP} 2015)},
month = jul,
year = {2015},
pages = {6:1--6:6},
url = {http://doi.acm.org/10.1145/2786536.2786544},
doi = {10.1145/2786536.2786544},
publisher = {ACM},
%% SNIP
abstract = {Regression verification and checking for illicit
information flow in programs are probably the two
most prominent instances of so-called relational
program reasoning. Regression verification is
concerned with proving that two programs behave
either equally or differently in a formally
specified manner; information-flow checking aims to
establish that an attacker cannot distinguish
executions of a program that vary in a part of the
initial state designated as secret. While the
theoretical connections between the two problems are
well understood, there are also subtle but
significant pragmatic differences. This paper
reports the results of an experiment to adapt a
state-of-the-art deductive information-flow
verification system for Java to the problem of
regression verification.},
find_pdf = {ftfjp2015.pdf},
keywords = {IMPROVE}
}