SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Events (86 results)

Safe Object Initialization, Abstractly

Scala When: Sun 17 Oct 2021 11:10 - 11:30 People: Fengyun Liu, Ondřej Lhoták, Enze Xing, Cao Nguyên Pham

… , beginning with all fields being empty until all of
them are filled. However …

ShapeRank: Rank Polymorphism meets Reactive Streams

REBLS 2021 When: Mon 18 Oct 2021 11:40 - 12:05 People: Gilad Bracha

… ShapeRank is a statically typed, functional programming lan- guage designed for machine learning, data analytics and re- active programming. All ShapeRank values are multidimen- sional streams, known as hyperstreams, and all operations …

Restructuring Structure Editing

LIVE 2021 When: Tue 19 Oct 2021 14:30 - 14:50 People: David Moon, Cyrus Omar

… Structure editors have long promised to improve the programming experience for all, but are often too slow or difficult to use. In this essay, we describe a new approach to structure editing, called tile-based editing, that recovers many …

Trampoline Variables: A General Method for State Accumulation in Reactive Programming

REBLS 2021 When: Mon 18 Oct 2021 13:50 - 14:15 People: Bjarno Oeyen, Sam Van den Vonder, Wolfgang De Meuter

… Reactive programming is all about relegating the management of a program's state changes to the realm of the runtime environment. Nevertheless, sometimes it is still necessary to enrich a reactive program with state variables …

Runtime and Compiler Support for HAMTs

DLS 2021 When: Tue 19 Oct 2021 08:15 - 08:40Tue 19 Oct 2021 16:15 - 16:40 People: Sona Torosyan, Jon Zeppieri, Matthew Flatt

… burdening the compiler with all of the
complexity and design choices of a HAMT …

Dyninka: A FaaS Framework for Distributed Dataflow Applications

REBLS 2021 When: Mon 18 Oct 2021 10:50 - 11:15 People: Patrik Fortier, Frédéric Le Mouël, Julien Ponge

… resources and several load profiles. For all scenarios, Dyninka shows better …

Symmetric Distributed Applications

REBLS 2021 When: Mon 18 Oct 2021 14:15 - 14:40 People: Francisco Sant'Anna, Rodrigo Santos, Noemi Rodriguez

… .
Our middleware intercepts event generation and synchronizes all instances …

Lightweight IOT abstractions for Embedded WebAssembly

VMIL 2021 When: Tue 19 Oct 2021 10:00 - 10:20 People: Tom Lauwaerts, Robbert Gurdeep Singh, Christophe Scholliers

… WebAssembly is a novel safe virtual machine instruction set supported by all major browsers. Its main strengths are safety, portability, compact code representation and fast code execution. These properties also make it an attractive …

Modifiable Software Systems: Smalltalk and HyperCard

LIVE 2021 When: Tue 19 Oct 2021 11:10 - 11:30 People: Josh Justice

… already has all the tooling they need to see how the application works and modify …

Inkbase: Programmable Ink

LIVE 2021 When: Tue 19 Oct 2021 14:50 - 15:10 People: Joshua Horowitz, Szymon Kaliski, James Lindenbaum

… yet won the greatest computational capability of all. This is the ability …

Cross-Domain Compilation: Exploiting Synergies Across the CS Community

VMIL 2021 When: Tue 19 Oct 2021 13:50 - 14:50 People: Tobias Grosser

… Developing a new programming language, constructing a new domain-specific compiler, writing a new verification tool, optimizing a large application, designing a microprocessor, or verifying some of its components, all of these tasks …

A Separation Logic for Probabilistic Independence

Keynote Talks When: Mon 18 Oct 2021 09:00 - 10:00Mon 18 Oct 2021 17:00 - 18:00 People: Justin Hsu

… Probabilistic independence is a useful concept for describing the result of random sampling—a basic operation in all probabilistic languages … methods handle independence poorly, if at all. We propose a probabilistic …

A Variational Database Management System

