LLM-Integrated Declarative Program Analysis
summary
SemQL extends CodeQL with an LLM-as-oracle predicate that materializes semantic judgments (e.g., whether a method name starts with a verb, whether a string literal leaks secrets or is an untrustworthy URL) into standard CodeQL predicates, evaluated over SpotBugs samples. An algorithm decomposes queries to DNF, adds negation guards, and skips already-identified tuples to minimize LLM calls; evaluation reports 81% fewer tokens and much lower latency. Implementation is open-sourced and supports local or remote oracles.
AI-written summary · about
chapters (13)
- 0:00LLM-integrated program analysis
- 2:04LLM and static analyzer limits
- 3:28SemQL core idea
- 4:54Naming convention violation example
- 5:55Security analysis with reasoning
- 6:58SemQL syntax and integration
- 8:01Query evaluation challenges
- 10:31Optimizing LLM token usage
- 13:03Experimental evaluation
- 13:48Open-sourcing SemQL and future work
- 14:13Q&A
- 15:19Q&A
- 16:28Q&A
related talks
22mTowards Verified Code Reasoning by LLMs
53mSemantics-based program manipulation in the age of LLMs
30mPrompting Is Programming: A Query Language for Large Language Models
29mKeynote: LLMs, what are they good for?
33mLeveraging LLM Reasoning with Dual Horn Programs
01h 16mHow Will LLMs Change Haskell, Programming and Open Source?
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants