Events (45 results)

Why can’t we all just get along? Training SA and AI tools to communicate

ASA 2023 When: Sat 17 Jun 2023 16:00 - 16:45 People: Yaniv David

… …

Covering All the Bases: Type-Based Verification of Test Input Generators

PLDI Research Papers When: Mon 19 Jun 2023 10:40 - 11:00 People: Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan

… expected of these generators is that they be capable of producing _all

HERO-ML: A Very High-Level Array Language for Executable Modelling of Data Parallel Algorithms

ARRAY 2023 When: Sun 18 Jun 2023 14:00 - 14:30 People: Bjorn Lisper, Linus Källberg

… HERO-ML is an array language, on very high level, which is intended for
specifying data parallel algorithms in a concise and platform-independent
way where all the inherent data parallelism is easy to identify. The goal is to support …

AI-based Program Analysis via Relevance and Similarity

ASA 2023 When: Sat 17 Jun 2023 16:45 - 17:30 People: Kihong Heo

… results. All this information is incorporated into a probabilistic model based …

ItyFuzz: Snapshot-Based Fuzzer for Onchain Smart Contract Auditing

ASA 2023 People: Koushik Sen

… Smart contracts are critical financial instruments, and their security is paramount. However, smart contract programs are challenging to fuzz due to the persistent blockchain state behind all transactions. Mutating sequences …

Lightning Talks

CSC 2023 When: Sat 17 Jun 2023 09:50 - 11:00 People: Andrew Siegel, Sreepathi Pai, Harshitha Menon, Piotr Luszczek, Alyson Fox, Vivek Sarkar, Andrew W. Appel

… Can Bind Us All (in the Quest for Correctness)

The Instruction Set …

F-IVM: Analytics over Relational Databases under Updates

DRAGSTERS 2023 When: Sat 17 Jun 2023 11:50 - 12:10 People: Ahmet Kara, Milos Nikolic, Dan Olteanu, Haozhe Zhang

… . In the key space, all tasks require general joins and variable marginalization …

Static Analysis of Data Transformations in Jupyter Notebooks (Virtual)

SOAP 2023 When: Sat 17 Jun 2023 09:30 - 10:00 People: Luca Negrini, Guruprerana Shabadi, Caterina Urban

all transformations applied to the data. Several properties can …

E-graph Extraction Using ZDDs

EGRAPHS 2023 When: Sun 18 Jun 2023 16:40 - 17:00 People: Eli Rosenthal

… encode all possible extractions for an e-graph. With such a ZDD, computing …

When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C

SOAP 2023 When: Sat 17 Jun 2023 10:30 - 11:00 People: Michael Schwarz, Julian Erhard, Vesal Vojdani, Simmo Saan, Helmut Seidl

… The C programming language offers setjmp/longjmp as a mechanism for non-local control flow. This mechanism has complicated semantics. As most developers do not encounter it day-to-day, they may be unfamiliar with all its intricacies …

ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler

EGRAPHS 2023 When: Sun 18 Jun 2023 14:00 - 15:00 People: Chris Fallin

… or cascading merge step. Our novel “acyclic e-graph” approach replaces all of our …

Keynote: A Brave New World for Memory Management Research

ISMM 2023 When: Sun 18 Jun 2023 09:05 - 10:05 People: Martin Maas

… Memory management is a decades-old area with a large amount of practical impact. However, there is a frequent misconception that all important research problems in this area are either already solved or are unsolvable. In this talk, I …

Sandia's Formal Hardware Design and Verification, Present and Future

PLARCH 2023 When: Sat 17 Jun 2023 15:00 - 15:10 People: Noah Evans

all but the most critical systems in industry. This paper gives a brief overview …

Picking a CHERI Allocator: Security and Performance Considerations

ISMM 2023 When: Sun 18 Jun 2023 15:00 - 15:20 People: Jacob Bramley, Dejice Jacob, Andrei Lascu, Jeremy Singer, Laurence Tratt

… introduce a number of security attacks and show that all but one allocator …

NUMAlloc: A Faster NUMA Memory Allocator

ISMM 2023 When: Sun 18 Jun 2023 14:40 - 15:00 People: Hanmei Yang, Xin Zhao, Jin Zhou, Wei Wang, Sandip Kundu, Bo Wu, Hui Guan, Tongping Liu