GPCE When: Sun 17 Oct 2021 13:50 - 14:05Sun 17 Oct 2021 21:50 - 22:05 People: Parisa Ataei, Fariba Khan, Eric Walkingshaw

… in two problems: Some fail to address all users’ needs for their specific kind of variation and all fail to address the interaction of different kinds …

Automatic Grammar Repair

SLE When: Mon 18 Oct 2021 11:20 - 11:35Mon 18 Oct 2021 19:20 - 19:35 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 improve the grammar until it passes all tests. Our core idea …

Automating the Synthesis of Recommender Systems for Modelling Languages

SLE When: Sun 17 Oct 2021 19:20 - 19:35Sun 17 Oct 2021 11:20 - 11:35 People: Lissette Almonte, Sara Perez-Soler, Esther Guerra, Iván Cantador, Juan de Lara

… We are witnessing an increasing interest in building recommender systems (RSs) for all sorts of Software Engineering activities. Modelling is no exception to this trend, as modelling environments are being enriched with RSs that help …

Server-Side Computation of Package Dependencies in Package-Management Systems

Research Papers When: Sun 17 Oct 2021 19:05 - 19:20Sun 17 Oct 2021 11:05 - 11:20 People: Nobuhiro Kasai, Isao Sasano

… dependencies when copying all packages in existing package managers …

Scuemata: A Framework for Evolvable, Composable Data Schema

CONFLANG When: Mon 18 Oct 2021 11:10 - 11:15 People: Sam Boyer

… a logical meta-structure around schemas that allows for:

  • All versions …

Case Study: Building and testing programming assignments with Nix

CONFLANG When: Mon 18 Oct 2021 13:50 - 13:55 People: Martin Schwaighofer

… the same declared environment:

  • A grading pipeline which ingests all submissions …

A compilation method for dynamic typing in ML

Research Papers When: Sun 17 Oct 2021 14:05 - 14:20Sun 17 Oct 2021 22:05 - 22:20 People: Atsushi Ohori, Katsuhiro Ueno

all the standard features of ML, including polymorphic type inference, user …

Latent Effects for Reusable Language Components

Research Papers When: Mon 18 Oct 2021 11:20 - 11:35Mon 18 Oct 2021 19:20 - 19:35 People: Birthe van den Berg, Casper Bach Poulsen, Tom Schrijvers, Nicolas Wu

… and a MetaML-like staging can all be expressed in a modular fashion using …

Backward Symbolic Execution with Loop Folding

SAS When: Mon 18 Oct 2021 15:55 - 16:10Mon 18 Oct 2021 07:55 - 08:10 People: Marek Chalupa, Jan Strejcek

… to search all possible execution paths starting in the initial program location. Due … to analyze all execution paths and thus it is not convenient for program … all program loops, we present an extension called loop folding that aims …

Lifted Termination Analysis by Abstract Interpretation and its Applications

GPCE When: Mon 18 Oct 2021 16:10 - 16:25Mon 18 Oct 2021 08:10 - 08:25 People: Aleksandar S. Dimovski

… ) that terminate under all possible inputs, which represent the correct sketch …

On-Stack Replacement for Program Generators and Source-to-Source Compilers

GPCE When: Sun 17 Oct 2021 14:35 - 14:50Sun 17 Oct 2021 22:35 - 22:50 People: Gregory Essertel, Ruby Tahboub, Tiark Rompf

… OSR is a key component in all modern VMs for languages like Java or JavaScript …

Extracting The Power of Dependent Types

GPCE When: Sun 17 Oct 2021 08:25 - 08:40Sun 17 Oct 2021 16:25 - 16:40 People: Artjoms Šinkarovs, Jesper Cockx

all three steps in a single language that supports both dependent typ-es …

Data Abstraction: A General Framework to Handle Program Verification of Data Structures

SAS When: Sun 17 Oct 2021 14:30 - 14:45Sun 17 Oct 2021 22:30 - 22:45 People: Julien Braine, Laure Gonnord, David Monniaux

