Skip to yearly menu bar Skip to main content


Poster
in
Workshop: VerifAI: AI Verification in the Wild

ABSINT-AI: Language Models for Abstract Interpretation

Michael Wang · Kexin Pei · Armando Solar-Lezama


Abstract:

Static program analysis is a popular technique in software engineering. Traditionalstatic analysis algorithms treat programs as sets of logical statements withwell-defined semantics. These traditional analyzers can provide guarantees of theirperformance, such as guaranteeing that they will never miss a bug. However, theyleave out lots of very rich information such as variable and field names. Languagemodels for code on the other hand, take full advantage of information such asvariable names, but it is extremely difficult to provide guarantees of their output.In this work, we present ABSINT-AI, a language model augmented static analyzerbased on abstract interpretation that combines the best of both worlds. Using alanguage model in ABSINT-AI achieves up to a 70% decrease in false positivesfor bug detection while providing guarantees of never missing a bug.

Chat is not available.