SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 11:00 - 11:30 at Seminar Room LG004 - OOPSLA Papers Chair(s): Manas Thakur

Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure’s declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments.

This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust’s type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:30
OOPSLA PapersCOVID Time Papers In Person at Seminar Room LG004
Chair(s): Manas Thakur IIT Bombay
10:30
30m
Talk
Label dependent lambda calculus and gradual typing
COVID Time Papers In Person
Weili Fu University of Freiburg, Germany, Fabian Krause University of Freiburg, Peter Thiemann University of Freiburg, Germany
Link to publication DOI
11:00
30m
Talk
Modular Specification and Verification of Closures in Rust
COVID Time Papers In Person
Fabian Wolff , Aurel Bílý ETH Zurich, Christoph Matheja ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
Link to publication DOI
11:30
30m
Talk
Revisiting Iso-Recursive SubtypingVirtual
COVID Time Papers In Person
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Jinxu Zhao University of Hong Kong
Link to publication DOI
12:00
30m
Talk
Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts
COVID Time Papers In Person
Yannis Smaragdakis University of Athens, Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Konstantinos Triantafyllou ETH Zurich, Ilias Tsatiris University of Athens
Link to publication DOI