Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Compositional satisfiability solving in separation logic ⋮ StarFinder

Uses Software

• Java PathFinder
• TACO
• HIP
• GitHub
• JaCoCo
• JBSE

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