Limin Jia
where else to find them
linkedin:limin-jia-8a209711b
what they talk about
all 12 in the filters
where they keep going back
- OOPSLA3 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2025
- SOUPS2 editions2020–2023
all 10 in the filters
on a stage with
all 43 in the filters
who talks about the same things
- Milijana Surbatovich7 talks
- Brandon Lucia7 talks
- Jonathan Aldrich17 talks
- Zhendong Su25 talks
- Deepak Garg18 talks
- Yu Jiang21 talks
| title | conference | date |
|---|---|---|
| Quantified Underapproximation via Labeled Bunches | OOPSLA 2025 | 2025-10-16 |
Presents a formal system that lets over‑ and under‑approximate analyses compose soundly by attaching a test-level modality that ranges over component internal… | ||
| Automated Exploit Generation for Node.js Packages | PLDI 2025 | 2025-06-16 |
Explode.js combines static analysis and lazy symbolic execution plus SMT solving to synthesize concrete exploits that reach vulnerable sinks through multi-call… | ||
| An MLIR Dialect for WebAssembly | WAW 2025 | 2025-01-20 |
Describes an implemented MLIR WebAssembly dialect and a compiler pipeline that skips the LLVM backend by lowering higher-level MLIR dialects (e.g., scf… | ||
| Crabtree: Rust API Test Synthesis Guided by Coverage and Type | OOPSLA 2024 | 2024-10-20 |
Crabtree is a Rust API test synthesizer that combines program synthesis with fuzzing using a coverage- and type-guided DFS to grow tests and inputs; it… | ||
| Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs | PLDI 2024 | 2024-06-24 |
Introduces Multiversion Dependency Graphs as a single, versioned object graph that records property updates and data-flow order, implemented in Graph.js and… | ||
| Automatically Enforcing Rust Trait Properties | VMCAI 2024 | 2024-01-15 |
A VS Code tool automatically generates trait-check harnesses and uses Kani bounded verification to assert trait invariants (equality… | ||
| Towards Usable Security Analysis Tools for Trigger-Action Programming | SOUPS 2023 | 2023-08-06 |
Study evaluates usable security techniques for trigger-action programming by testing 447 Prolific users on writing declarative policies vs anti-patterns using… | ||
| A Type System for Safe Intermittent Computing | PLDI 2023 | 2023-06-17 |
Curricle is a Rust-based information-flow type system that classifies variables as item-potent or non-item-potent, adds access-mode inference to decide when… | ||
| Towards End-to-End Verified TEEs via Verified Interface Conformance and Interfa... | PriSC 2023 | 2023-01-21 |
Framework formalizes TEEs as isolated compartments (Uber objects) with exclusive memory and verified pre/post interfaces, verified in isolation and compiled… | ||
| Information Flow Types, Runtime Monitors, and Gradual Typing | POPL 2021 | 2021-01-17 |
Describes a concrete design that connects static information‑flow types and dynamic monitors: a two‑point lattice (L/H), typing rules that check explicit flows… | ||
| Towards a Formal Foundation of Intermittent Computing | OOPSLA 2020 | 2020-11-15 |
Provides a formal correctness definition: an intermittent execution is correct if it is observationally equivalent to some continuous execution, and it proves… | ||
| How Risky Are Real Users' IFTTT Applets? | SOUPS 2020 | 2020-08-10 |
Study collects and analyzes 732 applets from 28 participants using a browser extension and surveys to add context beyond public IFTTT listings. An automated… | ||
| NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification | NSDI 2020 | 2020-02-25 |
NetSMC is a custom symbolic model checker that encodes stateful NFs using an existential first-order encoding and analyzes a one-packet-at-a-time model that… | ||
| Efficient and Correct Test Scheduling for Ensembles of Network Policies | NSDI '18 | 2018-04-09 |
Mikado is a scheduling layer that takes test traces from black‑box tools (bust, ATPG, simnet per uploader) and guarantees correctness by formalizing stateful… | ||
| überSpark: Enforcing Verifiable Object Abstractions for Automated... | USENIX Security '16 | 2016-08-10 |
Architecture that enforces verifiable object abstractions for compositional hypervisor verification, using Frama‑C, ComCert, SMT solvers and a hardware model… | ||
| nothing matches | ||