SPLASH Companion 2022
2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion 2022)
Powered by
Conference Publishing Consulting

2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion 2022), December 5–10, 2022, Auckland, New Zealand

SPLASH Companion 2022 – Preliminary Table of Contents

Contents - Abstracts - Authors

Frontmatter

Title Page


Message from the Chairs



Posters

Provably Correct Smart Contracts: An Approach using DeepSEA
Daniel Britten, Vilhelm Sjöberg, and Steve Reeves
(University of Waikato, New Zealand; CertiK, n.n.)
It is possible to download a piece of software over the internet and then verify its correctness locally using an appropriate trusted proof system. However, on a blockchain like Ethereum, smart contracts cannot be altered once deployed. This guarantee of immutability makes it possible for end users to interact collectively with a ‘networked’ piece of software, with the same opportunity to verify its correctness. Formal verification of smart contracts on a blockchain therefore offers an unprecedented opportunity for end users to collectively interact with a deployed instance of software that they can verify while not relying on a central authority. All that is required to be trusted beyond the blockchain itself is an appropriate proof system, a component which always needs to be in the trusted computing base, and whose rules and definitions can be public knowledge. DeepSEA (Deep Simulation of Executable Abstractions) could serve as such a proof system. By pairing theorem-proving with a blockchain, the need to trust a central authority can be removed and replaced by trust in an appropriate proof system and a certain level of expertise in the end users to analyse high-level specifications. This poster explores recent work with DeepSEA relating to handling reentrancy, work towards verified price oracles, and on modelling a blockchain.

Publisher's Version Article Search Info
Multiverse Notebook: A Notebook Environment for Safe and Efficient Exploration
Tomoki NakamaruORCID logo and Shigeyuki SatoORCID logo
(University of Tokyo, Japan)
Notebook environments are used widely in data analysis and machine learning because their interactive user interfaces fit well with exploratory tasks in these areas. However, the execution model of existing notebook environments is unsuitable for safe and efficient exploration because every code cell of a notebook runs in a single execution environment even for independent exploratory tasks, where unintended interference can arise among them. To resolve this problem, we developed Multiverse Notebook, a notebook environment that runs each cell in a separate execution environment and saves its execution state. In this poster, we present Multiverse Notebook and our techniques to reduce the application's time and space of Multiverse Notebook.

Publisher's Version Article Search
Explicit Code Reuse Recommendation
Dov Fraivert ORCID logo and David H. Lorenz ORCID logo
(Open University of Israel, Israel)
Code reuse is a common and recommended practice. However, to avoid code duplication reuse may require substantial refactoring effort, especially in legacy code with which the developer is not profoundly familiar. For this reason, developers often prefer to reimplement simple code fragments rather than properly reuse them. In this work, we describe the use of annotations to recommend a useful piece of code for subsequent reuse. These annotations then guard the code against changes that can complicate its extraction, thus allowing subsequent developers to easily locate and reuse it.

Publisher's Version Article Search
Composing Linear Types and Separation Logic Proofs of Memory Safety
Pilar Selene Linares Arevalo ORCID logo
(University of Melbourne, Australia)
Separation logic and linear types are two formal techniques for reasoning about the memory safety of programs with manual memory management. To obtain the advantages of both methods when proving that a program is memory-safe, we investigate how to unify the notion of the frame from lin- ear types and the notion of the frame from a memory safety characterisation inspired by separation logic. That allows us to investigate the necessary conditions under which linear types and separation logic proofs of memory safety may be successfully composed. The benefit of that composition would be to design a framework that supports verifying that a program is memory-safe by proving the memory safety of parts of it using the more appropriate technique and then composing the proofs to certify that the entire program is safe.

Publisher's Version Article Search

Doctoral Symposium

Papers

Program Synthesis for Artifacts beyond Programs
Pankaj Kumar Kalita ORCID logo
(IIT Kanpur, India)


Publisher's Version Article Search
Formally Verified Resource Bounds through Implicit Computational Complexity
Neea Rusch
(Augusta University, USA)


Publisher's Version Article Search
Programming Support for Local-First Software: Enabling the Design of Privacy-Preserving Distributed Software without Relying on the Cloud
Julian Haas
(TU Darmstadt, Germany)


Publisher's Version Article Search
Proving Obliviousness of Probabilistic Algorithms with Formal Verification
Pengbo Yan ORCID logo
(University of Melbourne, Australia)


Publisher's Version Article Search
Towards Automated Updates of Software Dependencies
Dhanushka Jayasuriya
(University of Auckland, New Zealand)


Publisher's Version Article Search
Verification of Hardware and Software with Fuzzing and Proofs
Sujit Kumar MuduliORCID logo
(IIT Kanpur, India)


Publisher's Version Article Search
Grammar Inference for Ad Hoc Parsers
Michael SchröderORCID logo
(TU Wien, Austria)


Publisher's Version Article Search
Verification of Programs with Concealed Components
Sumit LahiriORCID logo
(IIT Kanpur, India)


Publisher's Version Article Search
Towards a Verified Cost Model for Call-by-Push-Value
Zhuo Chen
(University of Melbourne, Australia)


Publisher's Version Article Search
Modelling the Quantification of Technical Debt
Judith Perera
(University of Auckland, New Zealand)


Publisher's Version Article Search

Student Research Competition

Graduate Papers

Simple Extensible Programming through Precisely-Typed Open Recursion
Andong FanORCID logo
(Hong Kong University of Science and Technology, China)
In this abstract, we show that a small extension to the MLscript programming language gives a simple solution to the Expression Problem through precisely typed open recursion.

