SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Events (60 results)

Proving False in Object Oriented Verification Programs by Exploiting Non-Termination

Sources of Unsoundness in Verification When: Tue 6 Dec 2022 13:30 - 13:50 People: Jaymon Furniss

… We looked at three different verifiers for object-oriented program veri fication, Gobra, KeY, and Dafny. We show that all three can be made to prove false … much difficulty and that this is possibly common throughout all OO verifiers. …

Applicative Intersection Types

APLAS When: Mon 5 Dec 2022 16:00 - 16:30 People: Xu Xue, Bruno C. d. S. Oliveira, Ningning Xie

… }. Nevertheless no previous calculus supports all those features at once. In this paper … all the features, and is proven to be type sound. However, the semantics … of overloading are forbidden, but all other features are supported. The main challenge …

Formal Probabilistic Risk Assessment of a Nuclear Power Plant

Formal Techniques for Safety-Critical Systems When: Wed 7 Dec 2022 16:00 - 16:30 People: Mohamed Abdelghany, Sofiene Tahar

… ) dependability modeling techniques are typically used to associate all possible … formally determine all possible classes of accident events that can occur …

Domain-Specific Visual Language for Data Engineering Quality

Programming Abstractions and Interactive Notations, Tools, and Environments When: Mon 5 Dec 2022 11:15 - 11:30 People: Alexis De Meo, Michael Homer

… and their implications for all parties, eliminating repetition while increasing …

Interleaved 2D Notation for Concatenative Programming

Programming Abstractions and Interactive Notations, Tools, and Environments When: Mon 5 Dec 2022 11:45 - 12:00 People: Michael Homer

… stack to identify where values are produced and consumed. All

MetaCoq as a tool to prevent future unsoundness in Coq

Sources of Unsoundness in Verification When: Tue 6 Dec 2022 11:15 - 12:00 People: Yannick Forster

all aspects of Coq’s type theory in MetaCoq. In the future, we hope …

Toward a dynamic language toolkit

Virtual Machines and Language Implementations When: Mon 5 Dec 2022 11:35 - 12:00 People: Dave Mason

… -Oriented languages. By sharing, all could benefit from each others’ research …

RHLE: Modular Deductive Verification of Relational ∀∃ Properties

APLAS When: Mon 5 Dec 2022 13:30 - 14:00 People: Robert Dickerson, Qianchuan Ye, Michael K. Zhang, Benjamin Delaware

… that \emph{all} runs of a collection of programs do not violate a specified …

Live 2D Compositional Programming

Live Programming When: Tue 6 Dec 2022 16:10 - 16:30 People: Michael Homer

… We present an approach to live programming in a two-dimensional grid of functions where all intermediate values are always visible and tangible. Arguments are chosen through selecting values, and indicated by layout, so all interaction …

Characterizing functions mappable over GADTs

APLAS When: Mon 5 Dec 2022 15:30 - 16:00 People: Patricia Johann, Pierre Cagne

… It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all

Proving Memory Access Violations in Isabelle/HOL

Formal Techniques for Safety-Critical Systems When: Wed 7 Dec 2022 14:00 - 14:30 People: Sharar Ahmadi, Brijesh Dongol, Matt Griffin

… generate a set of programs covering all possible
cases in which an assembly-level …

A Calculus with Recursive Types, Record Concatenation and Subtyping

APLAS When: Mon 5 Dec 2022 16:30 - 17:00 People: Yaoda Zhou, Bruno C. d. S. Oliveira, Andong Fan

… of our disjointness definition. All the proofs are mechanized in the Coq theorem …

Live Programming and Text Editor Integration in the Croquet Microverse 3D Collaborative Construction System

Live Programming When: Tue 6 Dec 2022 14:10 - 14:30 People: Yoshiki Ohshima, Aran Lunzer, Vanessa Freudenberg, Brian Upton, David Smith

… . On each change of the application code, you need to load a new build onto all

Type System for Four Delimited Control Operators

GPCE When: Tue 6 Dec 2022 15:52 - 16:15 People: Chiaki Ishio, Kenichi Asai

… for all the four control operators. Following Danvy and Filinski’s approach, we … and that the calculus with all the four control operators is terminating. Furthermore, we show …

Generic Solution-Space Sampling for Multi-domain Product Lines

GPCE When: Wed 7 Dec 2022 14:37 - 15:00 People: Marc Hentze, Tobias Pett, Chico Sundermann, Sebastian Krieter, Thomas Thüm, Ina Schaefer

