5 Search Results for "Song, Fu"

Document
DOI: 10.4230/LIPIcs.AFT.2024.7
DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance

Authors: Rundong Gan, Liyi Zhou, Le Wang, Kaihua Qin, and Xiaodong Lin

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
Decentralized Finance (DeFi) has witnessed a monumental surge, reaching 53.039 billion USD in total value locked. As this sector continues to expand, ensuring the reliability of DeFi smart contracts becomes increasingly crucial. While some users are adept at reading code or the compiled bytecode to understand smart contracts, many rely on documentation. Therefore, discrepancies between the documentation and the deployed code can pose significant risks, whether these discrepancies are due to errors or intentional fraud. To tackle these challenges, we developed DeFiAligner, an end-to-end system to identify inconsistencies between documentation and smart contracts. DeFiAligner incorporates a symbolic execution tool, SEVM, which explores execution paths of on-chain binary code, recording memory and stack states. It automatically generates symbolic expressions for token balance changes and branch conditions, which, along with related project documents, are processed by LLMs. Using structured prompts, the LLMs evaluate the alignment between the symbolic expressions and the documentation. Our tests across three distinct scenarios demonstrate DeFiAligner’s capability to automate inconsistency detection in DeFi, achieving recall rates of 92% and 90% on two public datasets respectively.
Cite as

