OOPSLA 2020
109 papers
- A large-scale longitudinal study of flaky tests
- A model for detecting faults in build specifications
- A modular cost analysis for probabilistic programs
- A sparse iteration space transformation framework for sparse tensor algebra
- A structural model for contextual code changes
- A systematic approach to deriving incremental type checkers
- A type-and-effect system for object initialization
- Actor concurrency bugs: a comprehensive study on symptoms, root causes, API usages, and differences
- Adding interactive visual syntax to textual code
- Adversarial examples for models of code
- Assertion-based optimization of Quantum programs
- Automated policy synthesis for system call sandboxing
- Automatic and efficient variability-aware lifting of functional programs
- Build scripts with perfect dependencies
- CAMP: cost-aware multiparty session protocols
- Can advanced type systems be usable? An empirical study of ownership, assets, and typestate in Obsidian
- Certified and efficient instruction scheduling: application to interlocked VLIW processors
- CompCertELF: verified separate compilation of C programs into ELF object files
- Compiling symbolic execution with staging and algebraic effects
- Contextual dispatch for function specialization
- Counterexample-guided correlation algorithm for translation validation
- Dataflow-based pruning for speeding up superoptimization
- Deductive optimization of relational data storage
- Designing types for R, empirically
- Detecting locations in JavaScript programs affected by breaking library changes
- DiffStream: differential output testing for stream processing programs
- Differentially-private software frequency profiling under linear constraints
- Digging for fold: synthesis-aided API discovery for Haskell
- Do you have space for dessert? a verified space cost semantics for CakeML programs
- DynamiTe: dynamic termination and non-termination proofs
- Dynamic dispatch of context-sensitive optimizations
- Effects as capabilities: effect handlers and lightweight effect polymorphism
- Eliminating abstraction overhead of Java stream pipelines using ahead-of-time program optimization
- Enabling accuracy-aware Quantum compilers using symbolic resource estimation
- Exposing cache timing side-channel leaks through out-of-order symbolic execution
- Fast linear programming through transprecision computing on small and sparse data
- Featherweight go
- Feedback-driven semi-supervised synthesis of program transformations
- Finding bugs in database systems via query partitioning
- Fixpoints for the masses: programming with first-class Datalog constraints
- Flow2Vec: value-flow-based precise code embedding
- FlowCFL: generalized type-based reachability analysis: graph reduction and equivalence of CFL-based and type-based reachability
- Formulog: Datalog for SMT-based static analysis
- Foundations of empirical memory consistency testing
- Fuzzing channel-based concurrency runtimes using types and effects
- Geometry types for graphics programming
- Gradual verification of recursive heap data structures
- Guided linking: dynamic linking without the costs
- Guiding dynamic programing via structural probability for accelerating programming by example
- Handling bidirectional control flow
- Hidden inheritance: an inline caching design for TypeScript performance
- How do programmers use unsafe rust?
- Igloo: soundly linking compositional refinement and separation logic for distributed system verification
- Incremental predicate analysis for regression verification
- Inter-theory dependency analysis for SMT string solvers
- Interactive synthesis of temporal specifications from examples and natural language
- Just-in-time learning for bottom-up enumerative synthesis
- Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications
- Koord: a language for programming and verifying distributed robotics application
- Learning graph-based heuristics for pointer analysis without handcrafting application-specific features
- Learning semantic program embeddings with graph interval neural network
- Learning-based controlled concurrency testing
- LiveDroid: identifying and preserving mobile app state in volatile runtime environments
- Macros for domain-specific languages
- Mossad: defeating software plagiarism detection
- Multiparty motion coordination: from choreographies to robotics programs
- Neural reverse engineering of stripped binaries using augmented control flow graphs
- On the unusual effectiveness of type-aware operator mutations for testing SMT solvers
- Perfectly parallel fairness certification of neural networks
- Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86
- Polymorphic types and effects with Boolean unification
- Pomsets with preconditions: a simple model of relaxed memory
- Precise inference of expressive units of measurement types
- Precise static modeling of Ethereum "memory"
- Program equivalence for assisted grading of functional programs
- Programming and reasoning with partial observability
- Programming at the edge of synchrony
- Programming with a read-eval-synth loop
- Projection-based runtime assertions for testing and debugging Quantum programs
- Proving highly-concurrent traversals correct
- Random testing for C and C++ compilers with YARPGen
- Regex matching with counting-set automata
- Resolution as intersection subtyping via Modus Ponens
- Rethinking safe consistency in distributed object-oriented programming
- Revisiting iso-recursive subtyping
- Satune: synthesizing efficient SAT encoders
- Scalable and serializable networked multi-actor programming
- Scaling exact inference for discrete probabilistic programs
- Semiring optimizations: dynamic elision of expressions with identity and absorbing elements
- Shiftry: RNN inference in 2KB of RAM
- Sound garbage collection for C using pointer provenance
- Statically verified refinements for multiparty protocols
- StreamQL: a query language for processing streaming time series
- Structure interpretation of text formats
- TacTok: semantics-aware proof synthesis
- Taming callbacks for smart contract modularity
- Taming type annotations in gradual typing
- Termination analysis for evolving programs: an incremental approach by reusing certified modules
- Testing consensus implementations using communication closure
- Testing differential privacy with dual interpreters
- The anchor verifier for blocking and non-blocking concurrent software
- Towards a formal foundation of intermittent computing
- Towards a unified proof framework for automated fixpoint reasoning using matching logic
- Unifying execution of imperative generators and declarative specifications
- Verifying and improving Halide's term rewriting system with program synthesis
- Verifying replicated data types with typeclass refinements in Liquid Haskell
- WATCHER: in-situ failure diagnosis
- World age in Julia: optimizing method dispatch in the presence of eval
- ιDOT: a DOT calculus with object initialization