… the best performance among all evaluated allocators, running 15.7% faster than …

OMRGx: Programmable and Transparent Out-of-Core Graph Partitioning and Processing

ISMM 2023 When: Sun 18 Jun 2023 16:20 - 16:40 People: Gurneet Kaur, Rajiv Gupta

… of all. …

Predicting Dynamic Properties of Heap Allocations using Neural Networks Trained on Static Code: An Intellectual Abstract

ISMM 2023 When: Sun 18 Jun 2023 11:40 - 12:00 People: Christian Navasca, Martin Maas, Petros Maniatis, Hyeontaek Lim, Harry Xu

… are often not representative of all workload behavior and may miss important corner …

Stellar: A DSL to Build and Explore Sparse Accelerators

PLARCH 2023 When: Sat 17 Jun 2023 11:30 - 11:45 People: Hasan Genc, Hansung Kim, Prashanth Ganesh, Yakun Sophia Shao

… accurately describe all the different components of sparse accelerator design …

Search-Based Regular Expression Inference on a GPU

PLDI Research Papers When: Wed 21 Jun 2023 16:00 - 16:20 People: Mojtaba Valizadeh, Martin Berger

… that is precise (i.e., accepts all positive and rejects all negative examples …, as characteristic sequences, all sub-languages of the infix-closure of the union …

Parameterized Algebraic Protocols

PLDI Research Papers When: Wed 21 Jun 2023 15:20 - 15:40 People: Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos

… We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all

An Eager SMT Solver for Algebraic Data Type Queries

SRC When: Mon 19 Jun 2023 18:00 - 18:07 People: Amar Shah

… Algebraic Data Types (ADTs) are a programming construct classically found in functional programming languages but are increasingly found in all kinds of modern languages. ADTs are a convenient generalization of structures like enumerated …

Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning

PLDI Research Papers When: Tue 20 Jun 2023 14:00 - 14:20 People: Alexander Bagnall, Gordon Stewart, Anindya Banerjee

… . We exploit the key idea that all discrete probability distributions can …

Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels

PLDI Research Papers When: Mon 19 Jun 2023 16:40 - 17:00 People: Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo

… with polynomial memory consumption in all cases. We report on an implementation …

Obtaining Information Leakage Bounds via Approximate Model Counting

PLDI Research Papers When: Tue 20 Jun 2023 09:00 - 09:20 People: Seemanta Saha, Surendra Ghentiyala, Shihua Lu, Lucas Bang, Tevfik Bultan

… not be able to explore all execution paths, 2) Model counting constraints …

A Lineage-Based Referencing DSL for Computer-Aided Design

PLDI Research Papers When: Wed 21 Jun 2023 17:20 - 17:40 People: Dan Cascaval, Rastislav Bodík, Adriana Schulz

… is designing reference semantics that can express programmer intent across allall paths. We give a semantics for fine-grained element lineage that can …

Sound Dynamic Deadlock Prediction in Linear Time

PLDI Research Papers When: Tue 20 Jun 2023 15:00 - 15:20 People: Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

all sync-preserving deadlocks, with running time that is linear per abstract … SPDOnline predicts all sync-preserving deadlocks that involve two threads …

Putting Weak Memory in Order via a Promising Intermediate Representation

PLDI Research Papers When: Wed 21 Jun 2023 09:20 - 09:40 People: Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav

… that validates all compiler optimizations that are performed in single-threaded …

Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks

PLDI Research Papers When: Mon 19 Jun 2023 16:20 - 16:40 People: Mark Niklas Müller, Marc Fischer, Robin Staab, Martin Vechev

… We present a new abstract interpretation framework for the precise over-approximation of numerical fixpoint iterators.
Our key observation is that unlike in standard abstract interpretation (AI), typically used to over-approximate all

Architecture-Preserving Provable Repair of Deep Neural Networks

PLDI Research Papers When: Mon 19 Jun 2023 17:00 - 17:20 People: Zhe Tao, Stephanie Nawas, Jacqueline Mitchell, Aditya V. Thakur

… repair approach that has all of these features. We implement our approach …

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

PLDI Research Papers When: Mon 19 Jun 2023 10:20 - 10:40 People: Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen

… and 1,758 gates, where all tools we compared with failed. In addition, our work …

Discrete Adversarial Attack to Models of Code

PLDI Research Papers When: Tue 20 Jun 2023 09:40 - 10:00 People: Fengjuan Gao, Yu Wang, Ke Wang