all potential error sources missed by problem-space sampling. …

Automated Synthesis of Asynchronizations

SAS When: Tue 6 Dec 2022 16:00 - 16:30 People: Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu Lahiri

… introducing data races. We investigate the delay complexity of enumerating all data race …

Freon: An Open Web Native Language Workbench

SLE 2022 When: Tue 6 Dec 2022 11:42 - 11:57 People: Jos Warmer, Anneke Kleppe

… to be the one tool that can meet all these requirements. Instead the architecture …

Principles of Staged Static+Dynamic Partial Analysis

SAS When: Wed 7 Dec 2022 11:00 - 11:30 People: Aditya Anand, Manas Thakur

… transform a general whole-program analysis (that resolves dependencies across all … partial analysis that addresses all these points, based on the classic theory …

Gradual Grammars: Syntax in Levels and Locales

SLE 2022 When: Wed 7 Dec 2022 14:10 - 14:34 People: Tijs van der Storm, Felienne Hermans

… Programming language implementations are often one-size-fits-all. Irrespective … a single, canonical syntax for all language users. Whereas professional software developers might be willing to learn a programming language all in one go, this might …

Data Types as a More Ergonomic Frontend for Grammar-Guided Genetic Programming

GPCE When: Wed 7 Dec 2022 10:52 - 11:15 People: Guilherme Espada, Leon Ingelse, Paulo Canelas, Pedro Barbosa, Alcides Fonseca

… while using the host language type-system to take advantage of all the existing …

Fast and incremental computation of weak control closure

SAS When: Wed 7 Dec 2022 11:30 - 12:00 People: Abu Naser Masud

… of 31.03 in all benchmarks and a maximum speedup of 35.29 than the best state …

Lang-n-Prove: A DSL for Language Proofs

SLE 2022 When: Wed 7 Dec 2022 15:30 - 15:54 People: Matteo Cimini

… the type safety of all these languages, when the correct code for substitution lemmas …

Partial Parsing for Structured Editors

SLE 2022 When: Tue 6 Dec 2022 10:54 - 11:18 People: Tom Beckmann, Patrick Rein, Toni Mattis, Robert Hirschfeld

… Creating structured editors, which maintain a valid syntax tree at all times rather than allowing to edit program text, is typically a time consuming task. Recent work has investigated the use of existing general-purpose language grammars …

From Coverage Computation to Fault Localization: A Generic Framework for Domain-Specific Languages

SLE 2022 When: Tue 6 Dec 2022 14:35 - 14:59 People: Faezeh Khorram, Erwan Bousse, Antonio Garmendia, Jean-Marie Mottu, Gerson Sunyé, Manuel Wimmer

… meaningful coverage matrices for all investigated DSLs and models. The applied fault …

Language-parametric static semantic code completion

OOPSLA When: Sat 10 Dec 2022 11:30 - 12:00 People: Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, Eelco Visser

… . It should be complete, such that it proposes all valid fragments so that code completion can be used to construct all programs. To realize soundness and completeness …

Synthesizing fine-grained synchronization protocols for implicit monitors

OOPSLA When: Fri 9 Dec 2022 11:30 - 12:00 People: Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, Işıl Dillig

… A monitor is a widely-used concurrent programming abstraction that encapsulates all shared state between threads. Monitors can be classified as being either … monitors from an implicit specification, but prior work does not exploit all

A Language Based on Two Relations between Symbols

Onward! Papers When: Fri 9 Dec 2022 13:30 - 14:00 People: Agustín Rafael Martínez

… We present a language with all the power of abstraction and the simplicity of two fundamental relations: substitution and categorization. With a graphic symbol representing each one of them, we created a playful visual programming …

Foundationally Sound Annotation Verifier via Control Flow Splitting

Student Research Competition When: Mon 5 Dec 2022 18:00 - 20:00Wed 7 Dec 2022 18:30 - 18:45 People: Litao Zhou

… of the rich assertion language, not all reduced proof goals can be automatically …

Portals: An Extension of Dataflow Streaming for Stateful Serverless

Onward! Papers When: Sat 10 Dec 2022 11:30 - 12:00 People: Jonas Spenger, Paris Carbone, Philipp Haller

… introduce all programming model invariants and the corresponding system methods used …

Grammar-based testing for little languages: an experience report with student compilers

COVID Time Papers In Person When: Mon 5 Dec 2022 14:00 - 14:30 People: Phillip van Heerden, Moeketsi Raselimo, Konstantinos (Kostis) Sagonas, Bernd Fischer

… ) all test suites constructed systematically following different grammar … suites performs as well or better than the instructor’s test suite in all aspects … of triggered semantic errors and detected failures and crashes. Moreover, all failing …