… Proving properties on programs operating over arrays, or array-like data structures, most often involves universally quantified invariants, e.g., “all elements below index i are nonzero”. In this article, we propose a general data …

Exploiting Verified Neural Networks via Floating Point Numerical Error

SAS When: Sun 17 Oct 2021 17:15 - 17:30Sun 17 Oct 2021 09:15 - 09:30 People: Kai Jia, Martin C. Rinard

… to all inputs in a space for a neural network. However, many verifiers …

Verified Functional Programming of an Abstract Interpreter

SAS When: Sun 17 Oct 2021 14:05 - 14:20Sun 17 Oct 2021 22:05 - 22:20 People: Lucas Franceschino, David Pichardie, Jean-Pierre Talpin

… assistants. Almost all the code of our implementation, proofs included, written …

Compositional Verification of Smart Contracts Through Communication Abstraction

SAS When: Mon 18 Oct 2021 10:50 - 11:05Mon 18 Oct 2021 18:50 - 19:05 People: Scott Wesley, Maria Christakis, Arie Gurfinkel, Jorge A. Navas, Richard Trefler, Valentin Wüstholz

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

Automatic Synthesis of Data-Flow Analyzers

SAS When: Tue 19 Oct 2021 13:50 - 14:05Tue 19 Oct 2021 21:50 - 22:05 People: Xuezheng Xu, Xudong Wang, Jingling Xue

… ) and seven custom data-flow problems. DFASy has successfully solved all the 14 …

PLTea

PLTea When: Sun 17 Oct 2021 10:20 - 10:50

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Sun 17 Oct 2021 15:10 - 15:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Sun 17 Oct 2021 20:10 - 20:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Mon 18 Oct 2021 13:20 - 13:50

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Mon 18 Oct 2021 15:10 - 15:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Mon 18 Oct 2021 20:10 - 20:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Tue 19 Oct 2021 13:20 - 13:50

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Tue 19 Oct 2021 15:10 - 15:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Tue 19 Oct 2021 20:10 - 20:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Wed 20 Oct 2021 13:20 - 13:50

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Wed 20 Oct 2021 15:10 - 15:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Wed 20 Oct 2021 20:10 - 20:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Thu 21 Oct 2021 10:20 - 10:50

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Thu 21 Oct 2021 15:10 - 15:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Thu 21 Oct 2021 20:10 - 20:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Fri 22 Oct 2021 10:20 - 10:50

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Fri 22 Oct 2021 15:10 - 15:40

… of minutes, or as long as you like. All welcome! …

PLTea

PLTea When: Fri 22 Oct 2021 20:10 - 20:40

… of minutes, or as long as you like. All welcome! …

Making Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity

OOPSLA When: Wed 20 Oct 2021 15:40 - 15:55Wed 20 Oct 2021 07:40 - 07:55 People: Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, Yannis Smaragdakis

… )to combine and maximize the precision of all components of S. When Unity fails … that is more precise than all approaches in S.
As a proof-of-concept, we … clients. Compared with the state of the art, Baton achieves the best precision for all

SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework

SIGPLAN Papers When: Fri 22 Oct 2021 11:20 - 11:35 People: Sotiris Apostolakis, Ziyang Xu, Zujun Tan, Greg Chan, Simone Campanoni, David I. August

