SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Mon 5 Dec 2022 18:00 - 20:00 at Atrium - SPLASH Posters Chair(s): Xujie Si, Caterina Urban
Wed 7 Dec 2022 17:45 - 18:00 at AMRF Auditorium - SRC Talks

The correctness of real-time systems depends both on the correct functionalities and the realtime constraints. To go beyond the existing Timed Automata based techniques, we propose a novel solution that integrates a modular Hoare-style forward verifier with a new term rewriting system (TRS) on Timed Effects (TimEffs).
The main purposes are to increase the expressiveness, dy- namically create clocks, and efficiently solve constraints on the clocks. We formally define a core language Ct, generalizing the real-time systems, modeled using mutable variables and timed behavioral patterns, such as delay, deadline, interrupt, etc. Secondly, to capture real-time specifications, we introduce TimEffs, a new effects logic, that extends Regular Ex- pressions with dependent values and arithmetic constraints. Thirdly, the forward verifier infers temporal behaviors of given Ct programs, expressed in TimEffs. Lastly, we present a purely algebraic TRS, i.e., an extended Antimirov algorithm, to efficiently prove language inclusions between TimEffs. To demonstrate the proposal’s feasibility, we prototype the verification system; prove its soundness; report on experimental results.

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
Simple Extensible Programming through Precisely-Typed Open Recursion
Student Research Competition
Andong Fan Hong Kong University of Science and Technology
DOI
18:00
2h
Poster
CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis
Student Research Competition
Chengpeng Wang Hong Kong University of Science and Technology
DOI
18:00
2h
Poster
LoRe: Local-First Reactive Programming with Verified Safety Guarantees
Student Research Competition
Julian Haas TU Darmstadt
DOI
18:00
2h
Poster
Qiwi: A Beginner Friendly Quantum Language
Student Research Competition
Abhinandan Pal IIIT Kalyani, Anubhab Ghosh IIIT Kalyani
DOI
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
DOI
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
Using Mutations to Analyze Formal Specifications
Student Research Competition
Siraphob Phipathananunth Vanderbilt University
DOI
18:00
2h
Poster
Competitive Debugging: Toward Contests Promoting Debugging as a Skill
Posters
Patrick Rein University of Potsdam; Hasso Plattner Institute, Tom Beckmann University of Potsdam; Hasso Plattner Institute, Leonard Geier University of Potsdam; Hasso Plattner Institute, Toni Mattis University of Potsdam; Hasso Plattner Institute, Robert Hirschfeld University of Potsdam; Hasso Plattner Institute
18:00
2h
Poster
Foundationally Sound Annotation Verifier via Control Flow Splitting
Student Research Competition
Litao Zhou Shanghai Jiao Tong University
DOI
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
A Study of the Impact of Callbacks in Staged Static+Dynamic Partial Analysis
Student Research Competition
Aditya Anand IIT Mandi
DOI
18:00
2h
Poster
Multiverse Notebook: A Notebook Environment for Safe and Efficient Exploration
Posters
Tomoki Nakamaru University of Tokyo, Shigeyuki Sato University of Tokyo
DOI
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 of Israel
DOI
18:00
2h
Poster
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
DOI
18:00
2h
Poster
Composing Linear Types and Separation Logic Proofs of Memory Safety
Posters
Pilar Selene Linares Arévalo University of Melbourne
DOI
18:00
2h
Poster
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Student Research Competition
Yuyi Zhong National University of Singapore, Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore
DOI
18:00
2h
Poster
Termination of Recursive Functions by Lexicographic Orders of Linear Combinations
Student Research Competition
DOI

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

17:30 - 19:30
17:30
15m
Poster
Termination of Recursive Functions by Lexicographic Orders of Linear Combinations
Student Research Competition
DOI
17:45
15m
Poster
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
DOI
18:00
15m
Poster
CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis
Student Research Competition
Chengpeng Wang Hong Kong University of Science and Technology
DOI
18:15
15m
Poster
LoRe: Local-First Reactive Programming with Verified Safety Guarantees
Student Research Competition
Julian Haas TU Darmstadt
DOI
18:30
15m
Poster
Foundationally Sound Annotation Verifier via Control Flow Splitting
Student Research Competition
Litao Zhou Shanghai Jiao Tong University
DOI
18:45
15m
Poster
Using Mutations to Analyze Formal Specifications
Student Research Competition
Siraphob Phipathananunth Vanderbilt University
DOI
19:00
15m
Poster
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Student Research Competition
Yuyi Zhong National University of Singapore, Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore
DOI
19:15
15m
Poster
Qiwi: A Beginner Friendly Quantum Language
Student Research Competition
Abhinandan Pal IIIT Kalyani, Anubhab Ghosh IIIT Kalyani
DOI
Hide past events

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

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