Hypersafety properties of arity n are program properties that relate n traces of a program (or, more generally, traces of n programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the n related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples.
Fri 9 DecDisplayed time zone: Auckland, Wellington change
13:30 - 15:00 | Logic and Verification IOOPSLA at AMRF Auditorium Chair(s): Benjamin Lucien Kaminski Saarland University and University College London | ||
13:30 30mResearch paper | Finding real bugs in big programs with incorrectness logic OOPSLA Quang Loc Le University College London, Azalea Raad Imperial College London, Jules Villard Meta, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London DOI | ||
14:00 30mTalk | Fractional Resources in Unbounded Separation Logic OOPSLA Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia DOI | ||
14:30 30mTalk | Proving Hypersafety Compositionally OOPSLA DOI Pre-print |