-
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
Authors:
Quang Loc Le,
Xuan-Bach D. Le
Abstract:
An 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 requi…
▽ More
An 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 have implemented the proposal in a prototype tool and evaluated it over challenging problems taken from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system.
△ Less
Submitted 2 October, 2022;
originally announced October 2022.
-
S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs
Authors:
Quang Loc Le,
Jun Sun,
Long H. Pham,
Shengchao Qin
Abstract:
Heap-manipulating programs are known to be challenging to reason about. We present a novel verifier for heap-manipulating programs called S2TD, which encodes programs systematically in the form of Constrained Horn Clauses (CHC) using a novel extension of separation logic (SL) with recursive predicates and dangling predicates. S2TD actively explores cyclic proofs to address the path explosion probl…
▽ More
Heap-manipulating programs are known to be challenging to reason about. We present a novel verifier for heap-manipulating programs called S2TD, which encodes programs systematically in the form of Constrained Horn Clauses (CHC) using a novel extension of separation logic (SL) with recursive predicates and dangling predicates. S2TD actively explores cyclic proofs to address the path explosion problem. S2TD differentiates itself from existing CHC-based verifiers by focusing on heap-manipulating programs and employing cyclic proof to efficiently verify or falsify them with counterexamples. Compared with existing SL-based verifiers, S2TD precisely specifies the heaps of de-allocated pointers to avoid false positives in reasoning about the presence of bugs. S2TD has been evaluated using a comprehensive set of benchmark programs from the SV-COMP repository. The results show that S2TD is more effective than state-of-art program verifiers and is more efficient than most of them.
△ Less
Submitted 19 September, 2022;
originally announced September 2022.
-
Bi-Abduction for Shapes with Ordered Data
Authors:
Christopher Curry,
Quang Loc Le
Abstract:
Shape analysis is of great importance for the verification of the correctness and memory-safety of heap-manipulating programs, yet such analyses have been shown to be highly difficult problems. The integration of separation logic into shape analyses has improved the effectiveness of the techniques, but the most significant advancement in this area is bi-abductive inference. Enabled by separation l…
▽ More
Shape analysis is of great importance for the verification of the correctness and memory-safety of heap-manipulating programs, yet such analyses have been shown to be highly difficult problems. The integration of separation logic into shape analyses has improved the effectiveness of the techniques, but the most significant advancement in this area is bi-abductive inference. Enabled by separation logic, bi-abduction - a combination of abductive inference and frame inference - is the key enabler for compositional reasoning, hel** to scale up verification significantly. Indeed, the success of bi-abduction has led to the development of Infer, the tool used daily to verify Facebook's codebase of millions of lines of code. However, this success currently stays largely within the shape domain. To extend this impact towards the combination of shape and arithmetic domains, in this work, we present a novel one-stage bi-abductive procedure for a combination of data structures and ordering values. The procedure is designed in the spirit of the Unfold-and-Match paradigm where the inference is utilized to derive any mismatched portion. We have also implemented a prototype solver, based on the Cyclist library, and demonstrate its capabilities over a range of benchmarks from the SL-COMP competition. The experimental results show that our proposal shows promise for the specification inference in an automated verification of heap-manipulating programs.
△ Less
Submitted 18 June, 2020;
originally announced June 2020.
-
Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning
Authors:
Long H. Pham,
Jun Sun,
Quang Loc Le
Abstract:
Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applyin…
▽ More
Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.
△ Less
Submitted 27 August, 2019;
originally announced August 2019.
-
Concolic Testing Heap-Manipulating Programs
Authors:
Long H. Pham,
Quang Loc Le,
Quoc-Sang Phan,
Jun Sun
Abstract:
Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on numeric programs. Heap-manipulating programs make extensive use of complex heap objects like trees and lists. Testing such programs is challenging due to multiple reasons. Firstly, test inputs for such program are requir…
▽ More
Concolic testing is a test generation technique which works effectively by integrating random testing generation and symbolic execution. Existing concolic testing engines focus on numeric programs. Heap-manipulating programs make extensive use of complex heap objects like trees and lists. Testing such programs is challenging due to multiple reasons. Firstly, test inputs for such program are required to satisfy non-trivial constraints which must be specified precisely. Secondly, precisely encoding and solving path conditions in such programs are challenging and often expensive. In this work, we propose the first concolic 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.
△ Less
Submitted 12 July, 2019;
originally announced July 2019.
-
Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
Authors:
Quang Loc Le
Abstract:
In 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). T…
▽ More
In 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.
△ Less
Submitted 23 May, 2018;
originally announced May 2018.
-
Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
Authors:
Long H. Pham,
Quang Loc Le,
Quoc-Sang Phan,
Jun Sun,
Shengchao Qin
Abstract:
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs bas…
▽ More
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs based on separation logic. The essence of our proposal is context-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two ways. Firstly, our approach is based on separation logic, which allows us to precisely capture preconditions of heap-based programs so that we avoid generating invalid test inputs. Secondly, we generate only fully initialized test inputs, which are more useful in practice compared to those partially initialized test inputs generated by the state-of-the-art tools. We have implemented our approach as a tool, called Java StarFinder, and evaluated it on a set of programs with complex heap inputs. The results show that our approach significantly reduces the number of invalid test inputs and improves the test coverage.
△ Less
Submitted 16 September, 2019; v1 submitted 16 December, 2017;
originally announced December 2017.
-
Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
Authors:
Quang Loc Le
Abstract:
This paper presents an approach to lemma synthesis to support advanced inductive entailment procedures based on separation logic. We first propose a mechanism where lemmas are automatically proven and systematically applied. The lemmas may include universal guard and/or unknown predicate. While the former is critical for expressivity, the latter is essential for supporting relationships between mu…
▽ More
This paper presents an approach to lemma synthesis to support advanced inductive entailment procedures based on separation logic. We first propose a mechanism where lemmas are automatically proven and systematically applied. The lemmas may include universal guard and/or unknown predicate. While the former is critical for expressivity, the latter is essential for supporting relationships between multiple predicates. We further introduce lemma synthesis to support (i) automated inductive reasoning together with frame inference and (ii) theorem exploration. For (i) we automatically discover and prove auxiliary lemmas during an inductive proof; and for (ii) we automatically generate a useful set of lemmas to relate user-defined or system-generated predicates. We have implemented our proposed approach into an existing verification system and tested its capability in inductive reasoning and theorem exploration. The experimental results show that the enhanced system can automatically synthesize useful lemmas to facilitate reasoning on a broad range of non-trivial inductive proofs.
△ Less
Submitted 12 May, 2018; v1 submitted 17 October, 2017;
originally announced October 2017.
-
A Decision Procedure for String Logic with Equations, Regular Membership and Length Constraints
Authors:
Quang Loc Le
Abstract:
In this paper, we consider the satisfiability problem for string logic with equations, regular membership and Presburger constraints over length functions. The difficulty comes from multiple occurrences of string variables making state-of-the-art algorithms non-terminating. Our main contribution is to show that the satisfiability problem in a fragment where no string variable occurs more than twic…
▽ More
In this paper, we consider the satisfiability problem for string logic with equations, regular membership and Presburger constraints over length functions. The difficulty comes from multiple occurrences of string variables making state-of-the-art algorithms non-terminating. Our main contribution is to show that the satisfiability problem in a fragment where no string variable occurs more than twice in an equation is decidable. In particular, we propose a semi-decision procedure for arbitrary string formulae with word equations, regular membership and length functions. The essence of our procedure is an algorithm to enumerate an equivalent set of solvable disjuncts for the formula. We further show that the algorithm always terminates for the aforementioned decidable fragment. Finally, we provide a complexity analysis of our decision procedure to prove that it runs, in the worst case, in factorial time.
△ Less
Submitted 11 October, 2016; v1 submitted 5 October, 2016;
originally announced October 2016.
