Many natural program correctness properties can be stated in terms of symmetries, but existing formal methods have little support for reasoning about such properties. We consider how to formally verify a broad class of symmetry properties expressed in terms of group actions. To specify these properties, we design a syntax for group actions, supporting standard constructions and a natural notion of entailment. Then, we develop a Hoare-style logic for verifying symmetry properties of imperative programs, where group actions take the place of the typical pre- and post-condition assertions. Finally, we develop a prototype tool $\mathsf{SymVerif}$, and use it to verify symmetry properties on a series of handcrafted benchmarks. Our tool uncovered an error in a model of a dynamical system described by \citet{McLachlan_Quispel_2002}.
Sat 18 OctDisplayed time zone: Perth change
16:00 - 17:30 | AbstractionOOPSLA at Orchid East Chair(s): Steve Blackburn Google and Australian National University | ||
16:00 15mTalk | Abstract Interpretation of Temporal Safety Effects of Higher Order Programs OOPSLA Mihai Nicola Stevens Institute of Technology, Chaitanya Agarwal New York University, Eric Koskinen Stevens Institute of Technology, Thomas Wies New York University | ||
16:15 15mTalk | A Hoare Logic For Symmetry Properties OOPSLA | ||
16:30 15mTalk | Efficient Abstract Interpretation via Selective Widening OOPSLA | ||
16:45 15mTalk | Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic OOPSLA Shushu Wu Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University | ||
17:00 15mTalk | Structural Abstraction and Refinement for Probabilistic Programs OOPSLA Guanyan Li University of Oxford, Juanen Li Beijing Normal University, Zhilei Han Tsinghua University, Peixin Wang East China Normal University, Hongfei Fu Shanghai Jiao Tong University, Fei He Tsinghua University | ||
17:15 15mTalk | Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google | ||