Provably Correct Smart Contracts: An Approach using DeepSEA

Posters When: Mon 5 Dec 2022 18:00 - 20:00 People: Daniel Britten, Vilhelm Sjöberg, Steve Reeves

… not relying on a central authority. All that is required to be trusted beyond …

Conferences & Остраннeние: Shortchanging Topos and Ourselves

Onward! Essays When: Thu 8 Dec 2022 11:10 - 11:50 People: Richard P. Gabriel, Jenny Quillien

… about conference design of all types. Cutting access to these deeper physical …

CAAT: Consistency as a Theory

OOPSLA When: Sat 10 Dec 2022 11:00 - 11:30 People: Thomas Haas, Roland Meyer, Hernán Ponce de León

… We propose a family of logical theories for capturing an abstract notion of consistency and show how to build a generic and efficient theory solver that works for all members in the family.
The theories can be used to model the influence …

Automatic Grammar Repair

COVID Time Papers In Person When: Mon 5 Dec 2022 13:30 - 14:00 People: Moeketsi Raselimo, Bernd Fischer

… We describe the first approach to automatically repair bugs in context-free grammars: given a grammar that fails some tests in a given test suite, we iteratively and gradually transform the grammar until it passes all tests. Our core idea …

Symbolic Execution for Randomized Programs

OOPSLA When: Fri 9 Dec 2022 16:00 - 16:30 People: Zachary Susag, Sumit Lahiri, Justin Hsu, Subhajit Roy

… quantify over all possible inputs. Our technique augments standard symbolic …

Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back

OOPSLA When: Fri 9 Dec 2022 15:30 - 16:00 People: Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, Aleksander Boruch-Gruszecki

… that capabilities and effects can be reconciled harmoniously. By assuming that all functions …

Digital Crochet: Toward a Visual Language for Pattern Description

Onward! Papers When: Fri 9 Dec 2022 11:30 - 12:00 People: Klara Seitz, Patrick Rein, Jens Lincke, Robert Hirschfeld

… or ambiguous instructions after all.

We propose a first visual, domain-specific …

Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment

OOPSLA When: Sat 10 Dec 2022 10:30 - 11:00 People: Nico Ritschel, Felipe Fronchetti, Reid Holmes, Ronald Garcia, David C. Shepherd

… functions, but does not require decomposition. We found that while almost all users … decomposition strategy fits all domains, we believe that similar domain-specific sub …

Revisiting Iso-Recursive Subtyping

COVID Time Papers In Person When: Fri 9 Dec 2022 11:30 - 12:00 People: Yaoda Zhou, Bruno C. d. S. Oliveira, Jinxu Zhao

… that two recursive types are subtypes if all their finite unfoldings … involving recursive types. All results are mechanically formalized in the Coq …

Tower: Data Structures in Quantum Superposition

OOPSLA When: Fri 9 Dec 2022 14:00 - 14:30 People: Charles Yuan, Michael Carbin

all recursion using classical parameters as is necessary for a program …. We provide the first executable implementation of sets that satisfies all three …

Scalable Linear Invariant Generation with Farkas’ Lemma

V-OOPSLA When: Wed 30 Nov 2022 21:15 - 21:30 People: Hongming Liu, Hongfei Fu, zhiyong yu, Jiaxin Song, Guoqiang Li

… to a parallel processing that divides the invariant-generation task for all program … the execution time for all program locations.
Hence, our approach constitutes …

Proof transfer for fast certification of multiple approximate neural networks

OOPSLA When: Sat 10 Dec 2022 11:30 - 12:00 People: Shubham Ugare, Gagandeep Singh, Sasa Misailovic

… for the robustness verification of neural networks, a major limitation of almost all state …, and the robustness of all the networks needs to be verified efficiently.

We present FANC …

Evaluating the Quality of Student-Written Software Tests with Curated Mutation Analysis

SPLASH-E When: Mon 5 Dec 2022 16:00 - 16:30 People: Braxton Hall, Elisa Baniassad

… ' suites over all generated clones.

We employed Mutation Analysis to assess …

Applying cognitive principles to model-finding output: the positive value of negative information

