title=Path-optimal symbolic execution of heap-manipulating programs
authors=Pietro Braione; Giovanni Denaro; Luca Guglielmo
arxiv_id=2407.16827v2
arxiv_submitted=2024-07-23
arxiv_v2=2026-01-14
arxiv_url=https://arxiv.org/abs/2407.16827
paper_pdf_sha256=5a4137d0b06ad021ef08c653ee43339d158b44d197093f7766f626aa4ca3c9a7
paper_pages=18
venue=SANER 2026 Research Track
venue_url=https://conf.researchr.org/details/saner-2026/saner-2026-papers/7/Path-Optimal-Symbolic-Execution-of-Heap-Manipulating-Programs
venue_talk=2026-03-20
artifact_repository=https://github.com/pietrobraione/jpose
artifact_head=427c19bbbce12021fda958e7d88650be2417920e
paper_principle=encode relevant heap alias and distinctness assumptions in if-then-else expressions and fork only at actual program decisions
paper_implementation=Java bytecode symbolic executor based mostly on JBSE and using Z3
paper_benchmark=69 SBST Java classes and 816 methods before filtering; 55 classes and 692 methods in Table I
paper_bounds=80 nested calls; 150 loop iterations; 6 hours per method; 10 hours per class for test generation
paper_query_time_test=paired Wilcoxon p-value 0.0014
klee_title=KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
klee_url=https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar_html/index.html
adaptation=F405 applies the defer-alias-choice principle only to already allocated bounded C heap bases and lifetime markers
not_equivalent=No initial symbolic heap materialization, fresh-object creation, Java field refinement, inheritance, polymorphism, or full POSE artifact reproduction
evidence_boundary=Local finite-domain semantics and mechanism cost only; no public-target coverage, solver-throughput, bug-yield, or end-to-end speedup claim