Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 14:22 - 14:45 at Olympia - Specification and Certification Chair(s): Colin Gordon

The modern software engineering process is evolutionary, with commits/patches begetting new versions of code, progressing steadily toward improved systems. In recent years, program analysis and verification tools have exploited version-based reasoning, where new code can be seen in terms of how it has changed from the previous version. When considering program versions, refinement seems a natural fit and, in recent decades, researchers have weakened classical notions of concrete refinement and program equivalence to capture similarities as well as differences between programs. For example, Benton, Yang and others have worked on state-based \emph{refinement relations}.

In this paper, we explore a form of weak refinement based on \emph{trace} relations rather than state relations. The idea begins by partitioning traces of a program $C_1$ into trace classes, each identified via a \emph{restriction} $r_1$. For each class, we specify similar behavior in the other program $C_2$ via a separate restriction $r_2$ on $C_2$. Still, these two trace classes may not yet be equivalent so we further permit a weakening via a binary relation $\mathcal{A}$ on traces, that allows one to, for instance disregard unimportant events, relate analogous atomic events, etc.

We address several challenges that arise. First, we explore one way to specify trace refinement relations by instantiating the framework to Kleene Algebra with Tests (KAT) due to Kozen. We use KAT intersection for restriction, KAT hypotheses for $\mathcal{A}$, KAT inclusion for refinement, and have proved compositionality. Next, we present an algorithm for automatically synthesizing refinement relations, based on a mixture of semantic program abstraction, KAT inclusion, a custom edit-distance algorithm on counterexamples, and case-analysis on nondeterministic branching. We have proved our algorithm to be sound. Finally, we implemented our algorithm as a tool called {\textsc{Knotical}}, on top of {\textsc{Interproc}} and {\textsc{Symkat}}. We demonstrate promising first steps in synthesizing trace refinement relations across a hand-crafted collection of 37 benchmarks that include changing fragments of array programs, models of systems code, and examples inspired by the \texttt{thttpd} and Merecat web servers.

Thu 24 Oct

Displayed time zone: Beirut change

14:00 - 15:30
Specification and CertificationOOPSLA at Olympia
Chair(s): Colin Gordon Drexel University
14:00
22m
Talk
Relational Verification using Reinforcement Learning
OOPSLA
Jia Chen University of Texas at Austin, Jiayi Wei University of Texas at Austin, Yu Feng University of California, Santa Barbara, Osbert Bastani University of Pennsylvania, Işıl Dillig University of Texas Austin
DOI
14:22
22m
Talk
Specification and Inference of Trace Refinement Relations
OOPSLA
Timos Antonopoulos Yale University, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology
DOI
14:45
22m
Talk
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
OOPSLA
Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco IRIF - Université de Paris, Ignacio Fábregas IMDEA Software Institute
Link to publication DOI
15:07
22m
Talk
Certifying Graph-Manipulating C Programs via Localizations within Data Structures
OOPSLA
Shengyi Wang National University of Singapore, Qinxiang Cao Shanghai Jiao Tong University, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of Singapore
DOI Pre-print