Copertina

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Su, Yuheng, Bu, Tianjun, Yang, Qiusong, Ci, Yiwei, Tian, Enyuan
Natura:	Preprint
Pubblicazione:	2026
Soggetti:	Logic in Computer Science Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3
di: Su, Yuheng, et al.
Pubblicazione: (2025)

Deeply Optimizing the SAT Solver for the IC3 Algorithm
di: Su, Yuheng, et al.
Pubblicazione: (2025)

AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
di: Tian, Enyuan, et al.
Pubblicazione: (2025)

TIUP: Effective Processor Verification with Tautology-Induced Universal Properties
di: Li, Yufeng, et al.
Pubblicazione: (2024)

The rIC3 Hardware Model Checker
di: Su, Yuheng, et al.
Pubblicazione: (2025)

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
di: Bharti, Varun, et al.
Pubblicazione: (2025)

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
di: Barth, Max, et al.
Pubblicazione: (2025)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
di: Cristiá, Maximiliano, et al.
Pubblicazione: (2022)

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
di: King, Daragh, et al.
Pubblicazione: (2025)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
di: Zilberstein, Noam, et al.
Pubblicazione: (2024)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
di: Rustenholz, Louis, et al.
Pubblicazione: (2024)

Can LLMs Perform Synthesis?
di: Egolf, Derek, et al.
Pubblicazione: (2026)

Provenance Guided Rollback Suggestions
di: Zhao, David, et al.
Pubblicazione: (2025)

GATlab: Modeling and Programming with Generalized Algebraic Theories
di: Lynch, Owen, et al.
Pubblicazione: (2024)

Syntax-Guided Automated Program Repair for Hyperproperties
di: Beutner, Raven, et al.
Pubblicazione: (2024)

Realizability in Semantics-Guided Synthesis Done Eagerly
di: Meyer, Roland, et al.
Pubblicazione: (2024)

Verifying Solutions to Semantics-Guided Synthesis Problems
di: Murphy, Charlie, et al.
Pubblicazione: (2024)

Meaningfulness and Genericity in a Subsuming Framework
di: Kesner, Delia, et al.
Pubblicazione: (2024)

Linearization via Rewriting (Long Version)
di: Lago, Ugo Dal, et al.
Pubblicazione: (2025)

Zippy -- Generic White-Box Proof Search with Zippers
di: Kappelmann, Kevin
Pubblicazione: (2025)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
di: Klinkenberg, Lutz, et al.
Pubblicazione: (2023)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
di: Stübinger, Terru, et al.
Pubblicazione: (2023)

Equational Bit-Vector Solving via Strong Gröbner Bases
di: Song, Jiaxin, et al.
Pubblicazione: (2024)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
di: Li, Runming, et al.
Pubblicazione: (2025)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
di: Zimmerman, Conrad, et al.
Pubblicazione: (2024)

Kleene algebra with commutativity conditions is undecidable
di: de Amorim, Arthur Azevedo, et al.
Pubblicazione: (2024)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
di: Vollmer, Victoria, et al.
Pubblicazione: (2024)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
di: Elad, Neta, et al.
Pubblicazione: (2023)

Model Checking Probabilistic Operator Precedence Automata
di: Pontiggia, Francesco, et al.
Pubblicazione: (2024)

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
di: Jiang, Hongjian, et al.
Pubblicazione: (2025)

BLAST: Benchmarking LLMs with ASP-based Structured Testing
di: Santana, Manuel Alejandro Borroto, et al.
Pubblicazione: (2026)

Pearce's Characterisation in an Epistemic Domain
di: Su, Ezgi Iraz
Pubblicazione: (2025)

Impredicativity in Linear Dependent Type Theory
di: Speight, Sam, et al.
Pubblicazione: (2026)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
di: Kaye, George
Pubblicazione: (2025)

CSLib: The Lean Computer Science Library
di: Barrett, Clark, et al.
Pubblicazione: (2026)

Recursive Mutexes in Separation Logic
di: Du, Ke, et al.
Pubblicazione: (2026)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
di: Zhang, Cheng, et al.
Pubblicazione: (2026)

Symmetric Proofs of Parameterized Programs
di: Cheng, Ruotong, et al.
Pubblicazione: (2026)

Type Theory With Erasure
di: Theocharis, Constantine, et al.
Pubblicazione: (2026)

A Program Logic for Abstract (Hyper)Properties
di: Baldan, Paolo, et al.
Pubblicazione: (2026)