swear01

Vocabulary-Guided CEGAR with LLM Predicate Injection

Project Report — Updated 2026-05-27

---

Executive Summary

This project investigates whether LLM-generated predicates can accelerate CEGAR-based predicate abstraction in CPAchecker. The key finding is that useful predicates should not be treated only as locally entailed invariants. Instead, many useful formulas are abstraction predicates: Boolean features that predicate abstraction should track, regardless of whether they are locally true.

swear01

Pono + LLM Lemma Generalization — 開發進度報告 (2026-05-25)

Pono + LLM Lemma Generalization — 開發進度報告 (2026-05-25)

Pono + LLM Lemma Generalization — 開發進度報告 (2026-05-25)

Pono + LLM Lemma Generalization — 開發進度報告 (2026-05-25)

Pono + LLM Lemma Generalization — Design & Progress