A5100381605- Formal Methods in Verification
- Logic, programming, and type systems
- Software Testing and Debugging Techniques
- Web Application Security Vulnerabilities
- semigroups and automata theory
- Logic, Reasoning, and Knowledge
- Security and Verification in Computing
- Advanced Database Systems and Queries
- Distributed systems and fault tolerance
- Advanced Malware Detection Techniques
- Natural Language Processing Techniques
- Advanced Graph Theory Research
- Machine Learning and Algorithms
- Semantic Web and Ontologies
- Network Packet Processing and Optimization
- Algorithms and Data Compression
- Digital and Cyber Forensics
- Complexity and Algorithms in Graphs
- DNA and Biological Computing
- Web Data Mining and Analysis
- Embedded Systems Design Techniques
- Error Correcting Code Techniques
- Advanced Algebra and Logic
- Advanced Data Storage Technologies
- Synthetic Organic Chemistry Methods
Changsha University of Science and Technology
2025
Chinese Academy of Sciences
2014-2024
Institute of Software
2014-2024
University of Chinese Academy of Sciences
2022-2024
Hunan University of Finance and Economics
2023
Shanghai Key Laboratory of Trustworthy Computing
2020
East China Normal University
2020
Université Paris Cité
2015-2017
Délégation Paris 7
2015-2017
Laboratoire d'Informatique Algorithmique: Fondements et Applications
2016
The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, with such applications as symbolic execution strings automated detection cross-site scripting (XSS) vulnerabilities web applications. A (symbolic) given a finite sequence assignments assertions (i.e. without loops), its amounts to determining the existence inputs that yield successful execution. Modern programming languages (e.g. JavaScript, PHP, Python)...
The theory of strings with concatenation has been widely argued as the basis constraint solving for verifying string-manipulating programs. However, this is far from adequate expressing many string constraints that are also needed in practice; example, use regular (pattern matching against a expression), and string-replace function (replacing either first occurrence or all occurrences ``pattern'' constant/variable/regular expression by ``replacement'' constant/variable), among others. Both...
Regular expressions are a classical concept in formal language theory. programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), well additional features capturing groups and references. While symbolic execution programs containing RegExes appeals to string solvers natively supporting important RegEx, solver is hitherto missing. In this paper, we propose the first theory that provides support. The key idea our introduce new...
We investigate the impact of initial public offering a focal firm on its competitors' innovation, with novel measure peer similarity annual reports via Text-Based Network Industry Classifications. find higher between firms and competitors predicts greater innovation output competitors. Further, we experience increased pressure R&D investment after IPOs firms, which serve as two channels supporting main findings. Additionally, this phenomenon is weakened for high financing constraints intensity.
Ant-based routing protocols for mobile ad hoc networks (MANETs) have been widely explored, but most of them are essentially single-path methods that tend to impose a heavy burden on the hosts along shortest path from source destination. In this paper, we combine swarm intelligence and node-disjoint multipath alleviate these problems. A novel approach called ant-based energy-aware disjoint algorithm (AEADMRA) is proposed. AEADMRA based especially ant colony-based meta heuristic. can discover...
The analysis of datalog programs over relational structures has been studied in depth, most notably the problem containment. problems that have considered were shown to be undecidable with exception (i) containment arbitrary nonrecursive ones, (ii) monadic programs, and (iii) emptiness. In this paper, we are concerned a much less problem, data trees. We show is more complex for trees than structures. particular, prove three aforementioned But practice, (e.g., XML trees) often bounded depth....
We propose a novel automata model over the alphabet of rational numbers, which we call register rationals (RA <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ℚ</sub> ). It reads sequence numbers and outputs another number. RA is an extension well-known (RA) infinite alphabets, are finite equipped with number registers/variables for storing values. Like in standard RA, allows both equality ordering tests between It, moreover, to perform linear...
Pushdown multi-agent systems, modeled by pushdown game structures (PGSs), are an important paradigm of infinite-state systems. Alternating-time temporal logics well-known specification formalisms for where the selective path quantifier is introduced to reason about strategies agents. In this paper, we investigate model checking algorithms variants alternating-time over PGSs, initiated Murano and Perelli at IJCAI'15. We first give a triply exponential-time algorithm ATL* PGSs. The based on...
This paper proposes a data tree-rewriting framework for modeling evolving documents. The is close to Guarded Active XML, platform used handling XML repositories through web services. We focus on automatic verification of properties documents that can contain from an infinite domain. establish the boundaries decidability, and show {\em positive} fragment handle recursive service calls decidable. also consider bounded model-checking in our it $\nexptime$-complete.
Data automata on data words is a decidable model proposed by Boja\'nczyk et al. in 2006. Class automata, introduced recently and Lasota, an extension of which unifies different models words. The nonemptiness class undecidable, since can simulate two-counter machines. In this paper, called with priority condition, restricts but strictly extends proposed. decidability obtained establishing correspondence multicounter automata. This also completes the picture links between various conditions...