Source author record

Cong Tian

Cong Tian appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Formal Languages and Automata Theory Artificial Intelligence Software Engineering

Catalog footprint

What is connected

7works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2026arXiv

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation

Formal specification is essential for rigorous program verification, yet writing correct specifications remains costly and difficult to automate. Although large language models (LLMs) and agents have shown promising progress, their true capabilities and failure modes remain unclear. We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs. We introduce LiveFMBench, a continuously evolving benchmark of 630 ACSL (ANSI/ISO C Specification Language)-annotated C programs, including 360 newly collected cases designed to mitigate data leakage. Using this benchmark, we evaluate direct prompting with different sampling sizes, reasoning-enabled (thinking mode) inference, the agentic pipeline, and perform a fine-grained failure analysis. Experimental results reveal that naive evaluation substantially overestimates performance because models under direct prompting may exhibit unfaithful behaviors, such as deceiving automated provers or ignoring code-context constraints; after excluding such cases, the true specification generation accuracy drops by approximately 20\%. We further find that both increased sampling and thinking mode significantly improve success rates, with smaller models benefiting more from thinking mode. Agentic pipelines are particularly effective under low sampling budgets and on harder datasets. Failure analysis further shows that incorrect loop invariants are the dominant error type, while agentic pipelines notably reduce assertion errors. These results expose fundamental limitations in current LLM-based approaches and suggest they remain far from replacing human-authored formal specifications. We release LiveFMBench at https://huggingface.co/datasets/fm-universe/Live-FM-Bench and all evaluation artifacts to support future research.

preprint2020arXiv

Making Streett Determinization Tight

Optimal determinization construction of Streett automata is an important research problem because it is indispensable in numerous applications such as decision problems for tree temporal logics, logic games and system synthesis. This paper presents a transformation from nondeterministic Streett automata (NSA) with $n$ states and $k$ Streett pairs to equivalent deterministic Rabin transition automata (DRTA) with $n^{5n}(n!)^{n}$ states, $O(n^{n^2})$ Rabin pairs for $k=ω(n)$ and $n^{5n}k^{nk}$ states, $O(k^{nk})$ Rabin pairs for $k=O(n)$. This improves the state of the art Streett determinization construction with $n^{5n}(n!)^{n+1}$ states, $O(n^2)$ Rabin pairs and $n^{5n}k^{nk}n!$ states, $O(nk)$ Rabin pairs, respectively. Moreover, deterministic parity transition automata (DPTA) are obtained with $3(n(n+1)-1)!(n!)^{n+1}$ states, $2n(n+1)$ priorities for $k=ω(n)$ and $3(n(k+1)-1)!n!k^{nk}$ states, $2n(k+1)$ priorities for $k=O(n)$, which improves the best construction with $n^{n}(k+1)^{n(k+1)}(n(k+1)-1)!$ states, $2n(k+1)$ priorities. Further, we prove a lower bound state complexity for determinization construction from NSA to deterministic Rabin (transition) automata i.e. $n^{5n}(n!)^{n}$ for $k=ω(n)$ and $n^{5n}k^{nk}$ for $k=O(n)$, which matches the state complexity of the proposed determinization construction. Besides, we put forward a lower bound state complexity for determinization construction from NSA to deterministic parity (transition) automata i.e. $2^{Ω(n^2 \log n)}$ for $k=ω(n)$ and $2^{Ω(nk \log nk)}$ for $k=O(n)$, which is the same as the state complexity of the proposed determinization construction in the exponent.

preprint2015arXiv

An Improved Decision Procedure for Linear Time Mu-Calculus

An improved Present Future form (PF form) for linear time $μ$-calculus ($ν$TL) is presented in this paper. In particular, the future part of the new version turns into the conjunction of elements in the closure of a formula. We show that every closed $ν$TL formula can be transformed into the new PF form. Additionally, based on the PF form, an algorithm for constructing Present Future form Graph (PFG), which can be utilized to describe models of a formula, is given. Further, an intuitive and efficient decision procedure for checking satisfiability of the guarded fragment of $ν$TL formulas based on PFG is proposed and implemented in C++. The new decision procedure has the best time complexity over the existing ones despite the cost of exponential space. Finally, a PFG-based model checking approach for $ν$TL is discussed where a counterexample can be obtained visually when a model violates a property.

preprint2015arXiv

Extending PPTL for Verifying Heap Evolution Properties

In this paper, we integrate separation logic with Propositional Projection Temporal Logic (PPTL) to obtain a two-dimensional logic, namely PPTL$^{\tiny\mbox{SL}}$. The spatial dimension is realized by a decidable fragment of separation logic which can be used to describe linked lists, and the temporal dimension is expressed by PPTL. We show that PPTL and PPTL$^{\tiny\mbox{SL}}$ are closely related in their syntax structures. That is, for any PPTL$^{\tiny\mbox{SL}}$ formula in a restricted form, there exists an "isomorphic" PPTL formula. The "isomorphic" PPTL formulas can be obtained by first an equisatisfiable translation and then an isomorphic mapping. As a result, existing theory of PPTL, such as decision procedure for satisfiability and model checking algorithm, can be reused for PPTL$^{\tiny\mbox{SL}}$.

preprint2014arXiv

Buchi Determinization Made Tighter

By separating the principal acceptance mechanism from the concrete acceptance condition of a given Büchi automaton with $n$ states,Schewe presented the construction of an equivalent deterministic Rabin transition automaton with $o((1.65n)^n)$ states via \emph{history trees}, which can be simply translated to a standard Rabin automaton with $o((2.26n)^n)$ states. Apart from the inherent simplicity, Schewe's construction improved Safra's construction (which requires $12^nn^{2n}$ states). However, the price that is paid is the use of $2^{n-1}$ Rabin pairs (instead of $n$ in Safra's construction). Further, by introducing the \emph{later introduction record} as a record tailored for ordered trees, deterministic automata with Parity acceptance condition is constructed which exactly resembles Piterman's determinization with Parity acceptance condition where the state complexity is $O((n!)^2)$ and the index complexity is $2n$.In this paper, we improve Schewe's construction to $2^{\lceil (n-1)/2\rceil}$ Rabin pairs with the same state complexity. Meanwhile, we give a new determinization construction of Parity automata with the state complexity being $o(n^2(0.69n\sqrt{n})^n)$ and index complexity being $n$.

preprint2011arXiv

Detecting Spurious Counterexamples Efficiently in Abstract Model Checking

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample in the concrete model. Accordingly, the abstract model needs to be further refined. How to check whether or not a reported counterexample is spurious is a key problem in the abstraction-refinement loop. In this paper, a formal definition for spurious path is given. Based on it, efficient algorithms for detecting spurious counterexamples are proposed.

preprint2010arXiv

Making Abstraction Refinement Efficient in Model Checking

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, although the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. And the abstract model needs to be further refined where an NP-hard state separation problem is often involved. In this paper, a novel method is presented by adding extra variables to the abstract model for the refinement. With this method, not only the NP-hard state separation problem is avoided, but also a smaller refined abstract model is obtained.