Barista: Synthesizing Typestate Specifications with LLM Agents
Object-oriented classes encode implicit protocols that clients must follow, such as connecting a socket before sending data or opening a stream before reading. Mainstream programming languages like Java cannot validate the correct use of these protocols, but more advanced type systems, such as typestate systems, can detect these violations at compile time. However, these systems require a formalization of these implicit protocols. To overcome this limitation, we propose to extract object protocols from documentation using a combination of LLMs and test generation. We developed Barista, an agentic workflow that transforms class documentation into verifiable LiquidJava specifications through DFA-guided protocol extraction, test synthesis, and verification-driven refinement. We evaluated our approach on 35 Java classes with expert-written ground truth, achieving 87.0% precision and 68.3% recall, with 75% of specifications usable directly or with minor edits. Barista bootstraps these specifications for well-documented libraries, reducing the manual annotation burden and enabling compile-time protocol safety without specialized expertise.
Thu 15 OctDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 17:30 | Formal Aspects of Software Engineering: Specification Languages 2Research Papers / Journal First at Forum 7 Chair(s): Dominik Sobania paluno, University of Duisburg-Essen | ||
16:30 15mTalk | Barista: Synthesizing Typestate Specifications with LLM Agents Research Papers Catarina Gamboa Carnegie Mellon University and University of Lisbon, Paulo Canelas SonarSource, Ricardo Costa University of Lisbon, Marcio Caetano University of Lisbon, Jonathan Aldrich Carnegie Mellon University, Alcides Fonseca LASIGE; University of Lisbon DOI Pre-print | ||
16:45 15mTalk | SpecFSM: Extracting and Repairing Finite State Machines from Protocol Specification Documents Research Papers Xiangdong Li Beijing University of Posts and Telecommunications, DaWei Huang Beijing University of Posts and Telecommunications, Jingjing Guan Beijing University of Posts and Telecommunications, Hui Li Beijing University of Posts and Telecommunications | ||
17:00 15mTalk | Diagnosing Violations of State-based Specifications in iCFTL Journal First Cristina Stratan University of Luxembourg, Claudio Mandrioli University of Luxembourg, Domenico Bianculli University of Luxembourg DOI | ||
17:15 15mTalk | Refine2Diff: Detecting Protocol Specification–Implementation Inconsistencies via Specification-Driven Code Refinement Research Papers Yuekun Wang Singapore Management University, Lili Quan Singapore Management University (SMU), Xiaofei Xie Singapore Management University | ||