Long Hoang Pham, Quang Loc Le, Quoc-Sang Phan et al. · arXiv (Cornell University) · 2019
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.
Cited by 0Open access
RYAN SHI HERN LEE · National University of Singapore · 2025
Bachelor's
Cited by 0
Long Hoang Pham, Quang Loc Le, Quoc-Sang Phan et al. · Lecture notes in computer science · 2019
Cited by 9
Viktor Malík, Martin Hruška, Peter Schrammel et al. · 2018
We propose a shape analysis suitable for analysis engines that perform automatic invariant inference using an SMT solver. The proposed solution includes an abstract template domain that encodes the shape of the program heap based on logical formulae over bit-vectors. It is based on computing a points-to relation between pointers and symbolic addresses of abstract memory objects. Our abstract heap domain can be combined with value domains in a straightforward manner, which particularly allows us to reason about shapes and contents of heap structures at the same time. The information obtained from the analysis can be used to prove memory safety and reachability properties, expressed by user assertions, of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and compared against state-of-the-art tools that perform the best in heap-related categories of the well-known Software Verification Competition (SV-COMP). Results show that 2LS outperforms these tools on benchmarks requiring combined reasoning about unbounded data structures and their numerical contents.
Cited by 6
Nadia Polikarpova, Ilya Sergey · Proceedings of the ACM on Programming Languages · 2019
This paper describes a deductive approach to synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. Our synthesis algorithm takes as input a pair of assertions—a pre- and a postcondition—which describe two states of the symbolic heap, and derives a program that transforms one state into the other, guided by the shape of the heap. Our approach to program synthesis is grounded in proof theory: we introduce the novel framework of Synthetic Separation Logic (SSL), which generalises the classical notion of heap entailment P ⊢ Q to incorporate a possibility of transforming a heap satisfying an assertion P into a heap satisfying an assertion Q . A synthesized program represents a proof term for a transforming entailment statement P ↝ Q , and the synthesis procedure corresponds to a proof search. The derived programs are, thus, correct by construction, in the sense that they satisfy the ascribed pre/postconditions, and are accompanied by complete proof derivations, which can be checked independently. We have implemented a proof search engine for SSL in a form of the program synthesizer called SuSLik. For efficiency, the engine exploits properties of SSL rules, such as invertibility and commutativity of rule applications on separate heaps, to prune the space of derivations it has to consider. We explain and showcase the use of SSL on characteristic examples, describe the design of SuSLik, and report on our experience of using it to synthesize a series of benchmark programs manipulating heap-based linked data structures.
Cited by 45Open access
Felix Winterstein, Kermin Fleming, Hsin-Jung Yang et al. · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2016
Memory-intensive implementations often require access to an external, off-chip memory which can substantially slow down an field-programmable gate array accelerator due to memory bandwidth limitations. Buffering frequently reused data on chip is a common approach to address this problem and the optimization of the cache architecture introduces yet another complex design space. This paper presents a high-level synthesis (HLS) design aid that automatically generates parallel multicache systems which are tailored to the specific requirements of the application. Our program analysis identifies nonoverlapping memory regions, supported by private caches, and regions which are shared by parallel units after parallelization, which are supported by coherent caches and synchronization primitives. It also decides whether the parallelization is legal with respect to data dependencies. The novelty of this paper is the focus on programs using dynamically allocated, pointer-based data structures which, while common in software engineering, remain difficult to analyze and are beyond the scope of the overwhelming majority of HLS techniques to date. Second, we devise a high-level cache performance estimation to find a heterogeneous configuration of cache sizes that maximizes the performance of the multicache system subject to an on-chip memory resource constraint. We demonstrate our technique with three case studies of applications using dynamic data structures and use Xilinx Vivado HLS as an exemplary HLS tool. We show up to 15× speedup after parallelization of the HLS implementations and the insertion of the application-specific distributed hybrid multicache architecture.
Cited by 1
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea et al. · Proceedings of the ACM on Programming Languages · 2021
Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend. In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.
Cited by 7Open access
Elvira Albert, Richard Bubel, Samir Genaim et al. · Lecture notes in computer science · 2012
Cited by 13Open access
Vesal Vojdani · 2015
Cited by 0
Longming Dong, Ji Wang, Liqian Chen · 2012
Code clone is a prevalent activity during the development of softwares. However, it is harmful to the maintenance and evolution of softwares. Current techniques for detecting code clones are most syntax-based, and cannot detect all code clones. In this paper, we present a novel semantic-based clone detection technique by obtaining the similarity about the precondition and post condition of each procedure, which are computed by a context and field sensitive fix point iteration algorithm based on modular heap abstraction in heap-manipulating programs. Experimental evaluation about a set of C benchmark programs shows that the proposed approach can be scalable to detect various clones that existing syntax-based clone detectors have missed.
Cited by 1
Stephen Magill, Stephen Magill, Stephen Brookes et al. · 2010
A number of questions regarding programs involving heap-based data structures can be phrased as questions about numeric properties of those structures. A data structure traversal might terminate if the length of some path is eventually zero or a function to remove n elements from a collection may only be safe if the collection has size at least n.
Cited by 0
Supratik Chakraborty · Co-Published with Indian Institute of Science (IISc), Bangalore, India eBooks · 2012
Cited by 4
Sun, Chenguang · Purdue · 2019
Modern Java application frameworks present significant challenges for existing static analysis algorithms. Such challenges include large-scale code bases, heap-carried dependency, and asynchronous control flow caused by message passing.Existing analysis algorithms are not suitable to deal with these challenges. One reason is that analyses are typically designed to operate homogeneously on the whole program. This leads to scalability problems when the analysis algorithms are used on applications built as plug-ins of large frameworks, since the framework code is analyzed together with the application code. Moreover, the asynchronous message passing of the actor model adopted by most modern frameworks leads to control flows which are not modeled by existing analyses.This thesis presents several techniques for more powerful debugging and program understanding tools based on slicing. In general, slicing-based techniques aim to discover interesting properties of a large program by only reasoning about the relevant part of the program (typically a small amount of code) precisely, abstracting away the behavior of the rest of the program.The key contribution of this thesis is a demand-driven framework to enable precise and scalable analyses on programs built on large frameworks. A slicing algorithm, which can handle heap-carried dependence, is used to identify the program elements relevant to an analysis query. We instantiated the framework to infer correlations between registration call sites and callback methods, and resolve asynchronous control flows caused by asynchronous message passing.
Cited by 0Open access
Braione, Pietro, Denaro, Giovanni, Guglielmo, Luca · arXiv (Cornell University) · 2024
Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally achieves path optimality against heap-manipulating programs. We formalize the POSE algorithm and experiment it against a benchmark of programs that take data structures as inputs, supporting the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs.
Cited by 0Open access
Alexey Gotsman · CL Technical Reports · 2021
Reasoning about concurrent programs is difficult because of the need to consider all possible interactions between concurrently executing threads. The problem is especially acute for programs that manipulate shared heap-allocated data structures, since heap-manipulation provides more ways for threads to interact. Modular reasoning techniques sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. In this dissertation we develop modular program logics and program analyses for the verification of concurrent heap-manipulating programs. Our approach is to exploit reasoning principles provided by program logics to construct modular program analyses and to use this process to obtain further insights into the logics. In particular, we build on concurrent separation logic—a Hoare-style logic that allows modular manual reasoning about concurrent programs written in a simple heap-manipulating programming language. Our first contribution is to show the soundness of concurrent separation logic without the conjunction rule and the restriction that resource invariants be precise, and to construct an analysis for concurrent heap-manipulating programs that exploits this modified reasoning principle to achieve modularity. The analysis can be used to automatically verify a number of safety properties, including memory safety, data-structure integrity, data-race freedom, the absence of memory leaks, and the absence of assertion violations. We show that we can view the analysis as generating proofs in our variant of the logic, which enables the use of its results in proof-carrying code or theorem proving systems. Reasoning principles expressed by program logics are most often formulated for only idealised programming constructs. Our second contribution is to develop logics and analyses for modular reasoning about features present in modern languages and libraries for concurrent programming: storable locks (i.e., locks dynamically created and destroyed in the heap), first-order procedures, and dynamically-created threads.
Cited by 4Open access
Zvonimir Rakamarić, Roberto Bruttomesso, Alan J. Hu et al. · Lecture notes in computer science · 2007
Cited by 24
Shengchao Qin, Guanhua He, Chenguang Luo et al. · Science of Computer Programming · 2013
Cited by 8
Chenguang Sun · Figshare · 2019
Modern Java application frameworks present significant challenges for existing static analysis algorithms. Such challenges include large-scale code bases, heap-carried dependency, and asynchronous control flow caused by message passing.Existing analysis algorithms are not suitable to deal with these challenges. One reason is that analyses are typically designed to operate homogeneously on the whole program. This leads to scalability problems when the analysis algorithms are used on applications built as plug-ins of large frameworks, since the framework code is analyzed together with the application code. Moreover, the asynchronous message passing of the actor model adopted by most modern frameworks leads to control flows which are not modeled by existing analyses.This thesis presents several techniques for more powerful debugging and program understanding tools based on slicing. In general, slicing-based techniques aim to discover interesting properties of a large program by only reasoning about the relevant part of the program (typically a small amount of code) precisely, abstracting away the behavior of the rest of the program.The key contribution of this thesis is a demand-driven framework to enable precise and scalable analyses on programs built on large frameworks. A slicing algorithm, which can handle heap-carried dependence, is used to identify the program elements relevant to an analysis query. We instantiated the framework to infer correlations between registration call sites and callback methods, and resolve asynchronous control flows caused by asynchronous message passing.
Cited by 0Open access
Braione, Pietro, Denaro, Giovanni, Guglielmo, Luca · arXiv (Cornell University) · 2024
Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally achieves path optimality against heap-manipulating programs. We formalize the POSE algorithm and experiment it against a benchmark of programs that take data structures as inputs, supporting the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs.
Cited by 0Open access
Longming Dong, Ji Wang, Chen Liqian et al. · 2012
Cited by 0