Publisher's Version Article Search
LoRe: Local-First Reactive Programming with Verified Safety Guarantees
Julian Haas
(TU Darmstadt, Germany)
Nowadays, the dominant design approach in distributed software is cloud-centric. This comes at the cost of several issues including loss of control over data ownership and privacy, lack of offline availability, poor latency, inefficient use of communication infrastructure, and waste of (powerful) computing resources on the edge. Local-first software presents an alternative approach where data is stored and managed locally and devices primarily communicate in a peer-to-peer manner. However, the decentralized nature of local-first software paired with the unpredictability of interactions driven from the outside world impede reasoning about correctness of such applications. Yet, existing solutions to develop local-first software do not provide safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions.
In this work, we propose LoRe, a programming language and compiler that automatically verifies developer-supplied safety properties for local-first applications.

Publisher's Version Article Search
Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm
Yahui SongORCID logo and Wei-Ngan ChinORCID logo
(National University of Singapore, Singapore)
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.

Publisher's Version Article Search
CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis
Chengpeng WangORCID logo
(Hong Kong University of Science and Technology, China)
Querying code conveniently is an appealing goal to the software engineering community. This work advances this goal by presenting a multi-modal query synthesis technique. Given a natural language description and code examples, we synthesize a conjunctive query extracting positive examples and ignoring negative ones, which is further used to query desired constructs in a program. To prune the huge search space, we generate well-typed query sketches for refinement by analyzing code examples and API signatures. We also introduce two quantitative metrics to measure the quality of candidate queries and select the best one. We have implemented our approach as a tool named CodeSpider and evaluated it upon sixteen code querying tasks. Our experimental results demonstrate its effectiveness and efficiency.

Publisher's Version Article Search
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Yuyi Zhong ORCID logo, Quang-Trung Ta, and Siau-Cheng Khoo
(National University of Singapore, Singapore)
Formal verification on neural networks is earnestly needed to guarantee its robustness property. In this paper, we propose an abstract refinement process that leverages the double description method and the new activation relaxation technique to improve the verification precision and efficiency. We implement our proposal into a verification framework named ARENA. And the experimental results show that ARENA yields significantly better verification precision compared to the existing abstract-refinement-based tool DeepSRGR. It also identifies adversarial examples, with reasonable execution efficiency. Lastly, it verifies more images than a state-of-the-art verifier PRIMA.

Publisher's Version Article Search
Foundationally Sound Annotation Verifier via Control Flow Splitting
Litao Zhou ORCID logo
(Shanghai Jiao Tong University, China)
We propose VST-A, a foundationally sound program verifier for assertion annotated C programs. Our approach combines the benefits of interactive provers as well as the readability of annotated programs. VST-A analyzes control flow graphs and reduces the program verification problem to a set of straightline Hoare triples, which correspond to the control flow paths between assertions. 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.

Publisher's Version Article Search
A Study of the Impact of Callbacks in Staged Static+Dynamic Partial Analysis
Aditya AnandORCID logo
(IIT Mandi, India)
Partial analysis is a program analysis technique used in compilation systems when the whole program is not available. Many recent promising approaches perform partial analysis statically that involves identifying the interprocedural dependencies across program elements. These generated dependencies further get evaluated during runtime while generating the final analysis result. However, as the application and library methods are analyzed independently during static analysis, these approaches do not account for the effect of dynamic features such as callbacks. Consequently, in such scenarios, the runtime (say the Java Virtual Machine) needs to discard the static-analysis results and use the existing imprecise builtin analyses. The primary goal of this work is to find out the percentage of objects and methods that may get affected by callbacks, and to propose possible techniques to enhance the generation of dependencies in their presence.

Publisher's Version Article Search

Undergraduate Papers

Termination of Recursive Functions by Lexicographic Orders of Linear Combinations
Raphael Douglas Giles
(UNSW, Australia)
This paper presents an improvement to Isabelle/HOL’s lex- icographic termination algorithm. This paper also shows how to encode positive vector-component maximisation as a linear program.

Publisher's Version Article Search
Qiwi: A Beginner Friendly Quantum Language
Abhinandan Pal ORCID logo and Anubhab Ghosh ORCID logo
(IIIT Kalyani, India)
Acknowledging the inter-disciplinary aspect of quantum computing, there is a need to make quantum programming more accessible for its fast-growing community. With the advent of quantum computers with hundreds of qubits designing circuits manually is infeasible. Most current languages are low-level or involve a steep learning curve or lack control. Thus we propose a quantum programming language (QPL) that allows for high-level abstractions with intuitive syntax while still allowing users to directly construct circuits.
High-level languages decrease user control and caution leading to sub-optimal circuits. To prevent this, Qiwi allows for dead qubit elimination and has dynamically sized data types. We also introduce a mechanism to let the compiler decide the most optimal among several overloaded function definitions, based on statements following the call. Moreover, this work also presents circuits for if outside the control family of gates and a control for loop on quantum data.

Publisher's Version Article Search
Using Mutations to Analyze Formal Specifications
Siraphob Phipathananunth
(Vanderbilt University, USA)
The result of a formal verification is only as good as the specifications. A key challenge in automated verification is therefore coming up with a strong specification. This is somewhat analogous to having a good test suite in software testing. A well-studied technique for improving and assessing a test suite is mutation testing. It is a method for systematically modifying the source code to determine whether the resulting “mutants” can be “caught” by the tests. This paper explores mutation verification, i.e., the use of mutations to strengthen and assess the quality of formal specifications used in a verification tool. We built a prototype for mutation verification—dubbed Gambit—and used it for an industrial tool that verifies smart contracts. Early results indicate that Gambit generates useful mutants that can provide valuable insights about the coverage of the specifications.

Publisher's Version Article Search

proc time: 2.92