221 research outputs found
A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints
No full textIn this work, we consider the satisfiability problem in a logic that combines word equations over string variables denoting words of unbounded lengths, regular languages to which words belong and Presburger constraints on the length of words. We present a novel decision procedure over two decidable fragments that include quadratic word equations (i.e., each string variable occurs at most twice). The proposed procedure reduces the problem to solving the satisfiability in the Presburger arithmetic. The procedure combines two main components: (i) an algorithm to derive a complete set of all solutions of conjunctions of word equations and regular expressions; and (ii) two methods to precisely compute relational constraints over string lengths implied by the set of all solutions. We have implemented a prototype tool and evaluated it over a set of satisfiability problems in the logic. The experimental results show that the tool is effective and efficient
Automated Verification of Complete Specification with Shape Inference
No full textPh.DDOCTOR OF PHILOSOPH
Compositional Satisfiability Solving in Separation Logic
No full textWe introduce a novel decision procedure to the satisfiability problem in array separation logic combined with general inductively defined predicates and arithmetic. Our proposal differentiates itself from existing works by solving satisfiability through compositional reasoning. First, following Fermat’s method of infinite descent, it infers for every inductive definition a “base” that precisely characterises the satisfiability. It then utilises the base to derive such a base for any formula where these inductive predicates reside in. Especially, we identify an expressive decidable fragment for the compositionality. We have implemented the proposal in a tool and evaluated it over challenging problems. The experimental results show that the compositional satisfiability solving is efficient and our tool is effective and efficient when compared with existing solvers
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
No full textAn efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent.
This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our procedure is efficient and does not require back-tracking; it uses normalisation rules that help avoid the introduction of disjunction in the consequent. Moreover, our decidable fragment is sufficiently expressive: It is based on compositional predicates and can capture a wide range of data structures, including sorted and nested list segments, skip lists with fast-forward pointers, and binary search trees. We implemented the proposal in a prototype tool, called S2SLin
, and evaluated it over challenging problems from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system
Data update for Vietnam economics research institutions as of October 2021
No full textResearch data in Vietnam have been fragmented, and this is a long-standing fact. Although several universities repeatedly claim that they have been the leading players in economics research, actual data may not support their claims. In a recent attempt, Dr. Le Van Ut of Ton Duc Thang University in Ho Chi Minh City compiled a data set to figure out Vietnamese scholars’ internal capacity. Nonetheless, this report covers too large a spectrum that economics research has little weight. In fact, only one person represents the humanities and social sciences in Dr. Ut’s 22-person lifetime achievement list, and only a handful in his 2021 most influential list
Concolic Testing Heap-Manipulating Programs
No full textConcolic testing is a test generation technique which works effectivelyby integrating random testing generation and symbolic execution. Existing concolictesting engines focus on numeric programs. Heap-manipulating programsmake extensive use of complex heap objects like trees and lists. Testing suchprograms is challenging due to multiple reasons. Firstly, test inputs for such programsare required to satisfy non-trivial constraints which must be specified precisely.Secondly, precisely encoding and solving path conditions in such programsare challenging and often expensive. In this work, we propose the firstconcolic testing engine called CSF for heap-manipulating programs based on separation logic. CSF effectively combines specification-based testing and concolic execution for test input generation. It is evaluated on a set of challenging heap-manipulating programs. The results show that CSF generates valid test inputs with high coverage efficiently. Furthermore, we show that CSF can be potentially used in combination with precondition inference tools to reduce the user effort
Decision procedure for separation logic with inductive predicates and Presburger arithmetic
No full textThis paper considers the satisfiability problem of symbolic heaps in separation logic with Presburger arithmetic and inductive definitions. First the system without any restrictions is proved to be undecidable. Secondly this paper proposes some syntactic restrictions for decidability. These restrictions are identified based on a new decidable subsystem of Presburger arithmetic with inductive definitions. In the subsystem of arithmetic, every inductively defined predicate represents an eventually periodic set and can be eliminated. The proposed system is quite general as it can handle the satisfiability of the arithmetical parts of fairly complex predicates such as sorted lists and AVL trees. Finally, we prove the decidability by presenting a decision procedure for symbolic heaps with the restricted inductive definitions and arithmetic
Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning
No full textMinistry of Education (MOE) Singapore Academic Tertiary Education Research Fund Tier
Satisfiability Modulo Heap-Based Programs
No full textIn this work, we present a semi-decision procedure for a fragment of separation logic with user-defined predicates and Presburger arithmetic. To check the satisfiability of a formula, our procedure iteratively unfolds the formula and examines the derived disjuncts. In each iteration, it searches for a proof of either satisfiability or unsatisfiability. Our procedure is further enhanced with automatically inferred invariants as well as detection of cyclic proof. We also identify a syntactically restricted fragment of the logic for which our procedure is terminating and thus complete. This decidable fragment is relatively expressive as it can capture a range of sophisticated data structures with non-trivial pure properties, such as size, sortedness and near-balanced. We have implemented the proposed solver and a new system for verifying heap-based programs. We have evaluated our system on benchmark programs from a software verification competition
Biến đổi khí hậu – ngành nghiên cứu còn nhiều bất bình đẳng
No full textNhững năm gần đây, chủ đề nghiên cứu về biến đổi khí hậu ngày càng nở rộ trên toàn cầu. Nhưng có một sự thật đáng buồn là số bài nghiên cứu có chất lượng đến từ các học giả ở các nước đang phát triển chỉ chiếm một tỉ lệ khá nhỏ, mặc dù các nước này đóng góp rất lớn, đặc biệt về dữ liệu để đánh giá tác động của biến đổi khí hậu
- …
