OOPSLA 2020
2020-11-15..2020-11-20
-- online --
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
as the organisers put it
PACMPL Issue OOPSLA 2020 seeks contributions on all aspects of programming languages and software engineering. Authors of papers published in PACMPL Issue OOPSLA 2020 will be invited to present their work in the OOPSLA track of the SPLASH virtual conference in November. Papers may target any stage of software development, including requirements, modeling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools (such as language front-ends, program analyse ...
| title | author | length |
|---|---|---|
| Koord: A Language for Programming and Verifying Distributed Robotics Application | Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, Sayan Mitra | 15m |
Koord provides a high-level language that separates distributed coordination from platform-dependent control, with Controller Ports for sensing, planning and… | ||
| TacTok: Semantics-Aware Proof Synthesis | Emily First, Yuriy Brun, Arjun Guha | 15m |
Automatic proof synthesis that combines both goal semantics and prior scripts, not just one or the other. TacTok models proof state and proof script together… | ||
| Learning-Based Controlled Concurrency Testing | Suvam Mukherjee, Pantazis Deligiannis, Arpita Biswas, Akash Lal | 15m |
A reinforcement learning scheduler based on Q-learning is implemented inside P# to choose scheduling decisions and data non-determinism values; it optimizes… | ||
| Macros for Domain-Specific Languages | Michael Ballantyne, Alexis King, Matthias Felleisen | 17m |
Presents an implementation of a two-layer expander API for Racket that lets internal DSLs get their own expander and compiler while reusing host services like… | ||
| Gradual Verification of Recursive Heap Data Structures | Jenna Wise, Jenna DiVincenzo, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, Joshua Sunshine | 15m |
Practical system that extends a base static verifier with gradual formulas and optimistic strengthening, inserting runtime checks when a missing spec was… | ||
| Just-in-Time Learning for Bottom-Up Enumerative Synthesis | Shraddha Barke, Hila Peleg, Nadia Polikarpova | 16m |
Builds a solver called Probe that uses just-in-time learning to update PCFG production costs from cheapest partial solutions and then runs guided bottom-up… | ||
| Foundations of Empirical Memory Consistency Testing | Jake Kirkham, Tyler Sorensen, Esin Tureci, Margaret Martonosi | 15m |
Claims a reproducible, efficient GPU litmus-testing workflow that finds weak-memory behaviors by combining a new OpenCL tool, randomized 737000 parameter sets… | ||
| Neural Reverse Engineering of Stripped Binaries using Augmented Control Flow Graphs | Yaniv David, Uri Alon, Eran Yahav | 14m |
Procedure name prediction for stripped binaries using a prototype called Nero that reconstructs CFGs, stitches paths, and builds augmented call sites with… | ||
| Guiding Dynamic Programing via Structural Probability for Accelerating Programming by Example | Ruyi Ji, Yican Sun, Yingfei Xiong, Zhenjiang Hu | 17m |
MaxFlash combines dynamic programming (PROSE-style witness functions and caching) with structural probability from Euphony, using a topdown prediction model to… | ||
| Revisiting Iso-Recursive Subtyping | Yaoda Zhou, Jinxu Zhao | 13m |
Proposes that iso-recursive subtyping is equivalent to checking all finite n-times unfolding inclusions, and then shows an algorithmic reduction: only 1- and… | ||
| Adding Interactive Visual Syntax to Textual Code | Leif Andersen, Michael Ballantyne, Matthias Felleisen | 12m |
Extends textual languages with reusable interactive-syntax extensions that embed runnable visual editors into source code; examples include a tree editor that… | ||
| Counterexample-Guided Correlation Algorithm for Translation Validation | Shubhani Gupta, Abhishek Rose, Sorav Bansal | 16m |
An algorithm constructs product CFGs that correlate sets of source paths with assembly paths using pathset correlation to avoid exponential path blowup, and it… | ||
| Contextual Dispatch for Function Specialization | Olivier Flückiger, Guido Chari, Ming-Ho Yee, Jan Ječmen, Jakob Hain, Jan Vitek | 16m |
Built a JIT called Ř JIT compiler that specializes functions to dynamic call-site properties using contextual dispatch: contexts form a comparable lattice… | ||
| Feedback-Driven Semi-supervised Synthesis of Program Transformations | Xiang Gao, Shraddha Barke, Arjun Radhakrishna, Gustavo Soares, Sumit Gulwani, Alan Leung, Nachiappan Nagappan, Ashish Tiwari | 16m |
Semi-supervised synthesis combines input-output examples with extra unlabeled inputs (cursor locations and mined candidates) and uses anti-unification modulo… | ||
| Regex Matching with Counting-Set Automata | Lenka Turoňová, Lukáš Holík, Ondřej Lengál, Olli Saarikivi, Margus Veanes, Tomáš Vojnar | 14m |
Paper builds a counting-set automata implementation (a CA prototype in Microsoft’s automata library) that determinises regexes with counters without exploding… | ||
| Unifying Execution of Imperative Generators and Declarative Specifications | Pengyu Nie, Marinela Parovic, Zhiqiang Zang, Sarfraz Khurshid, Aleksandar Milicevic, Milos Gligoric | 15m |
Deuterium implements executable contracts as Java code combining an imperative generator that builds the solution backbone and a declarative spec in 2H that… | ||
| Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell | Yiyun Liu, Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou | 16m |
Extension to Liquid Haskell adds refined typeclasses in Liquid Haskell so class laws become checkable at Core; the implementation verifies laws for 34… | ||
| A Structural Model for Contextual Code Changes | Shaked Brody, Uri Alon, Eran Yahav | 13m |
A structural model predicts the next edit given a contextual code change by modeling edit likelihood over AST paths rather than generating full files. The… | ||
| Actor Concurrency Bugs: A Comprehensive Study on Symptoms, Root Causes, API Usages, and Differences | Mehdi Bagherzadeh, Nicholas Fireman, Anas Shawesh, Raffi Khatchadourian | 18m |
Dataset includes 186 real-world Akka bugs mined from 130 Stack Overflow items and 56 GitHub commits, manually validated. Bugs classify into five symptoms… | ||
| Structure Interpretation of Text Formats | Sumit Gulwani, Vu Le, Arjun Radhakrishna, Ivan Radiček, Mohammad Raza | 15m |
An extensible program-synthesis system called Unravel framework learns sequences of parametrized parsing rules (Regex-Split, Delimiter-Split, String-Split… | ||
| Finding Bugs in Database Systems via Query Partitioning | Manuel Rigger, Zhendong Su | 15m |
Automated testing partitions a query into three cases — ϕ, NOT ϕ, and ϕ IS NULL — then recomposes them (using UNION ALL) and compares results; implemented as… | ||
| Testing Consensus Implementations using Communication Closure | Cezara Drăgoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic | 15m |
Presents a randomized tester that exploits communication closure to sample k-periodic uniform lossy synchronous executions instead of all asynchronous… | ||
| Taming Callbacks for Smart Contract Modularity | Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv | 15m |
Paper claims the first sound semantic static algorithm to ensure callbacks don’t break modular reasoning, and ships ECFChecker that decompiles EVM bytecode… | ||
| ιDOT: A DOT Calculus with Object Initialization | Ifaz Kabir, Yufeng Li, Ondřej Lhoták | 14m |
Introduces iDOT, a DOT calculus that models Scala-style fields, strict field reads, and constructors and enforces initialization so null pointer exceptions… | ||
| World Age in Julia: Optimizing Method Dispatch in the Presence of Eval | Julia Belyakova, Benjamin W Chung, Jack Gelinas, Jameson Nash, Ross Tate, Jan Vitek | 14m |
Julia uses a world-age semantics that delays visibility of methods added by eval until between top-level calls, enabling safe inlining and avoiding… | ||
| Resolution as Intersection Subtyping via Modus Ponens | Koar Marntirosian, Tom Schrijvers, Georgios Karachalias | 15m |
Integrates resolution into coercive subtyping with intersection types by adding a modus ponens rule that, when a context type is both a function and its… | ||
| Digging for Fold: Synthesis-Aided API Discovery for Haskell | Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova | 16m |
A synthesis-backed search called Hoogle Plus indexes popular Haskell libraries and synthesizes compositions that match either a provided type or inferred types… | ||
| Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs | Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan | 15m |
Presents a concrete, verified space-cost semantics for CakeML by formalizing a dataLang cost semantics that measures heap and stack with a size_of function… | ||
| Differentially-Private Software Frequency Profiling under Linear Constraints | Hailong Zhang, Yu Hao, Sufian Latif, Raef Bassily, Atanas Rountev | 14m |
Reformulates local differential privacy for frequency vectors that must satisfy software-specific linear inequalities and gives a concrete noise calibration… | ||
| A Large-Scale Longitudinal Study of Flaky Tests | Wing Lam, Stefan Winter, Anjiang Wei, Tao Xie, Darko Marinov, Jonathan Bell | 16m |
Empirical study applies iDFlakies and NonDex plus Isolation and One-By-One to 68 Maven Java projects, detecting 684 flaky tests and evaluating 245 at their… | ||
| Interactive Synthesis of Temporal Specifications from Examples and Natural Language | Ivan Gavran, Eva Darulova, Rupak Majumdar | 16m |
LTLTalk synthesizes co-safe LTL specifications from one natural-language command plus a single demonstration by encoding structure and semantics as an SMT… | ||
| Programming and Reasoning with Partial Observability | Eric Atkinson, Michael Carbin | 15m |
Presents belief programming plus Epistemic Hoare Logic and a new language BLIMP that treat program state as a set of environments and use box/diamond… | ||
| Termination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules | Fei He, Jitao Han | 16m |
Presents an incremental termination checker that reuses certified modules extracted from prior runs, implemented on top of UAutomizer and tested on 276… | ||
| Scalable and Serializable Networked Multi-actor Programming | Bo Sang, Patrick Eugster, Gustavo Petri, Srivatsan Ravi, Pierre-Louis Roman | 15m |
AEON is an actor language and runtime that enforces serializable multi-actor events by organizing actors in a DAG via ownership and using a dominator lock… | ||
| CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files | Yuting Wang, Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao | 17m |
CompCertELF is a Coq-verified C-to-ELF toolchain that adds a verified assembler and supports verified separate compilation by proving commutativity between… | ||
| Random Testing for C and C++ Compilers with YARPGen | Vsevolod Livinskii, Dmitry Babokin, John Regehr | 12m |
YARPGen is a C/C++ fuzzer that generates UB-free code by exact value tracking and operation swapping for arithmetic trees, applies generation policies… | ||
| Fast Linear Programming through Transprecision Computing on Small and Sparse Data | Tobias Grosser, Theodoros Theodoridis, Maximilian Falkenstein, Arjun Pitchanathan, Michael Kruse, Manuel Rigger, Zhendong Su, Torsten Hoefler | 14m |
Analyzes ~500,000 simplex tableaux from Polly PPCG and HayStack and finds >99% of coefficients <9 bits, medians of 18 columns and 84% sparsity, with rare… | ||
| Pomsets with Preconditions: A Simple Model of Relaxed Memory | Radha Jagadeesan, Alan Jeffrey, James Riely | 16m |
A denotational memory model called pomsets with preconditions represents executions as labeled partial orders augmented with logical preconditions, uses… | ||
| On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers | Dominik Winterer, Chengyu Zhang, Zhendong Su | 13m |
Proposes type-aware operator mutation: randomly replace operators with others of the same SMT-LIB type, chain mutations, and cross-check Z3 vs CVC4 to spot… | ||
| Inter-theory Dependency Analysis for SMT String Solvers | Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar | 15m |
Introduces a concrete analysis called solved form distance that measures how many case splits are needed to break string/integer coupling, plus decision… | ||
| Taming Type Annotations in Gradual Typing | John Peter Campora III, Sheng Chen | 15m |
Paper claims static analysis can find incorrect annotations that later cause runtime cast errors by combining type inference with variational types and a… | ||
| Precise Static Modeling of Ethereum “Memory” | Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, Yannis Smaragdakis | 15m |
Declarative modeling of EVM memory using datalog rules and a gigahorse decompiler recovers source-level arguments and array allocations from low-level… | ||
| DynamiTe: Dynamic Termination and Non-termination Proofs | Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, ThanhVu Nguyen | 13m |
DynamiTe is a Python tool that instruments loops with vtrace instrumentation and iteration counters, learns linear ranking functions from concrete terminating… | ||
| Rethinking Safe Consistency in Distributed Object-Oriented Programming | Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, Guido Salvaneschi | 15m |
ConSysT is an extension to Java that models a replicated store with Ref references annotated by consistency (examples: @Ev for eventual) and supports… | ||
| Detecting Locations in JavaScript Programs Affected by Breaking Library Changes | Anders Møller, Benjamin Barslev Nielsen, Martin Toldam Torp | 15m |
This OOPSLA 2020 talk presents the tool TAPIR that can help JavaScript developers when their application dependencies have breaking changes.
Detecting… | ||
| Fuzzing Channel-Based Concurrency Runtimes using Types and Effects | Quentin Stiévenart, Magnus Madsen | 15m |
An automatic generator produces terminating effects and emits small, type- and effect-correct programs to fuzz channel runtimes; effects are built by… | ||
| Perfectly Parallel Fairness Certification of Neural Networks | Caterina Urban, Maria Christakis, Valentin Wüstholz, Fuyuan Zhang | 15m |
A perfectly parallel static analysis certifies dependency fairness for feed‑forward ReLU networks by combining a cheap forward pre-analysis (interval abstract… | ||
| Incremental Predicate Analysis for Regression Verification | Qianshan Yu, Fei He, Bow-Yaw Wang | 16m |
Implements an end-to-end regression-verification pipeline on CPAchecker that reuses assertion annotations across revisions: a CFA Diff based on similarity… | ||
| StreamQL: A Query Language for Processing Streaming Time Series | Lingkun Kong, Konstantinos Mamouras | 15m |
StreamQL presents an algebra of stream transformations (monotone As→Bs functions) that composes relational, dataflow and temporal operators so a pipeline like… | ||
| Shiftry: RNN Inference in 2KB of RAM | Aayan Kumar, Vivek Seshadri, Rahul Sharma | 16m |
Shiftry compiles RNN inference into C that runs on an Arduino Uno with only 2 KB RAM by converting floating point to fixed point, using mixed bitwidth… | ||
| Designing Types for R, Empirically | Alexi Turcotte, Aviral Goel, Filip Krikava, Jan Vitek | 16m |
A function annotation language and runtime contract checker are built and evaluated: Typetracer is a dynamic tracer on a modified R VM that infers types from… | ||
| Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative S | Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser | 16m |
Derives executable type checkers from Statix specifications by giving an operational semantics that schedules name resolution to avoid unstable queries… | ||
| Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Featu | Minseok Jeon, Myungho Lee, Hakjoo Oh | 15m |
Graphick automatically generates graph-based context-sensitivity and heap-abstraction heuristics by learning feature sequences over program graphs… | ||
| FlowCFL: Generalized Type-Based Reachability Analysis: Graph Reduction and Equivalence of CFL-Based | Ana Milanova | 15m |
A new dynamic semantics tracks chains between stack variables (flow from a parameter in one context to a return in another) and turns points-to reasoning into… | ||
| Dataflow-Based Pruning for Speeding up Superoptimization | Manasij Mukherjee, Pranav Kant, Zhengyang Liu, John Regehr | 14m |
Applies abstract interpretation to prune Souper's enumerative synthesis by proving whole families of partially symbolic candidates infeasible using domains… | ||
| Sound Garbage Collection for C using Pointer Provenance | Subarno Banerjee, David Devecsery, Peter M. Chen, Peter M. Chen, Satish Narayanasamy | 16m |
Presents a sound garbage collector for C that tracks pointer provenance at runtime rather than guessing pointers by value, using Dynamic Pointer Provenance… | ||
| A Type-and-Effect System for Object Initialization | Fengyun Liu, Ondřej Lhoták, Aggelos Biboudis, Paolo G. Giarrusso, Martin Odersky | 16m |
Type-and-effect design enforces a concretely checkable initialization discipline: cold, warm, hot types plus potentials and effects track field accesses… | ||
| Hidden Inheritance: An Inline Caching Design for TypeScript Performance | Zhefeng Wu, Zhe Sun, Kai Gong, lingyun Chen, Lingyun Chen, Bin Liao, Yihua Jin | 16m |
Claims a new inline-caching scheme called hidden inheritance that uses TypeScript’s static class/interface hierarchy to treat parent and descendant hidden… | ||
| Geometry Types for Graphics Programming | Dietrich Geisler, Irene Yoon, Aditi Kabra, Horace He, Yinnon Sanders, Adrian Sampson | 16m |
Defines geometry types that tag vectors with coordinate scheme, geometric object, and reference frame, and implements them in a new language called Gator with… | ||
| A Modular Cost Analysis for Probabilistic Programs | Martin Avanzini, Georg Moser, Michael Schaper | 15m |
Presents a modular method that derives symbolic upper bounds on expected resource cost for probabilistic imperative programs by combining the ERT-calculus with… | ||
| Program Equivalence for Assisted Grading of Functional Programs | Joshua Clune, Vijay Ramamurthy, Ruben Martins, Umut A. Acar | 16m |
Zeus clusters Standard ML student submissions by proving structural equivalence with inference rules and emits an SMT formula checked by z3 so clustering is… | ||
| Deductive Optimization of Relational Data Storage | Jack Feser, John Feser, Sam Madden, Nan Tang, Armando Solar-Lezama | 14m |
A system called Castor synthesizes specialized on-disk layouts and native executables from known query templates, serializing the static database ahead of time… | ||
| Build Scripts with Perfect Dependencies | Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt | 15m |
Build system that requires no author-specified deps: Rattle records per-command dependencies via file-system tracing, speculates parallel execution from… | ||
| Eliminating Abstraction Overhead of Java Stream Pipelines using Ahead-of-Time Program Optimization | Anders Møller, Oskar Haarklou Veileborg | 13m |
Streamliner is an ahead-of-time optimizer that inlines Java Stream pipelines by using a precise must-points-to pointer analysis, aggressive inlining, stack… | ||
| Dynamic Dispatch of Context-Sensitive Optimizations | Gabriel Poesia, Fernando Magno Quintão Pereira | 09m |
Implements a runtime DFA-based context tracking that avoids cloning whole call chains, implemented as an LLVM link-time pass and published with code on Github… | ||
| Verifying and Improving Halide’s Term Rewriting System with Program Synthesis | Julie L. Newcomb, Andrew Adams, Steven Johnson, Rastislav Bodík, Shoaib Kamil | 15m |
Halide’s term rewriting system is formally verified and extended using SMT and synthesis tools: Z3 proves 88% of rules automatically and Coq completes the… | ||
| Testing Differential Privacy with Dual Interpreters | Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, Aaron Roth | 16m |
An automated tester called DPCheck converts a common DP proof pattern into a hybrid test that combines instrumented concrete traces and symbolic execution… | ||
| Compiling Symbolic Execution with Staging and Algebraic Effects | Guannan Wei, Oliver Bračevac, Shangyin Tan, Tiark Rompf | 16m |
Claims a first Futamura projection for symbolic interpreters and shows a pipeline that stages a definitional interpreter (Scala + Freer monads + LMS) to… | ||
| Towards a Formal Foundation of Intermittent Computing | Milijana Surbatovich, Brandon Lucia, Limin Jia | 15m |
Provides a formal correctness definition: an intermittent execution is correct if it is observationally equivalent to some continuous execution, and it proves… | ||
| Adversarial Examples for Models of Code | Noam Yefet, Uri Alon, Eran Yahav | 15m |
Claims a first adversarial attack on models of code and provides a concrete algorithm DAMP that computes gradients on token embeddings to propose new variable… | ||
| Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic | Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu | 15m |
A unified proof framework uses matching logic as a base to build automated provers for multiple logics, implementing 11 generic rules (including LFP based on… | ||
| LiveDroid: Identifying and Preserving Mobile App State in Volatile Runtime Environments | Umar Farooq, Zhijia Zhao, Manu Sridharan, Iulian Neamtiu | 15m |
LiveDroid automatically discovers and preserves the minimal app state needed to survive activity restarts by static analysis and runtime patches. It defines… | ||
| Programming with a Read-Eval-Synth Loop | Hila Peleg, Roi Gabay, Shachar Itzhaky, Eran Yahav | 13m |
A live REPL extended with synthesis called Read-Eval-Synth Loop stitches examples, sketching, and new predicates (notably retain) into specifications so the… | ||
| A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra | Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman Amarasinghe, Fredrik Kjolstad | 17m |
Framework implements sparse iteration-space transformations inside TACO and a CUDA backend and generates fused sparse kernels (SpMV, SpMM, SDDMM, MTTKRP) that… | ||
| Automatic and Efficient Variability-Aware Lifting of Functional Programs | Ramy Shahin, Marsha Chechik | 15m |
Implements a variability-aware extension of a PCF-like functional language (pattern matching, polymorphic lists and pairs) and a Haskell variability library… | ||
| The Anchor Verifier for Blocking and Non-blocking Concurrent Software | Cormac Flanagan, Stephen N. Freund | 15m |
Anchor is an automatic SMT-based verifier plus compiler that checks reduction-style concurrency using concise moves_as synchronization specs and… | ||
| CAMP: Cost-Aware Multiparty Session Protocols | David Castro-Perez, Nobuko Yoshida | 15m |
Extends multiparty session types with runtime cost annotations and extracts per-participant cost equations that account for message sizes, node/CPU counts and… | ||
| Polymorphic Types and Effects with Boolean Unification | Magnus Madsen, Jaco van de Pol | 16m |
Extends Hindley-Milner with Boolean unification to infer precise pure/impure effects, proven to compute principal types and soundly guarantee that terms typed… | ||
| DiffStream: Differential Output Testing for Stream Processing Programs | Konstantinos Kallas, Filip Niksic, Caleb Stanford, Rajeev Alur | 16m |
DiffStream is a Flink testing library that compares a sequential and a parallel run by a matching algorithm that decides stream equivalence up to an explicit… | ||
| Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica | Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, David Basin | 16m |
A methodology that links compositional refinement to separation-logic code verification and is fully formalized in Isabelle/HOL, yielding end-to-end trace… | ||
| Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel- | Azalea Raad, Ori Lahav, Viktor Vafeiadis | 16m |
The paper introduces POG, the first program logic for persistent x86, and an Ix86 instrumented semantics that reduces Px86 by removing the pbuffer via a… | ||
| Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs | Gushu Li, Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie | 16m |
Proposes projection-based assertions that express quantum-state predicates more richly than classical patterns while enabling efficient runtime checks by… | ||
| Featherweight Go | Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, Nobuko Yoshida | 16m |
Defines a minimal core language Featherweight Go (FG) and its generic extension Featherweight Generic Go (FGG), proves a semantics-by-translation claim that… | ||
| Statically Verified Refinements for Multiparty Protocols | Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, Nobuko Yoshida | 15m |
Theory proves refined multiparty session types preserve trace equivalence while tracking variable knowledge with multiplicities 0 or ω; implementation builds a… | ||
| Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution | Shengjian Guo, Yueqi Chen, Jiyong Yu, Meng Wu, Zhiqiang Zuo, Peng Li, Yueqiang Cheng, Huibo Wang, Huibo Wang | 13m |
Claims a practical symbolic-execution tool that models CPU out-of-order and speculative scheduling to expose cache-timing leaks. Implements Out-of-Order… | ||
| Satune: Synthesizing Efficient SAT Encoders | Hamed Gorjiara, Guoqing Harry Xu, Brian Demsky | 15m |
Satune synthesizes and auto-tunes SAT encoders from a small sample of domain problems, providing a DSL for total and partial orders, integers and booleans, a… | ||
| Guided Linking: Dynamic Linking without the Costs | Sean Bartell, Will Dietz, Vikram S. Adve | 14m |
Guided Linking merges a developer-chosen optimized set into a single merged library (LLVM-based, using LTO+PGO), then uses developer-supplied constraints like… | ||
| A Model for Detecting Faults in Build Specifications | Thodoris Sotiropoulos, Stefanos Chaliasos, Dimitris Mitropoulos, Diomidis Spinellis | 16m |
Proposes BuildFS, a formal execution model that maps every file read/write to the build task that performed it and defines concrete faults: missing input and… | ||
| WATCHER: In-Situ Failure Diagnosis | Hongyu Liu, Hongyu Liu, Sam Silvestro, Xiangyu Zhang, Jian Huang, Tongping Liu | 13m |
WATCHER is an automated in-situ failure diagnoser built on iReplayer that deterministically replays crashes, identifies the failing… | ||
| Precise Inference of Expressive Units of Measurement Types | Tongtong Xiang, Jeff Y. Luo, Werner Dietl | 14m |
PUnits is a static unit-of-measurement system that proves sound in Coq, encodes units as boolean and integer variables, and solves whole-program constraints… | ||
| Formulog: Datalog for SMT-Based Static Analysis | Aaron Bembenek, Michael Greenberg, Stephen Chong | 15m |
Formulog is a DSL that combines Datalog, an ML-like term fragment, and SMT solving and a prototype runtime implements it. The authors implement three analyses… | ||
| Scaling Exact Inference for Discrete Probabilistic Programs | Steven Holtzen, Guy Van den Broeck, Todd Millstein | 15m |
Introduces Dice as a discrete PPL that compiles programs to binary decision diagrams and performs inference by weighted model counting, reusing compiled… | ||
| Handling Bidirectional Control Flow | Yizhou Zhang, Guido Salvaneschi, Andrew C. Myers | 15m |
Claims that algebraic effects can themselves raise effects and still be statically safe, implemented as a core calculus and type system that forbids unhandled… | ||
| Mossad: Defeating Software Plagiarism Detection | Breanna Devore-McDonald, Emery D. Berger | 16m |
A tool called MOSSAD automatically rewrites a compilable submission into semantically equivalent variants that evade popular detectors like Moss by breaking… | ||
| Learning Semantic Program Embeddings with Graph Interval Neural Network | Yu Wang, Ke Wang, Fengjuan Gao, Linzhang Wang | 11m |
Paper presents Graph Interval Neural Network that learns program embeddings by iteratively abstracting control flow graphs into interval-based abstraction… | ||
| How Do Programmers Use Unsafe Rust? | Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers | 15m |
Paper analyzes unsafe Rust across the ecosystem using the Qrates framework and a modified compiler to compile and extract MIR from almost 29k compiled crates… | ||
| Automated Policy Synthesis for System Call Sandboxing | Shankara Pailoor, Xinyu Wang, Hovav Shacham, Işıl Dillig, Isil Dillig | 17m |
Abhaya automatically generates sound, optimal syscall-whitelisting policies by combining a scalable static analysis with an SMT-guided synthesis phase. The… | ||
| Multiparty Motion Coordination: From Choreographies to Robotics Programs | Rupak Majumdar, Nobuko Yoshida, Damien Zufferey | 14m |
Combines multiparty session types with assume‑guarantee reasoning to avoid exponential state blowup and statically verify choreographies of robots; a Python… | ||
| Assertion-Based Optimization of Quantum Programs | Thomas Häner, Torsten Hoefler, Matthias Troyer | 15m |
An assertion-based optimizer that uses Z-basis, probability-1 pre/postconditions and triviality rules removes redundant gates and qubits by proving operations… | ||
| An Empirical Study of Ownership, Assets, and Typestate in Obsidian | Michael Coblenz, Jonathan Aldrich, Brad A. Myers, Joshua Sunshine | 15m |
A new language, Obsidian, implements typestate and linearity to track ownership and prevent asset loss; authors run a randomized controlled trial with 20… | ||
| Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements | Guilherme Vieira Leobas, Fernando Magno Quintão Pereira | 16m |
A compiler pass detects semiring patterns (c = c + ab) in LLVM IR and inserts speculative checks so identity/absorbing elements elide work; implemented in LLVM… | ||
| Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation | Giulia Meuli, Mathias Soeken, Martin Roetteler, Thomas Häner | 17m |
Claims an automatic accuracy manager that extracts closed-form cost and error formulas from source code and uses them to tune approximation parameters to… | ||
| Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors | Cyril Six, Sylvain Boulmé, David Monniaux | 15m |
Implements a post-pass instruction scheduler for CompCert targeting the Kalray Coolidge VLIW and ships an untrusted OCaml scheduler plus a Coq-verified… | ||
| Proving Highly-Concurrent Traversals Correct | Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham | 12m |
Paper proves that optimistic lock-free traversals are correct by reducing concurrent traversal correctness to sequential reasoning plus two concrete… | ||
| A Systematic Approach to Deriving Incremental Type Checkers | André Pacak, Sebastian Erdweg, Tamás Szabó | 17m |
Provides a compiler from textbook-style typing rules to Datalog that yields an incremental type checker and a DSL for language specs, with a concrete encoding… | ||
| Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism | Jonathan Immanuel Brachthäuser, Philipp Schuster, Klaus Ostermann | 15m |
A new language called Effekt implements contextual effect polymorphism by making function-like blocks second class so they cannot escape, providing a… | ||
| Fixpoints for the Masses: Programming with First-Class Datalog Constraints | Magnus Madsen, Ondřej Lhoták | 17m |
Presents a concrete embedding of first-class Datalog constraints into a functional language, implemented as a 5k-line extension to the 60k-line Flix compiler… | ||
| Flow2Vec: Value-Flow-Based Precise Code Embedding | Yulei Sui, Xiao Cheng, Guanqin Zhang, Haoyu Wang | 15m |
Builds an interprocedural value-flow graph from LLVM IR (IVFG) and uses CFL-reachability to filter only realizable call/return paths, formulates reachability… | ||
| nothing matches | ||