Ryan Beckett
where else to find them
linkedin:ryanbeckett
what they talk about
all 9 in the filters
where they keep going back
- NSDI2 editions2020–2023
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2024
all 7 in the filters
on a stage with
all 41 in the filters
who talks about the same things
- Aarti Gupta7 talks
- Ryan G. Scott2 talks
- David Walker15 talks
- Eric Hayden Campbell6 talks
- Ankush Desai10 talks
- Aseem Rastogi7 talks
| title | conference | date |
|---|---|---|
| Eywa: Automating Model-Based Testing using LLMs | NSDI '26 | 2026-05-04 |
Eywa uses LLMs to synthesize modular, executable protocol models (converted to code and composed via dependency graphs) and then drives KLEE-style symbolic… | ||
| Heuristic Analysis from Source Code via Symbolic-Guided Optimization | NSDI '26 | 2026-05-04 |
MetaEase analyzes heuristic source code directly, using symbolic execution (KLEE) to generate seeds per code path and a duality-based gradient for the optimal… | ||
| Efficient Multi-WAN Transport for 5G with OTTER | NSDI '25 | 2025-04-28 |
OTTER implements a multi-WAN overlay (VMs, VPN gateways, private VNETs) across an 8-region cloud topology and a controller/orchestrator/measurement-coordinator… | ||
| Kivi: Verification for Cluster Management | USENIX ATC 2024 | 2024-07-10 |
Kivi verifies Kubernetes controllers and configurations by modeling controllers, objects, and events and exhaustively exploring interleavings with model… | ||
| Diffy: Data-Driven Bug Finding for Configurations | PLDI 2024 | 2024-06-24 |
Diffy automatically synthesizes structured configuration templates with holes, then flags anomalous template parameters using unsupervised anomaly detection… | ||
| Finding Adversarial Inputs for Heuristics using Multi-level Optimization | 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24) | 2024-04-16 |
MetaOpt is a solver-backed tool that encodes heuristics and an optimal baseline as a bilevel optimization, automatically rewrites inner problems into… | ||
| MESSI: Behavioral Testing of BGP Implementations | 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24) | 2024-04-16 |
MESSI is a model-based tester that symbolically generates joint configuration–state–route triples to exercise BGP behavior, producing about 150K tests and… | ||
| Sequence Abstractions for Flexible, Line-Rate Network Monitoring | 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24) | 2024-04-16 |
A new system called FLM compiles sequence-monitoring programs to P4 that run on programmable switch ASICs, splitting specs into state management plus a regular… | ||
| Modular Control Plane Verification via Temporal Invariants | PLDI 2023 | 2023-06-17 |
Timepiece implements a temporal model and an SMT-backed verifier (C library plus harness) that replaces unsafe stable-state modular checks with temporal… | ||
| Synthesizing Runtime Programmable Switch Updates | NSDI 2023 | 2023-04-17 |
FlexPlan synthesizes step-by-step runtime P4 switch update plans using program synthesis and an SMT-based verifier, encoding intermediate states as version… | ||
| Formal Methods for Network Performance Analysis | NSDI 2023 | 2023-04-17 |
Formal analysis encodes queues and timed packet sequences in logic, uses Z3 and syntax-guided synthesis to produce concise constraint-based workloads (not… | ||
| Test Coverage for Network Configurations | NSDI 2023 | 2023-04-17 |
NetCov identifies which router configuration lines a test suite actually exercises by tracing data-plane facts back to contributing config lines using an… | ||
| Katra: Realtime Verification for Multilayer Networks | 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22) | 2022-04-04 |
Katra implements a new incremental verifier that models packets as a single header copy and uses partial equivalence classes plus a lazy repair of header… | ||
| SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers | 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22) | 2022-04-04 |
SCALE uses an executable RFC model to jointly generate zone files and queries and Ferret runs those tests against real servers. The pipeline uses the Zen… | ||
| Contra: A Programmable System for Performance aware Routing | NSDI 2020 | 2020-02-25 |
System compiles high-level path-ranking policies into switch-local P4 programs and a product graph that merges regex path constraints with the topology… | ||
| Finding Network Misconfigurations by Automatic Template Inference | NSDI 2020 | 2020-02-25 |
Automatic inference groups similar router config snippets into parameterized templates and flags small groups as outliers; implemented in the tool SelfStarter… | ||
| nothing matches | ||