… dependence analysis, and makes this resulting information available for all code … (modules cooperate to produce a result more precise than the confluence of all … speculation in the hot loops of all 16 evaluated C/C++ SPEC benchmarks. …

Towards Decidable and Expressive DOT

Student Research Competition When: Wed 20 Oct 2021 17:00 - 19:00Thu 21 Oct 2021 13:50 - 15:10 People: Sophia Roshal

… and theses written describing decidable variants of DOT, however, these variants all

Hedy: Creating a gradual programming language

REBASE When: Tue 19 Oct 2021 07:30 - 09:00 People: Felienne Hermans, Federico Tomassetti

… , there is hardly any syntax at all, for example printing is done with:

print … and lists. The leveled approach means that learners do not have to learn all syntax …

Future of Conferences

SIGPLAN Business When: Thu 21 Oct 2021 10:50 - 12:10Thu 21 Oct 2021 18:50 - 20:10 People: Eelco Visser, Amal Ahmed, Jonathan Aldrich, Sophia Drossopoulou, David Grove, Gorel Hedin, Tony Hosking, Stephen Kell, Shriram Krishnamurthi, Alex Potanin, Yannis Smaragdakis, Manu Sridharan

… Covid has turned all conferences into online events. SPLASH 2021 is a hybrid event, but all but Americans have to attend it online due to travel bans. (The lifting of the travel ban per November is coming just too late.) While many …

Liquid Information Flow Control

SIGPLAN Papers When: Thu 21 Oct 2021 11:35 - 11:50 People: Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama

… if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time. …

Run-Time Data Analysis to Drive Compiler Optimizations

Student Research Competition When: Wed 20 Oct 2021 17:00 - 19:00Thu 21 Oct 2021 13:55 - 15:10 People: Sebastian Kloibhofer

… Throughout program execution, types may stabilize, variables may become constant, and code sections may turn out to be redundant - all information that is used by just-in-time (JIT) compilers to achieve peak performance. Yet, since JIT …

Pomsets with Preconditions: A Simple Model of Relaxed Memory

SIGPLAN Papers When: Wed 20 Oct 2021 14:05 - 14:20 People: Radha Jagadeesan, Alan Jeffrey, James Riely

… compositional reasoning for temporal safety properties, (2) supports all

BCNC

Workshops People: Yegor Bugayenko, Letizia Jaccheri, Andrey Kuleshov, Giancarlo Succi, Anthony I. (Tony) Wasserman

… The first international workshop on “Beyond Code: No Code,” (BCNC 2021) targets one of the most engaging topics currently spanning the software engineering community.

The No Code movement is making its way through all industries, saving …

Snapshot-Free, Transparent, and Robust Memory Reclamation for Lock-Free Data Structures

SIGPLAN Papers When: Thu 21 Oct 2021 14:05 - 14:20 People: Ruslan Nikolaev, Binoy Ravindran

all threads, unlike most prior reclamation schemes such as epoch-based …-off with all existing schemes.

Hyaline schemes offer the following properties …}: supporting many data structures. All existing schemes lack one or more properties …

Run-time Data Analysis to Drive Compiler Optimizations

Doctoral Symposium When: Tue 19 Oct 2021 11:30 - 12:05 People: Sebastian Kloibhofer

… Throughout program execution, types may stabilize, variables may become constant, and code sections may turn out to be redundant - all information that is used by just-in-time (JIT) compilers to achieve peak performance. Yet, since JIT …

Integrated Scientific Modeling and Lab Automation

Keynotes When: Thu 21 Oct 2021 09:20 - 10:20Thu 21 Oct 2021 17:20 - 18:20 People: Luca Cardelli

… The cycle of observation, hypothesis formulation, experimentation, and falsification that has driven scientific and technical progress is lately becoming automated in all its separate components. However, integration between …

A Derivative-Based Parser Generator for Visibly Pushdown Grammars

OOPSLA When: Fri 22 Oct 2021 19:20 - 19:35Fri 22 Oct 2021 11:20 - 11:35 People: Xiaodong Jia, Ashish Kumar, Gang (Gary) Tan

… In this paper, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees …

Armada: Low-Effort Verification of High-Performance Concurrent Programs

SIGPLAN Papers When: Thu 21 Oct 2021 10:50 - 11:05 People: Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao

… . All these techniques are proven sound, and Armada can be soundly extended …

BlankIt Library Debloating: Getting What You Want Instead of Cutting What You Don’t

SIGPLAN Papers When: Fri 22 Oct 2021 10:50 - 11:05 People: Chris Porter, Girish Mururu, Prithayan Barua, Santosh Pande

