Files in this item



application/pdftusil-chen-rosu-2021-tr.pdf (847kB)
Main articlePDF


Title:Hyperproperties in Matching Logic
Author(s):Tusil, Jan; Chen, Xiaohong; Rosu, Grigore
matching logic
Abstract:Matching logic is a uniform logic to specify and reason about programming languages and program properties. Many important logics and/or formal systems have been shown to be definable in matching logic as logical theories. However, no research has been conducted to studying how hyperproperties can be treated in matching logic. In this paper, we give the first theoretical result that shows that HyperLTL (hyper linear temporal logic), which is an important temporal logic designed for specifying and reasoning about hyperproperties, can be completely captured by matching logic. Our result demonstrates that matching logic offers a uniform treatment to handling hyperproperties and to supporting their model checking problems.
Issue Date:2021
Genre:Technical Report
Date Available in IDEALS:2021-02-19

This item appears in the following Collection(s)

Item Statistics