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

Relational verification aims to prove properties that relate a pair of programs or two different runs of the same program. While relational properties (e.g., equivalence, non-interference) can be verified by reducing them to standard safety, there are typically many possible reduction strategies, only some of which result in successful automated verification. Motivated by this problem, we propose a novel relational verification algorithm that learns useful reduction strategies using reinforcement learning. Specifically, we show how to formulate relational verification as a Markov Decision Process (MDP) and use reinforcement learning to synthesize an optimal policy for the underlying MDP. The learned policy is then used to guide the search for a successful verification strategy. We have implemented this approach in a tool called Coeus and evaluate it on two benchmark suites. Our evaluation shows that Coeus solves significantly more problems within a given time limit compared to multiple baselines, including two state-of-the-art relational verification tools.

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, Isil 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