Search events for 'all'
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 all … all 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 …