SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Sun 15 Nov 2020 08:20 - 09:00 at SPLASH-VII - Posters Session 1
Sun 15 Nov 2020 20:20 - 21:00 at SPLASH-VII - Posters Session 1 Mirror

Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus their limited effort on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. The prior approach to gradual verification, however, was limited to toy programs without recursive data structures. This paper extends gradual verification to realistic programs that manipulate recursive, mutable data structures on the heap. We solve key technical challenges, semantically connecting iso- and equi-recursive interpretations of abstract predicates as well as gradual verification of heap ownership. Our work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit trade-offs can be made.

Sun 15 Nov

Displayed time zone: Central Time (US & Canada) change

08:20 - 09:00
Posters Session 1Posters at SPLASH-VII +12h
08:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
08:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California, Davis
08:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning Xie University of Toronto, Bruno C. d. S. Oliveira University of Hong Kong, Xuan Bi The University of Hong Kong, Tom Schrijvers KU Leuven
08:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna DiVincenzo (Wise) Carnegie Mellon University, Johannes Bader Jane Street, Cameron Wong Jane Street, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
08:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen Rouvoet Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
08:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh Dalvandi University of Surrey, Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University
08:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
08:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University, Brad A. Myers Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
08:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
08:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
08:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College London
08:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University
08:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
08:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros Tasos Imperial College London, Juliana Franco Microsoft Research, Cambridge, Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
08:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
08:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich Geisler Cornell University, Irene Yoon University of Pennsylvania, Aditi Kabra Carnegie Mellon University, Horace He Cornell University, Yinnon Sanders Cornell University, Adrian Sampson Cornell University
20:20 - 21:00
Posters Session 1 MirrorPosters at SPLASH-VII
20:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California, Davis
20:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
20:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
20:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
20:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen Rouvoet Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
20:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University
20:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College London
20:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh Dalvandi University of Surrey, Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University
20:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
20:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
20:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning Xie University of Toronto, Bruno C. d. S. Oliveira University of Hong Kong, Xuan Bi The University of Hong Kong, Tom Schrijvers KU Leuven
20:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros Tasos Imperial College London, Juliana Franco Microsoft Research, Cambridge, Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
20:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna DiVincenzo (Wise) Carnegie Mellon University, Johannes Bader Jane Street, Cameron Wong Jane Street, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
20:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
20:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University, Brad A. Myers Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
20:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich Geisler Cornell University, Irene Yoon University of Pennsylvania, Aditi Kabra Carnegie Mellon University, Horace He Cornell University, Yinnon Sanders Cornell University, Adrian Sampson Cornell University