Specy: Learning Specifications for Distributed Systems from Event Traces
This program is tentative and subject to change.
Reasoning about the correctness of distributed systems is a significant challenge, with precise correctness specifications serving as an essential prerequisite to verification. However, identifying and formulating specifications remains a major hurdle for developers in practice. Specy addresses this challenge by automatically learning specifications from observable \emph{event traces} generated by message exchanges in distributed systems. The system employs a specialized grammar tailored for event-based specifications, incorporating support for quantifiers over events – a capability essential for capturing the complex behavioral patterns inherent in distributed protocols. Specy utilizes a novel learning procedure that combines grammar-based enumerative search with dynamic learning from event traces, providing effective control over the specification search. We evaluated Specy on established distributed protocols and industrial case studies, demonstrating its ability to successfully learn important protocol specifications. Specy can discover previously unidentified specifications overlooked by developers, automatically derive inductive invariants that were previously constructed manually for verification purposes, and, through run-time monitoring in production systems, reveal gaps in testing coverage – highlighting opportunities to leverage specifications in practice.
This program is tentative and subject to change.
Mon 5 OctDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | |||
10:30 18mTalk | Debugging Debugging Information Using Dynamic Call Trees OOPSLA DOI Pre-print | ||
10:48 18mTalk | Automated Debugging of Datalog Programs OOPSLA Jiashen Wei Nanjing University, China, Baoyuan Luo Nanjing University, China, Runshuo Xie Nanjing University, China, Yun Qi Nanjing University, Yiyu Zhang Nanjing University, Xizao Wang Nanjing University, Xintao Niu Nanjing University, Zhiqiang Zuo Nanjing University | ||
11:06 18mTalk | Accurate Residues for Floating-Point Debugging OOPSLA | ||
11:24 18mTalk | Prosecutor: Bayesian Counterfactual Fault Localization OOPSLA Sara Baradaran University of Southern California, Yifei Huang University of Southern California, Wei Le Iowa State University, Mukund Raghothaman University of Southern California | ||
11:42 18mTalk | Specy: Learning Specifications for Distributed Systems from Event Traces OOPSLA Mike He Princeton University, Ankush Desai Snowflake, Aishwarya Jagarapu Amazon Web Services, Doug Terry LinkedIn, Sharad Malik Princeton University, Aarti Gupta Princeton University Pre-print | ||