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 OctDisplayed time zone: Beirut change
14:00 - 15:30 | |||
14:00 22mTalk | 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 22mTalk | 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 22mTalk | 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 22mTalk | 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 |