SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand

This program is tentative and subject to change.

Mon 5 Dec 2022 18:00 - 20:00 at Atrium - SPLASH Posters Chair(s): Xujie Si, Caterina Urban

We propose VST-A, a new framework for program verification, based on the idea of reducing large program proofs into simpler verification goals. This new approach combines the benefits of interactive provers as well as the readability of annotated programs, and enables incremental program verification for incremental program development. VST-A analyzes control flow graphs and reduces the program verification problem to the verification of each control flow path between assertions. This reduction is defined in Coq, proved sound in Coq, and computed call-by-value in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of its underlying Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.

This program is tentative and subject to change.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

18:00 - 20:00
SPLASH PostersStudent Research Competition / Posters at Atrium
Chair(s): Xujie Si McGill University, Canada, Caterina Urban INRIA & École Normale Supérieure | Université PSL
18:00
2h
Poster
[G] Simple Extensible Programming Through Precisely-Typed Open Recursion
Student Research Competition
Andong Fan The Hong Kong University of Science and Technology
18:00
2h
Poster
[G] CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis
Student Research Competition
Chengpeng Wang The Hong Kong University of Science and Technology
18:00
2h
Poster
[G] LoRe: Local-First Reactive Programming with Verified Safety Guarantees
Student Research Competition
Julian Haas Technische Universität Darmstadt
18:00
2h
Poster
[U] Qiwi: A Beginner Friendly Quantum Language
Student Research Competition
Abhinandan Pal Indian Institute of Information Technology Kalyani, Anubhab Ghosh Indian Institute of Information Technology Kalyani
18:00
2h
Poster
Provably correct smart contracts: an approach using DeepSEA
Posters
Daniel Britten University of Waikato, Vilhelm Sjöberg CertiK, Steve Reeves University of Waikato
18:00
2h
Poster
Tower: Data Structures in Quantum Superposition
Posters
Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
18:00
2h
Poster
[U] Using Mutations to Analyze Formal Specifications
Student Research Competition
Siraphob Phipathananunth Vanderbilt University
18:00
2h
Poster
Competitive Debugging: Toward Contests Promoting Debugging as a Skill
Posters
Patrick Rein Hasso Plattner Institute, Tom Beckmann Hasso Plattner Institute, Leonard Geier Hasso Plattner Institute, University of Potsdam, Toni Mattis Hasso Plattner Institute, University of Potsdam, Robert Hirschfeld HPI, University of Potsdam
18:00
2h
Poster
[G] Foundationally sound annotation verifier via control flow splitting
Student Research Competition
Litao Zhou Shanghai Jiao Tong University, China
18:00
2h
Poster
Semi-symbolic Inference for Efficient Streaming Probabilistic Programming
Posters
Eric Atkinson Massachusetts Institute of Technology, Charles Yuan Massachusetts Institute of Technology, Guillaume Baudart Inria, Louis Mandel IBM Research, Michael Carbin Massachusetts Institute of Technology
18:00
2h
Poster
[G] A Study of the Impact of Callbacks in Staged Static+Dynamic Partial Analysis
Student Research Competition
Aditya Anand Indian Institute of Technology Mandi
18:00
2h
Poster
Multiverse Notebook: A Notebook Environment for Safe and Efficient Exploration
Posters
Tomoki Nakamaru The University of Tokyo, Shigeyuki Sato The University of Tokyo
18:00
2h
Poster
Katara: Synthesizing CRDTs with Verified Lifting
Posters
Shadaj Laddad University of California at Berkeley, Conor Power University of California at Berkeley, Mae Milano University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein University of California at Berkeley
18:00
2h
Poster
Explicit Code Reuse Recommendation
Posters
Dov Fraivert Open University of Israel, David H. Lorenz Open University and Technion IIT
DOI
18:00
2h
Poster
[G] Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm
Student Research Competition
Yahui Song National University of Singapore, Wei-Ngan Chin National University of Singapore
18:00
2h
Poster
Composing linear types and separation logic proofs of memory safety.
Posters
Pilar Selene Linares Arevalo The University of Melbourne
18:00
2h
Poster
[G] ARENA: Enhancing Abstract Refinement for Neural Network Verification
Student Research Competition
Yuyi Zhong School of Computing, National University of Singapore, Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore
18:00
2h
Poster
[U] Termination of Recursive Functions by Lexicographic Orders of Linear Combinations
Student Research Competition

Information for Participants
Info for room Atrium:

This is the main atrium used for registration, posters, tea/coffee/lunches.