… in most cases of at least 97%, and adds a runtime overhead of 18% on all libraries (16% for glibc, 2% for others) across all benchmarks of SPEC 2006 …

Solver-Based Gradual Type Migration

OOPSLA When: Thu 21 Oct 2021 19:05 - 19:20Thu 21 Oct 2021 11:05 - 11:20 People: Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, Arjun Guha

… to reconstruct all human-written annotations on all but one program. …

MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels

OOPSLA When: Fri 22 Oct 2021 21:50 - 22:05Fri 22 Oct 2021 13:50 - 14:05 People: Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, Akash Lal

… specification of the isolation level to compute, on a read operation, the set of all

Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust

OOPSLA When: Wed 20 Oct 2021 14:20 - 14:35Wed 20 Oct 2021 22:20 - 22:35 People: Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, Amit Levy

… decisions appropriate for all cases. Application developers can tune libraries …

A General Approach to Define Binders using Matching Logic

SIGPLAN Papers When: Thu 21 Oct 2021 10:50 - 11:05 People: Xiaohong Chen, Grigore Roşu

… matching logic definition of binders also yields models to all binders, which …

Data-Driven Inference of Representation Invariants

SIGPLAN Papers When: Thu 21 Oct 2021 15:55 - 16:10 People: Anders Miltner, Saswat Padhi, Todd Millstein, David Walker

… A representation invariant is a property that holds of all values of abstract type produced by a module. Representation invariants play important roles in software engineering and program verification. In this paper, we develop …

Programming and Execution Models for Parallel Bounded Exhaustive Testing

OOPSLA When: Wed 20 Oct 2021 19:35 - 19:50Wed 20 Oct 2021 11:35 - 11:50 People: Nader Al Awar, Kush Jain, Chris Rossbach, Milos Gligoric

… Bounded-exhaustive testing (BET), which exercises a program under test for all inputs up to some bounds, is an effective method for detecting software bugs. Systematic property-based testing is a BET approach where developers write test …

Web Question Answering with Neurosymbolic Program Synthesis

SIGPLAN Papers When: Thu 21 Oct 2021 11:05 - 11:20 People: Jocelyn (Qiaochu) Chen, Aaron Lamoreaux, Xinyu Wang, Greg Durrett, Osbert Bastani, Işıl Dillig

… that generates all DSL programs that achieve optimal $F_1$ score on the training examples …

SpecSafe: Detecting Cache Side Channels in a Speculative World

OOPSLA When: Wed 20 Oct 2021 13:50 - 14:05Wed 20 Oct 2021 21:50 - 22:05 People: Robert Brotzman-Smith, Danfeng Zhang, Mahmut Taylan Kandemir, Gang (Gary) Tan

… not necessarily catch all cache side channels.
Motivated by this observation, we present …

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems

OOPSLA When: Wed 20 Oct 2021 07:55 - 08:10Wed 20 Oct 2021 15:55 - 16:10 People: Wolf Honore, Jieung Kim, Ji-Yong Shin, Zhong Shao

… replication (SMR) interface, or expose all of the network-level details, sacrificing …

A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra

SIGPLAN Papers When: Thu 21 Oct 2021 11:35 - 11:50 People: Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman Amarasinghe, Fredrik Kjolstad

… to hand-optimized implementations from the literature, while generalizing to all

Integration Verification Across Software and Hardware for a Simple Embedded System

SIGPLAN Papers When: Thu 21 Oct 2021 16:10 - 16:25 People: Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala

… that carry out this exercise, and all of them have simplified the task …

Semantic Code Search via Equational Reasoning

SIGPLAN Papers When: Thu 21 Oct 2021 14:35 - 14:50 People: Varot Premtoon, James Koppel, Armando Solar-Lezama

… We present a new approach to semantic code search based on equational reasoning, and the Yogo tool implementing this approach. Our approach works by considering not only the dataflow graph of a function, but also the dataflow graphs of all

