OOPSLA 2022
92 papers
- A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency
- A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoning
- A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model
- A concurrent program logic with a future and history
- A fast in-place interpreter for WebAssembly
- A general construction for abstract interpretation of higher-order automatic differentiation
- A study of inline assembly in solidity smart contracts
- AnICA: analyzing inconsistencies in microarchitectural code analyzers
- Applying cognitive principles to model-finding output: the positive value of negative information
- Automated transpilation of imperative to functional code using neural-guided program synthesis
- BFF: foundational and automated verification of bitfield-manipulating programs
- Bridging the semantic gap between qualitative and quantitative models of distributed systems
- Bugs in Quantum computing platforms: an empirical study
- C to checked C by 3c
- C4: verified transactional objects
- CAAT: consistency as a theory
- Can guided decomposition help end-users write larger block-based programs? a mobile robot experiment
- Checking equivalence in a non-strict language
- Coeffects for sharing and mutation
- Compilation of dynamic sparse tensor algebra
- Complexity-guided container replacement synthesis
- Compositional embeddings of domain-specific languages
- Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
- Concurrent size
- Consistency-preserving propagation for SMT solving of concurrent program verification
- Coverage-guided tensor compiler fuzzing with joint IR-pass mutation
- Data-driven lemma synthesis for interactive proofs
- Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
- Elipmoc: advanced decompilation of Ethereum smart contracts
- End-to-end translation validation for the halide language
- Fast shadow execution for debugging numerical errors using error free transformations
- Finding real bugs in big programs with incorrectness logic
- First-class names for effect handlers
- Fractional resources in unbounded separation logic
- Functional collection programming with semi-ring dictionaries
- Generic go to go: dictionary-passing, monomorphisation, and hybrid
- High-level effect handlers in C++
- Highly illogical, Kirk: spotting type mismatches in the large despite broken contracts, unsound types, and too many linters
- Implementing and verifying release-acquire transactional memory in C11
- Incremental type-checking for free: using scope graphs to derive incremental type-checkers
- Indexing the extended Dyck-CFL reachability for context-sensitive program analysis
- Intrinsically-typed definitional interpreters à la carte
- Katara: synthesizing CRDTs with verified lifting
- Language-parametric static semantic code completion
- Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities
- Linear types for large-scale systems verification
- MLstruct: principal type inference in a Boolean algebra of structural types
- Model checking for a multi-execution memory model
- Model-guided synthesis of inductive lemmas for FOL with least fixpoints
- Modular verification of op-based CRDTs in separation logic
- Monadic and comonadic aspects of dependency analysis
- Necessity specifications for robustness
- Neural architecture search using property guided synthesis
- Neurosymbolic repair for low-code formula languages
- On incorrectness logic for Quantum programs
- Optimal heap limits for reducing browser memory use
- Oracle-free repair synthesis for floating-point programs
- Overwatch: learning patterns in code edit sequences
- Parsing randomness
- Plausible sealing for gradual parametricity
- Proof transfer for fast certification of multiple approximate neural networks
- Proving hypersafety compositionally
- Purity of an ST monad: full abstraction by semantically typed back-translation
- Quantitative strongest post: a calculus for reasoning about the flow of quantitative information
- Reasoning about distributed reconfigurable systems
- SHARP: fast incremental context-sensitive pointer analysis for Java
- Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing
- Scalable linear invariant generation with Farkas' lemma
- Scalable verification of GNN-based job schedulers
- Semi-symbolic inference for efficient streaming probabilistic programming
- Seq2Parse: neurosymbolic parse error repair
- SigVM: enabling event-driven execution for truly decentralized smart contracts
- Solo: a lightweight static analysis for differential privacy
- Specification-guided component-based synthesis from effectful libraries
- Symbolic execution for randomized programs
- Synthesis-powered optimization of smart contracts via data type refactoring
- Synthesizing abstract transformers
- Synthesizing axiomatizations using logic learning
- Synthesizing code quality rules from examples
- Synthesizing fine-grained synchronization protocols for implicit monitors
- Taming transitive redundancy for context-free language reachability
- The essence of online data processing
- The road not taken: exploring alias analysis based optimizations missed by the compiler
- This is the moment for probabilistic loops
- Tower: data structures in Quantum superposition
- Translating canonical SQL to imperative code in Coq
- Type-directed synthesis of visualizations from natural language queries
- UniRec: a unimodular-like framework for nested recursions and loops
- Veracity: declarative multicore programming with commutativity
- Verified compilation of Quantum oracles
- Weighted programming: a programming paradigm for specifying mathematical models
- Wildcards need witness protection