{"689838":{"#nid":"689838","#data":{"type":"event","title":"Princeton PhD Student Mike He presents Specy : Learning Specifications for Distributed Systems from Event Traces","body":[{"value":"\u003Cp\u003EMike He is a Princeton PhD student working at the intersection of formal verification and distributed systems. He will be presenting Specy : Learning Specifications for Distributed Systems from Event Traces, an OOPSLA \u002726 paper!\u003C\/p\u003E\u003Cp\u003EWe will be meeting Monday, April 13th, from 6:30 to 7:30 PM in CoC 053, and hope to see you there! If you can\u0027t make it in person, a zoom link is also provided.\u003C\/p\u003E\u003Cp\u003EFor any additional information, please don\u0027t hesitate to reach out via our discord:\u0026nbsp;https:\/\/discord.gg\/cyNvsmtjqY\u003C\/p\u003E\u003Cp\u003EBelow is an abstract of the work:\u003Cbr\u003EReasoning about the correctness of distributed systems is a significant challenge, with precise correctness\u003Cbr\u003Especifications serving as an essential prerequisite to verification. However, identifying and formulating\u003Cbr\u003Especifications remains a major hurdle for developers in practice. Specy addresses this challenge by automatically\u003Cbr\u003Elearning specifications from observable event traces generated by message exchanges in distributed systems.\u003Cbr\u003EThe system employs a specialized grammar tailored for event-based specifications, incorporating support\u003Cbr\u003Efor quantifiers over events \u2013 a capability essential for capturing the complex behavioral patterns inherent in\u003Cbr\u003Edistributed protocols. Specy utilizes a novel learning procedure that combines grammar-based enumerative\u003Cbr\u003Esearch with dynamic learning from event traces, providing effective control over the specification search. We\u003Cbr\u003Eevaluated Specy on established distributed protocols and industrial case studies, demonstrating its ability to\u003Cbr\u003Esuccessfully learn important protocol specifications. Specy can discover previously unidentified specifications\u003Cbr\u003Eoverlooked by developers, automatically derive inductive invariants that were previously constructed manually\u003Cbr\u003Efor verification purposes, and, through run-time monitoring in production systems, reveal gaps in testing\u003Cbr\u003Ecoverage \u2013 highlighting opportunities to leverage specifications in practice.\u003C\/p\u003E","summary":"","format":"limited_html"}],"field_subtitle":"","field_summary":[{"value":"\u003Cp\u003EMike He is a Princeton PhD student working at the intersection of formal verification and distributed systems. He will be presenting Specy : Learning Specifications for Distributed Systems from Event Traces, an OOPSLA \u002726 paper!\u003C\/p\u003E","format":"limited_html"}],"field_summary_sentence":[{"value":"Mike He is a Princeton PhD student working at the intersection of formal verification and distributed systems. He will be presenting Specy : Learning Specifications for Distributed Systems from Event Traces, an OOPSLA \u002726 paper!"}],"uid":"36837","created_gmt":"2026-04-17 16:30:50","changed_gmt":"2026-04-17 16:30:50","author":"ejenkins47","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2026-04-24T12:25:37-04:00","event_time_end":"2026-04-24T13:25:37-04:00","event_time_end_last":"2026-04-24T13:25:37-04:00","gmt_time_start":"2026-04-24 16:25:37","gmt_time_end":"2026-04-24 17:25:37","gmt_time_end_last":"2026-04-24 17:25:37","rrule":null,"timezone":"America\/New_York"},"location":"Room 053, College of Computing","extras":[],"related_links":[{"url":"https:\/\/discord.gg\/cyNvsmtjqY","title":""}],"groups":[{"id":"1182","name":"General"}],"categories":[],"keywords":[],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1791","name":"Student sponsored"}],"invited_audience":[{"id":"78761","name":"Faculty\/Staff"},{"id":"174045","name":"Graduate students"},{"id":"78751","name":"Undergraduate students"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[{"value":"\u003Cp\u003E\u003Ca href=\u0022mailto:abhamra3@gatech.edu\u0022\u003E\u003Cstrong\u003EArjun Bhamra\u003C\/strong\u003E\u003C\/a\u003E\u0026nbsp;\u003C\/p\u003E","format":"limited_html"}],"email":[],"slides":[],"orientation":[],"userdata":""}}}