Relational verification using reinforcement learning
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 10, 2019
- Source ID
- 10.1145/3360567
Entities
People
- Işıl Dillig
- Jia Chen
- Jiayi Wei
- Osbert Bastani
- Yu Feng
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of California, Santa Barbara
- University of Pennsylvania
- University of Texas at Austin