Paper: Barista - Synthesizing Typestate Specifications with LLM Agents

This week, we are presenting the Barista paper at ASE'2026, and by 'we', I mean Catarina Gamboa, who is leading this work. When trying to adopt LiquidJava, an annotation-based language that adds refinements to types, in your Java project, you will have to write the annotations for any library that you use, including the Java Standard Library. This is just a huge amount of work for your simple application. This issue is shared by LiquidHaskell, Frama-C's ACML and Java Modeling Language. Roughly one year ago, we wanted to explore if we could have LLMs read the documentation (English) and write the specifications for libraries. We focused on a few examples from the Java Standard Library and, given that one year ago LLMs generated more slop than they do today, we came up with an agentic workflow that combined LLM to translate English to an Automata, and the Automata to specification. And by having the automata, we could create positive and negative examples of method call sequences that…