~/talk

Preguss: It Analyzes, It Specifies, It Verifies

on YouTube 16m
Talkat LMPL 2025 · 2025-10-12..10-18· [ai-assisted-development, software-architecture]

speakers

name:Zhongyi Wang
links:none on file
name:Tengjie Lin
links:none on file
name:Mingshuai Chen
linkedin:mingshuai-chen-481838aa
name:Mingqi Yang
links:none on file
name:Haokun Li
links:none on file
name:Xiao Yi
links:none on file
name:Shengchao Qin
links:none on file
name:Jianwei Yin
links:none on file

resources

video:https://youtu.be/VjFQ3gtc064
slides:none on file

summary

Preguss decomposes large verification tasks into small VUnits that contain only a guard assertion and minimal context, uses static analysis (RTE alarms) to prioritize units, and invokes an LLM to synthesize interprocedural specifications (pre/postconditions and loop invariants). Evaluated on a real-world X.509 parser (~1,000+ LOC, ~20 functions), developers wrote 251 specs, Preguss auto-generates 108, humans adjust 39, cutting manual effort by 84.5%, verifies most assertions in under three hours and for under $4.

AI-written summary · about

chapters (11)

  1. 0:00Preguss framework intro
  2. 1:08Static analysis vs theorem proving
  3. 3:17Specifications in verification
  4. 5:01LLM spec synthesis challenges
  5. 6:25Interprocedural specs explained
  6. 9:20Automated verification challenges
  7. 10:03Preguss divide and conquer
  8. 11:49X509 parser evaluation
  9. 12:32Preguss results and efficiency
  10. 12:53Conclusion and future work
  11. 13:15Q&A

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.