Programming as Architecture, Design, and Urban Planning

Onward! Essays When: Thu 21 Oct 2021 07:40 - 08:20Thu 21 Oct 2021 15:40 - 16:20 People: Tomas Petricek

… and aim to create navigable and habitable software for all its users? …

Designing Types for R, Empirically

SIGPLAN Papers When: Wed 20 Oct 2021 11:05 - 11:20 People: Alexi Turcotte, Aviral Goel, Filip Křikava, Jan Vitek

… , all operations are dynamically checked at run-time. The starting point for our …

Responsive Parallelism with Futures and State

SIGPLAN Papers When: Thu 21 Oct 2021 14:05 - 14:20 People: Stefan K. Muller, Kyle Singer, Noah Goldstein, Umut A. Acar, Kunal Agrawal, I-Ting Angelina Lee

… responsiveness. These advances share one important limitation: all of this work …

IOOpt- Automatic Derivation of I/O complexity bounds for affine programs

SIGPLAN Papers When: Thu 21 Oct 2021 15:55 - 16:10 People: Auguste Olivry, Guillaume Iooss, Nicolas Tollenaere, Atanas Rountev, Saday Sadayappan, Fabrice Rastello

… considering all possible valid schedules.

This paper presents \IOOpt, a fully automated …

A Stepper for a Functional JavaScript Sublanguage

SPLASH-E When: Wed 20 Oct 2021 14:30 - 14:50 People: Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Yee-Jian Tan, Xinyi Zhang, Jingjing Zhao

… that maximize sharing and enable random access to all steps. This work presents …

UDF to SQL Translation through Compositional Lazy Inductive Synthesis

OOPSLA When: Fri 22 Oct 2021 18:50 - 19:05Fri 22 Oct 2021 10:50 - 11:05 People: Guoqiang Zhang, Yuanchao Xu, Xipeng Shen, Işıl Dillig

… . However, because there is no universal decomposition strategy that works for all UDFs …

Automated Derivation of Parametric Data Movement Lower Bounds for Affine Programs

SIGPLAN Papers When: Thu 21 Oct 2021 13:50 - 14:05 People: Auguste Olivry, Julien Langou, Louis-Noël Pouchet, Saday Sadayappan, Fabrice Rastello

… is fundamentally different: one must consider all possible legal schedules …

The Reads-From Equivalence for the TSO and PSO Memory Models

OOPSLA When: Wed 20 Oct 2021 08:10 - 08:25Wed 20 Oct 2021 16:10 - 16:25 People: Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, Viktor Toman

… polynomial time per class when $k$ is bounded. Finally, we implement all our …

Efficient Automatic Scheduling of Imaging and Vision Pipelines for the GPU

OOPSLA When: Thu 21 Oct 2021 22:05 - 22:20Thu 21 Oct 2021 14:05 - 14:20 People: Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, Jonathan Ragan-Kelley

… ) memoization of repeated partial schedules, amortizing their cost over all

Formal Verification of High-Level Synthesis

OOPSLA When: Fri 22 Oct 2021 22:05 - 22:20Fri 22 Oct 2021 14:05 - 14:20 People: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, John Wickerson


proven correct in Coq. Vericert supports most C constructs, including all

Permchecker: A Toolchain for Debugging Memory Managers with Typestate

OOPSLA When: Wed 20 Oct 2021 19:05 - 19:20Wed 20 Oct 2021 11:05 - 11:20 People: Karl Cronburg, Sam Guyer

… manager
at all. A third reason is that existing tools for debugging memory errors …

Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs

OOPSLA When: Wed 20 Oct 2021 18:50 - 19:05Wed 20 Oct 2021 10:50 - 11:05 People: Ting Su, Yichen Yan, Jue Wang, Jingling Sun, Yiheng Xiong, Geguang Pu, Ke Wang, Zhendong Su

… releases — all have been confirmed, and 22 have
already been fixed. Most …