Author name cluster

Fu Song

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

FM Conference 2026 Conference Paper

Can LLM Aid in Solving Constraints with Inductive Definitions?

Weizhi Feng
Shidong Shen
Jiaxiang Liu
Taolue Chen
Fu Song
Zhilin Wu

Abstract Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e. g. , abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

DOI

AAAI Conference 2025 Conference Paper

Training Verification-Friendly Neural Networks via Neuron Behavior Consistency

Zongxin Liu
Zhe Zhao
Fu Song
Jun Sun
Pengfei Yang
Xiaowei Huang
Lijun Zhang

Formal verification provides critical security assurances for neural networks, yet its practical application suffers from the long verification time. This work introduces a novel method for training verification-friendly neural networks, which are robust, easy to verify, and relatively accurate. Our method integrates neuron behavior consistency into the training process, making neuron activation states remain consistent across different inputs within a local neighborhood. This reduces the number of unstable neurons and tightens the bounds of neurons thereby enhancing the network's verifiability. We evaluated our method using the MNIST, Fashion-MNIST, and CIFAR-10 datasets with various network architectures. The experimental results demonstrate that networks trained using our method are verification-friendly across different radii and architectures, whereas other tools fail to maintain verifiability as the radius increases. Additionally, we show that our method can be combined with existing approaches to further improve the verifiability of networks.

PDF Details DOI

AAAI Conference 2019 Conference Paper

Probabilistic Alternating-Time µ -Calculus

Fu Song
Yedi Zhang
Taolue Chen
Yu Tang
Zhiwu Xu

Reasoning about strategic abilities is key to an AI system consisting of multiple agents with random behaviors. We propose a probabilistic extension of Alternating µ-Calculus (AMC), named PAMC, for reasoning about strategic abilities of agents in stochastic multi-agent systems. PAMC subsumes existing logics AMC and PµTL. The usefulness of PAMC is exemplified by applications in genetic regulatory networks. We show that, for PAMC, the model checking problem is in UP∩co-UP, and the satisfiability problem is EXPTIME-complete, both of which are the same as those for AMC. Moreover, PAMC admits the small model property. We implement the satisfiability checking procedure in a tool PAMCSolver.

PDF Details

I&C Journal 2018 Journal Article

Analyzing pushdown systems with stack manipulation

Fu Song

Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems (PDSs) by associating each transition rule with a transduction, which allows to inspect and modify the stack content at each step of a transition rule. In this work, we propose two novel saturation procedures to compute p r e ⁎ ( C ) and p o s t ⁎ ( C ) for finite TrPDSs. From these two saturation procedures, we present two algorithms to compute p r e ⁎ ( C ) and p o s t ⁎ ( C ) that are suitable for implementation. We also show that the algorithms for computing p r e ⁎ ( C ) and p o s t ⁎ ( C ) also work for weak finite TrPDSs, where closure is defined with respect to the underlying PDSs. These results are extended to left contextual TrPDSs, which is an extension of finite TrPDSs. Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing and low-level assembly programs that manipulate the program stack content via a stack pointer.

Details DOI

AAAI Conference 2016 Conference Paper

Global Model Checking on Pushdown Multi-Agent Systems

Taolue Chen
Fu Song
Zhilin Wu

Pushdown multi-agent systems, modeled by pushdown game structures (PGSs), are an important paradigm of inﬁnite-state multi-agent systems. Alternatingtime temporal logics are well-known speciﬁcation formalisms for multi-agent systems, where the selective path quantiﬁer is introduced to reason about strategies of agents. In this paper, we investigate model checking algorithms for variants of alternating-time temporal logics over PGSs, initiated by Murano and Perelli at IJCAI’15. We ﬁrst give a triply exponential-time model checking algorithm for ATL∗ over PGSs. The algorithm is based on the saturation method, and is the ﬁrst global model checking algorithm with a matching lower bound. Next, we study the model checking problem for the alternating-time μ-calculus. We propose an exponential-time global model checking algorithm which extends similar algorithms for pushdown systems and modal μ-calculus. The algorithm admits a matching lower bound, which holds even for the alternation-free fragment and ATL.

PDF Details

I&C Journal 2016 Journal Article

On temporal logics with data variable quantifications: Decidability and complexity

Fu Song
Zhilin Wu

Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. Grumberg, Kupferman and Sheinvald initiated the research on this topic recently and obtained several interesting results. However, there is still a lack of systematic investigation on the theoretical aspects of the variable extensions of temporal logics. Our goal in this paper is to fill this gap. Around this goal, we make the following choices: 1. We consider the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), and allow arbitrary nestings of variable quantifications with Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL). 2. We investigate the decidability and complexity of both the satisfiability and model checking problems, over both finite and infinite words (trees). In particular, we obtain the following results: Existential variable quantifiers or one single universal quantifier in the beginning already entail the undecidability of the satisfiability problems of both VLTL and VCTL, over both finite and infinite words (trees); if only existential path quantifiers are used in VCTL, then the satisfiability problem (over finite trees) is decidable, no matter which variable quantifiers are available; for VLTL formulae with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variables, then its satisfiability problem becomes decidable, over both finite and infinite words; based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.

Details DOI

IJCAI Conference 2016 Conference Paper

Verifying Pushdown Multi-Agent Systems against Strategy Logics

Taolue Chen
Fu Song
Zhilin Wu

In this paper, we investigate model checking algorithms for variants of strategy logic over pushdown multi-agent systems, modeled by pushdown game structures (PGSs). We consider various fragments of strategy logic, i. e. , SL[CG], SL[DG], SL[1G] and BSIL. We show that the model checking problems on PGSs for SL[CG], SL[DG] and SL[1G] are 3EXTIME-complete, which are not harder than the problem for the subsumed logic ATL*. When BSIL is concerned, the model checking problem becomes 2EXPTIME-complete. Our algorithms are automata-theoretic and based on the saturation technique, which are amenable to implementations.

PDF Details

TCS Journal 2014 Journal Article

Efficient CTL model-checking for pushdown systems

Fu Song
Tayssir Touili

Pushdown systems (PDS) are well adapted to model sequential programs with (possibly recursive) procedure calls. Therefore, it is important to have efficient model checking algorithms for PDSs. We consider in this paper CTL model checking for PDSs. We consider the “standard” CTL model checking problem where whether a configuration of a PDS satisfies an atomic proposition or not depends only on the control state of the configuration. We consider also CTL model checking with regular valuations, where the set of configurations in which an atomic proposition holds is a regular language. We reduce these problems to the emptiness problem in Alternating Büchi Pushdown Systems, and we give an algorithm to solve this emptiness problem. Our algorithms are more efficient than the other existing algorithms for CTL model checking for PDSs in the literature. We implemented our techniques in a tool, and we applied it to different case studies. Our results are encouraging. In particular, we were able to confirm the existence of known bugs in Linux source code.

Details DOI