Rundong Gan, Liyi Zhou, Le Wang, Kaihua Qin, and Xiaodong Lin. DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gan_et_al:LIPIcs.AFT.2024.7,
  author =	{Gan, Rundong and Zhou, Liyi and Wang, Le and Qin, Kaihua and Lin, Xiaodong},
  title =	{{DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{7:1--7:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.7},
  URN =		{urn:nbn:de:0030-drops-209431},
  doi =		{10.4230/LIPIcs.AFT.2024.7},
  annote =	{Keywords: Decentralized Finance Security, Large Language Models, Project Review, Symbolic Analysis, Smart Contracts}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.37
Tractability of Separation Logic with Inductive Definitions: Beyond Lists

Authors: Taolue Chen, Fu Song, and Zhilin Wu

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
In 2011, Cook et al. showed that the satisfiability and entailment can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In this paper, we investigate whether the tractability results can be extended to more expressive fragments of separation logic that allow defining data structures beyond linked lists. To this end, we introduce separation logic with a simply-nonlinear compositional inductive predicate where source, destination, and static parameters are identified explicitly (SLID[snc]). We show that if the inductive predicate has more than one source (destination) parameter, the satisfiability problem for SLID[snc] becomes intractable in general. This is exemplified by an inductive predicate for doubly linked list segments. By contrast, if the inductive predicate has only one source (destination) parameter, the satisfiability and entailment problems for SLID[snc] are tractable. In particular, the tractability results hold for inductive predicates that define list segments with tail pointers and trees with one hole.
Cite as

Taolue Chen, Fu Song, and Zhilin Wu. Tractability of Separation Logic with Inductive Definitions: Beyond Lists. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CONCUR.2017.37,
  author =	{Chen, Taolue and Song, Fu and Wu, Zhilin},
  title =	{{Tractability of Separation Logic with Inductive Definitions: Beyond Lists}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.37},
  URN =		{urn:nbn:de:0030-drops-77826},
  doi =		{10.4230/LIPIcs.CONCUR.2017.37},
  annote =	{Keywords: Separation logic, Inductive definitions, Satisfiability, Entailment}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.254
On the Satisfiability of Indexed Linear Temporal Logics

Authors: Taolue Chen, Fu Song, and Zhilin Wu

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Indexed Linear Temporal Logics (ILTL) are an extension of standard Linear Temporal Logics (LTL) with quantifications over index variables which range over a set of process identifiers. ILTL has been widely used in specifying and verifying properties of parameterised systems, e.g., in parameterised model checking of concurrent processes. However there is still a lack of theoretical investigations on properties of ILTL, compared to the well-studied LTL. In this paper, we start to narrow this gap, focusing on the satisfiability problem, i.e., to decide whether a model exists for a given formula. This problem is in general undecidable. Various fragments of ILTL have been considered in the literature typically in parameterised model checking, e.g., ILTL formulae in prenex normal form, or containing only non-nested quantifiers, or admitting limited temporal operators. We carry out a thorough study on the decidability and complexity of the satisfiability problem for these fragments. Namely, for each fragment, we either show that it is undecidable, or otherwise provide tight complexity bounds.
Cite as

Taolue Chen, Fu Song, and Zhilin Wu. On the Satisfiability of Indexed Linear Temporal Logics. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 254-267, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CONCUR.2015.254,
  author =	{Chen, Taolue and Song, Fu and Wu, Zhilin},
  title =	{{On the Satisfiability of Indexed Linear Temporal Logics}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{254--267},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.254},
  URN =		{urn:nbn:de:0030-drops-53767},
  doi =		{10.4230/LIPIcs.CONCUR.2015.254},
  annote =	{Keywords: Satisfiability, Indexed linear temporal logic, Parameterised systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.383
On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference

Authors: Fu Song, Weikai Miao, Geguang Pu, and Min Zhang

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
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. It was shown by Uezato and Minamide that TrPDSs can model PDSs with checkpoint and discrete-timed PDSs. Moreover, TrPDSs can be simulated by PDSs and the predecessor configurations pre^*(C) of a regular set C of configurations can be computed by a saturation procedure when the closure of the transductions in TrPDSs is finite. In this work, we comprehensively investigate the reachability problem of finite TrPDSs. We propose a novel saturation procedure to compute pre^*(C) for finite TrPDSs. Also, we introduce a saturation procedure to compute the successor configurations post^*(C) of a regular set C of configurations for finite TrPDSs. From these two saturation procedures, we present two efficient implementation algorithms to compute pre^*(C) and post^*(C). Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing. The TrPDS model has finite closure of transductions which results in model-checking approach for Boolean programs with call-by-reference parameter passing against safety properties.
Cite as

Fu Song, Weikai Miao, Geguang Pu, and Min Zhang. On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 383-397, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{song_et_al:LIPIcs.CONCUR.2015.383,
  author =	{Song, Fu and Miao, Weikai and Pu, Geguang and Zhang, Min},
  title =	{{On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{383--397},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.383},
  URN =		{urn:nbn:de:0030-drops-53624},
  doi =		{10.4230/LIPIcs.CONCUR.2015.383},
  annote =	{Keywords: Verification, Reachability problem, Pushdown system with transductions, Boolean programs with call-by-reference}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.253
Extending Temporal Logics with Data Variable Quantifications

Authors: Fu Song and Zhilin Wu

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
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. In this paper, we focus on the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Grumberg, Kupferman and Sheinvald recently investigated the extension of LTL with variable quantifications. They defined the extension as formulas in the prenex normal form, that is, all the variable quantifications precede the LTL formulas. Our goal in this paper is to do a relatively complete investigation on this topic. For this purpose, we define the extensions of LTL and CTL by allowing arbitrary nestings of variable quantifications, Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL), and identify the decidability frontiers of both the satisfiability and model checking problem. In particular, we obtain the following results: 1) Existential variable quantifiers or one single universal quantifier in the beginning already entails undecidability for the satisfiability problem of both VLTL and VCTL, 2) If only existential path quantifiers are used in VCTL, then the satisfiability problem is decidable, no matter which variable quantifiers are available. 3) For VLTL formulas 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 variable, then its satisfiability problem becomes decidable. Based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.
Cite as

Fu Song and Zhilin Wu. Extending Temporal Logics with Data Variable Quantifications. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 253-265, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{song_et_al:LIPIcs.FSTTCS.2014.253,
  author =	{Song, Fu and Wu, Zhilin},
  title =	{{Extending Temporal Logics with Data Variable Quantifications}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{253--265},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.253},
  URN =		{urn:nbn:de:0030-drops-48475},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.253},
  annote =	{Keywords: Temporal logics with variable quantifications, satisfiability and model checking, alternating register automata, data automata}
}
  • Refine by Author
  • 4 Song, Fu
  • 3 Wu, Zhilin
  • 2 Chen, Taolue
  • 1 Gan, Rundong
  • 1 Lin, Xiaodong
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Satisfiability
  • 1 Boolean programs with call-by-reference
  • 1 Decentralized Finance Security
  • 1 Entailment
  • 1 Indexed linear temporal logic
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2015
  • 1 2014
  • 1 2017
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact