Memory Safety: Uniqueness as Separation.In Person Talk
This program is tentative and subject to change.
Programming languages with uniqueness type systems prevent pointer aliasing, simplifying memory safety reasoning. However, code implemented in these languages often interoperates through foreign function interfaces with external components implemented in languages lacking the same level of static safety guarantees. To verify safe updates in a combined system, one must manually verify that the external components preserve the safety invariants of the uniqueness type system. In particular, recent work showed that one can manually discharge such obligations on C components from a cross-language Cogent-C system by directly reasoning about the C code in higher-order logic. However, even for simple examples, discharging the uniqueness safety obligations, known as frame conditions, within a logic not specifically designed for direct reasoning in terms of heaps and pointers was not ideal. Separation logic is an established logic that facilitates reasoning about imperative programs by localising reasoning to the parts of the heap that the program mutates. This raises a vital question. Can we use separation logic to discharge the safety obligations imposed by uniqueness types? The answer is yes. This paper demonstrates that the frame conditions can be inferred from particular separation logic triples and, hence, discharged by reasoning using separation logic. We identify and verify the soundness of specific separation logic triples that imply the frame conditions imposed by a uniqueness type system.
This program is tentative and subject to change.
Tue 28 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
11:00 - 12:30 | Type Systems, Safety, and VerificationResearch Papers at R104 Chair(s): Alex Potanin Australian National University | ||
11:00 30mTalk | Memory Safety: Uniqueness as Separation.In Person Talk Research Papers Pilar Selene Linares Arévalo University of Melbourne, Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Vincent Jackson University of Melbourne, Liam O'Connor Australian National University, Peter Schachte The University of Melbourne, Christine Rizkallah University of Melbourne | ||
11:30 30mTalk | Fair Termination for Resource-Aware Active ObjectsIn Person Talk Research Papers Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Violet Ka I Pun Western Norway University of Applied Sciences, Ulises Torrella Høgskulen på Vestlandet | ||
12:00 30mTalk | A Formal Foundation for Equational Reasoning on Probabilistic Programs Research Papers Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Yoshihiro Ishiguro Nagoya University, AIST, Zachary Stone The MathComp-Analysis development team | ||