OOPSLA People: Tristan Dyer, Tim Nelson, Kathi Fisler, Shriram Krishnamurthi

… , and whether all instances must actually satisfy the input constraints. Using both …

C to checked C by 3c

OOPSLA When: Thu 8 Dec 2022 10:30 - 11:00 People: Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, MIchael Hicks

… necessarily all at once, so that safety retrofitting can be incremental. This paper …

Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities

OOPSLA When: Fri 9 Dec 2022 10:30 - 11:00 People: Aina Linn Georges, Alix Trieu, Lars Birkedal

… and frame lifetimes to a base capability machine. All results have been mechanized …

Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation

OOPSLA When: Fri 9 Dec 2022 16:00 - 16:30 People: Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, Jung-Eun Kim

… . All the proofs are mechanized in Coq. …

Modular Verification of Op-Based CRDTs in Separation Logic

V-OOPSLA When: Wed 30 Nov 2022 04:30 - 04:45 People: Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

… Operation-based Conflict-free Replicated Data Types (op-based CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge.
Additionally, op-based CRDTs …

Compositional Verification of Smart Contracts Through Communication Abstraction

COVID Time Papers In Person When: Wed 7 Dec 2022 15:30 - 16:00 People: Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, Arie Gurfinkel

… Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under …

Concurrent Size

OOPSLA When: Sat 10 Dec 2022 14:00 - 14:30 People: Gal Sela, Erez Petrank

… structure to count the elements, or acquiring one global lock in all update …

Neurosymbolic Repair for Low-Code Formula Languages

V-OOPSLA When: Wed 30 Nov 2022 22:00 - 22:15 People: Rohan Bavishi, Harshit Joshi, José Pablo Cambronero, Anna Fariha, Sumit Gulwani, Vu Le, Ivan Radiček, Ashish Tiwari

all baselines. We release these benchmarks to encourage subsequent work in low …

Competitive Debugging: Toward Contests Promoting Debugging as a Skill

Onward! Papers When: Sat 10 Dec 2022 11:00 - 11:30 People: Patrick Rein, Tom Beckmann, Leonard Geier, Toni Mattis, Robert Hirschfeld

… approaches, and that the format was enjoyable and engaging for all participants.
We …

Plausible sealing for gradual parametricity

OOPSLA When: Fri 9 Dec 2022 11:00 - 11:30 People: Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese

… that are not subject to graduality guarantees. Furthermore, all current proposals rely …

Highly Illogical, Kirk: Spotting Type Mismatches in the Large Despite Broken Contracts, Unsound Types, and Too Many Linters

OOPSLA People: Joshua Hoeflich, Robert Bruce Findler, Manuel Serrano

… of the language can be surprisingly important. Best of all, it also revealed a few …

Elipmoc: advanced decompilation of Ethereum smart contracts

OOPSLA When: Fri 9 Dec 2022 11:00 - 11:30 People: Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, Yannis Smaragdakis

… improves over all notable past decompilers, including its predecessor, Gigahorse …

Taming Transitive Redundancy for Context-Free Language Reachability

V-OOPSLA When: Wed 30 Nov 2022 21:00 - 21:15 People: Yuxiang Lei, Yulei Sui, Shuo Ding, Qirun Zhang

… .

This paper proposes a scalable yet precision-preserving approach to all

Fractional Resources in Unbounded Separation Logic

OOPSLA When: Fri 9 Dec 2022 14:00 - 14:30 People: Thibault Dardinier, Peter Müller, Alexander J. Summers

… whether distributivity and combinability hold for all assertions …

Compilation of Dynamic Sparse Tensor Algebra

OOPSLA When: Thu 8 Dec 2022 15:30 - 16:00 People: Stephen Chou, Saman Amarasinghe

… , including all the ones named above as well as many more. We then describe how, given …

Sources of Unsoundness in Verification (Unsound)

Workshops People: Jan Bessai, Marco Servetto

… this would be greatly beneficial not only because it will help all of us to iron out …

Software Profession Dimensions of Diversity, Equity, and Inclusion

Panels When: Fri 9 Dec 2022 10:30 - 12:00 People: Steven D. Fraser, Dennis Mancl, Alex Sloley, Sally Sloley, Kelly Blincoe, Stéphanie Camaréna, Tanya Johnson, Geoff Kaufman, Mahsa McCauley, Sheng-Ying Pao

… principles and their adoption remain relevant to all. This Systems, Programming …