Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 17:00 - 17:15 at VMCAI - Hyperproperties Chair(s): Grigory Fedyukovich

Hyperproperties lift conventional trace properties in a way that describes how a system behaves in its entirety, and not just based on its individual traces. We generalize this notion to multi-properties, which describe the behavior of not just a single system, but of a set of systems, which we call a multi-model. We demonstrate the usefulness of our setting with practical examples. We show that model-checking multi-properties is equivalent to model-checking hyperproperties. However, our framework has the immediate advantage of being compositional. We introduce sound and complete compositional proof rules for model-checking multi-properties, based on over- and under-approximations of the systems in the multi-model. We then describe methods of computing such approximations. The first is abstraction-refinement based, in which a coarse initial abstraction is continuously refined using counterexamples, until a suitable approximation is found. The second, tailored for models with finite traces, finds suitable approximations via the $L^*$ learning algorithm.
Our methods can produce much smaller models than the original ones, and can therefore be used for accelerating model-checking for both multi-properties and hyperproperties.

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory FedyukovichFlorida State University
17:00 - 17:15
Compositional Model Checking for Multi-Properties
Ohad GoudsmidDepartment of Computer Science, The Technion, Orna GrumbergTechnion – Israel Institute of Technology, Sarai SheinvaldDepartment of Software Engineering, ORT Braude College of Engineering
Media Attached
17:15 - 17:30
Decomposing Data Structure Commutativity Proofs with mn-Differencing
Eric KoskinenStevens Institute of Technology, Kshitij BansalGoogle
Media Attached