The Origins of Hyperproperties
Date:
Wednesday, November 11, 2020 15:00 - 16:00
Speaker:
Fred Schneider (Cornell University)
Location:
Zoom Link: https://istaustria.zoom.us/j/98469631645?pwd=ZDN1UVRTdVFFc2Yrc1YwUTdLcFZ3UT09 Meeting ID: 984 6963 1645 Passcode: 943951
Series:
CS Talk Series
Host:
Thomas Henzinger
Contact:
Fabian Mühlböck
We view through a verification lens the evolution of program specifications---from partial and total correctness, through safety and liveness properties, and culminating with hyperproperties. The exposition will include a new approach to verifying a large class of hyperproperties. That approach involves describing systems and their properties in the temporal logic TLA. The reduction of hyperproperties to TLA properties generalizes self-composition to a class of hyperproperties that includes all those we have seen to express security conditions and to express properties of programs.
*Joint work both with M. Clarkson and with L. Lamport is being described.