Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation
From MaRDI portal
Publication:3297594
DOI10.1007/978-3-030-31784-3_12zbMath1437.68044arXiv1712.06025OpenAlexW2967523636MaRDI QIDQ3297594
Quang Loc Le, Jun Sun, Quoc-Sang Phan, Shengchao Qin, Long H. Pham
Publication date: 20 July 2020
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1712.06025
Logic in computer science (03B70) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Frame inference for inductive entailment proofs in separation logic
- Exact Heap Summaries for Symbolic Execution
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Symbolic execution and program testing
- Satisfiability Modulo Heap-Based Programs
- BI as an assertion language for mutable data structures
- Compositional Shape Analysis by Means of Bi-Abduction
- Programming Languages and Systems
This page was built for publication: Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation