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

Applicative Intersection Types

Research Papers 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 …

RHLE: Modular Deductive Verification of Relational ∀∃ Properties

Research Papers 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 …

A Calculus with Recursive Types, Record Concatenation and Subtyping

Research Papers 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 …

Characterizing functions mappable over GADTs

Research Papers 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

Automated Synthesis of Asynchronizations

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

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

Principles of Staged Static+Dynamic Partial Analysis

SAS 2022 Papers 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 …

Fast and incremental computation of weak control closure

SAS 2022 Papers 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 …

Language-parametric static semantic code completion

OOPSLA 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 People: Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, Isil 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

CAAT: Consistency as a Theory

OOPSLA People: Thomas Haas, Roland Meyer, Hernan Ponce de Leon

… 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 …

[G] Foundationally sound annotation verifier via control flow splitting

Student Research Competition People: Litao Zhou

… Hoare triple. Because of the rich assertion language, not all reduced proof goals …

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

OOPSLA 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 …

Symbolic Execution for Randomized Programs

OOPSLA People: Zachary Susag, Sumit Lahiri, Justin Hsu, Subhajit Roy

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

Tower: Data Structures in Quantum Superposition

OOPSLA People: Charles Yuan, Michael Carbin

… a type system that bounds all recursion using classical parameters.

Using … implementation of sets that satisfies all three mandated properties of reversibility …

Proof transfer for fast certification of multiple approximate neural networks

OOPSLA 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 …

Provably correct smart contracts: an approach using DeepSEA

Posters People: Daniel Britten, Vilhelm Sjöberg, Steve Reeves

… on a central authority. All that is required to be trusted beyond the blockchain itself …

Concurrent size

OOPSLA People: Gal Sela, Erez Petrank

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

C to checked C by 3c

OOPSLA 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 People: Aina Linn Georges, Alix Trieu, Lars Birkedal

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

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 …

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

OOPSLA People: Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, Jung-Eun Kim

… ensures isolation between partitions. All the proofs are mechanized in Coq. …

Neurosymbolic Repair for Low-Code Formula Languages

OOPSLA People: Rohan Bavishi, Harshit Joshi, José Pablo Cambronero, Anna Fariha, Sumit Gulwani, Vu Le, Ivan Radiček, Ashish Tiwari

… LaMirage outperforms all baselines. We release these benchmarks to encourage …

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

SPLASH-E People: Braxton Hall, Elisa Baniassad

… ’ suites over all the clones.

We employed Mutation Analysis to assess …

Scalable Linear Invariant Generation with Farkas' Lemma

OOPSLA People: Hongming Liu, Hongfei Fu, zhiyong yu, Jiaxin Song, Guoqiang Li

… the invariant-generation task for all program locations by assigning … of magnitude, even if in the non-parallel scenario that sums up the execution time for all

Taming Transitive Redundancy for Context-Free Language Reachability

OOPSLA People: Yuxiang Lei, Yulei Sui, Shuo Ding, Qirun Zhang

… .

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

Compilation of Dynamic Sparse Tensor Algebra

OOPSLA People: Stephen Chou, Saman Amarasinghe

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

Fractional Resources in Unbounded Separation Logic

OOPSLA People: Thibault Dardinier, Peter Müller, Alexander J. Summers

… whether distributivity and combinability hold for all assertions.

In this paper …

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

OOPSLA People: Joshua Hoeflich, Robby Findler, Manuel Serrano

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

Plausible sealing for gradual parametricity

OOPSLA People: Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese

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

Modular Verification of Op-Based CRDTs in Separation Logic

OOPSLA People: Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

… \emph{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 …

Elipmoc: advanced decompilation of Ethereum smart contracts

OOPSLA People: Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, Yannis Smaragdakis

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

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 …