… realization of adversarial training improves the robustness of all evaluated models …

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A

PLDI Research Papers When: Wed 21 Jun 2023 10:00 - 10:20 People: Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal

… . This demonstrates the intended security guarantees of the hypercall ABIs. All

cuCatch: A Debugging Tool for Efficiently Catching Memory Safety Violations in CUDA Applications

PLDI Research Papers When: Wed 21 Jun 2023 17:00 - 17:20 People: Mohamed Tarek Ibn Ziad, Sana Damani, Aamer Jaleel, Stephen W. Keckler, Mark Stephenson

… CUDA, OpenCL, and OpenACC are the primary means of writing general-purpose software for NVIDIA GPUs, all of which are subject to the same well-documented memory safety vulnerabilities currently plaguing software written in C and C++. One …

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity

PLDI Research Papers When: Tue 20 Jun 2023 09:20 - 09:40 People: Marco Eilers, Thibault Dardinier, Peter Müller

… timing behavior. The key idea is to prove that all mutating operations …

CQS: A Formally-Verified Framework for Fair and Abortable Synchronization

PLDI Research Papers People: Nikita Koval, Dmitry Khalanskiy, Dan Alistarh

… .
Importantly, all our algorithms, including the CQS framework and the primitives …

A Type System for Safe Intermittent Computing

PLDI Research Papers When: Wed 21 Jun 2023 17:40 - 18:00 People: Milijana Surbatovich, Naomi Spargo, Limin Jia, Brandon Lucia

… recovering all written state. Moreover, no prior work allows the programmer to directly …

Towards Supporting Universal Static Analysis using WALA

Tutorials When: Sun 18 Jun 2023 14:00 - 15:30Sun 18 Jun 2023 16:00 - 17:50 People: Rahul Krishna, Raju Pavuluri, Saurabh Sinha, Divya Sankar, Julian Dolby, Rangeet Pan

… of the application across all these languages and frameworks to identify …

Efficient Parallel Functional Programming with Effects

PLDI Research Papers When: Tue 20 Jun 2023 14:20 - 14:40 People: Jatin Arora, Sam Westrick, Umut A. Acar

… compiler supports all features of the Parallel ML
language, including …

Mostly Automated Proof Repair for Verified Libraries

PLDI Research Papers When: Wed 21 Jun 2023 09:00 - 09:20 People: Kiran Gopinathan, Mayank Keoliya, Ilya Sergey

… versions. Sisyphus has managed to repair proofs for all those functions, suggesting …

Leveraging Rust Types for Program Synthesis

PLDI Research Papers When: Wed 21 Jun 2023 15:00 - 15:20 People: Jonas Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey

… effects, in Rust, all this information can be inferred from the types, letting …

Flux: Liquid Types for Rust

PLDI Research Papers When: Wed 21 Jun 2023 14:40 - 15:00 People: Nico Lehmann, Adam Geller, Niki Vazou, Ranjit Jhala

… from up to 25% of code size (average 9%), to nothing at all. …

Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations

PLDI Research Papers When: Wed 21 Jun 2023 09:40 - 10:00 People: Jihyeok Park, Dongjun Youn, Kanguk Lee, Sukyoung Ryu

… in all of them. The tool detected 143 distinct conformance bugs (42 in engines …

Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer Analysis

PLDI Research Papers When: Tue 20 Jun 2023 15:20 - 15:40 People: Wenjie Ma, Shengyuan Yang, Tian Tan, Xiaoxing Ma, Chang Xu, Yue Li

… Doop and the other in Java for the imperative Tai-e, and we consider all

Repairing Regular Expressions for Extraction

PLDI Research Papers When: Wed 21 Jun 2023 16:40 - 17:00 People: Nariyoshi Chida, Tachio Terauchi

… While synthesizing and repairing regular expressions (regexes) based on Programming-by-Examples (PBE) methods have seen rapid progress in recent years, all existing works only support synthesizing or repairing regexes for membership …

Recursive State Machine Guided Graph Folding for Context-Free Language Reachability

PLDI Research Papers When: Wed 21 Jun 2023 17:00 - 17:20 People: Yuxiang Lei, Yulei Sui, Shin Hwei Tan, Qirun Zhang

… edges can be folded—by merging the two nodes with all the edges joining them …