On Improving Backwards Reasoning with Symbolic Execution: Integrating Loop Summarization, Alias Analysis, and Compositional Summarization

Program analysis techniques play a crucial role in modern software development by helping developers find bugs and verify code behavior. These techniques rely heavily on systematic reasoning about program execution paths. Symbolic execution has emerged as a powerful method for systematic program analysis. However, symbolic execution faces a fundamental challenge known as state-space explosion, where the number of potential execution paths grows exponentially. While backwards symbolic execution (BSE) offers some advantages over forward approaches in managing this explosion, it still struggles with path explosion when handling complex program elements such as loops, pointers, and function calls. This dissertation advances backwards reasoning through several key contributions. We introduce BROIL, an approach that enables handling of loops in backwards reasoning without requiring complete loop unrolling. By developing parameterized loop summaries that capture loop behavior, BROIL significantly reduces the state-space explosion problem common in symbolic execution. We demonstrate BROIL's effectiveness by applying it with incorrectness logic for targeted assertions. Our empirical evaluation then investigates the question of which alias analysis technique best complements BSE. Through experimentation comparing different alias analysis approaches, we demonstrate that demand-driven analysis substantially outperforms whole-program approaches, achieving a 7.29× geometric mean speedup in symbolic execution. Finally, we develop CAMS, a compositional approach for function summarization in backwards analysis. CAMS introduces context-agnostic function summaries that capture pointer and global variable effects while supporting modular composition. By enabling the reuse of summaries across different program units, CAMS achieves significant performance improvements compared to non-compositional approach.

Name thesis:degree_name

Doctor of Philosophy

Level thesis:degree_level

doctoral

Discipline thesis:degree_discipline

Computer Engineering

Department dc:contributor.department

Electrical and Computer Engineering

Grantor dc:publisher

Virginia Tech

Year dc:date.issued

2025

Author dc:creator

• Sefat, Md Syadus

Chair dc:contributor.committeechair

• Ravindran, Binoy

Committee members dc:contributor.committeemember

• Butt, Ali R.
• Verbeek, Freek
• Plassmann, Paul E.
• Hsiao, Michael S.

• Incorrectness Logic
• Backwards Symbolic Execution
• Loop Summarization
• Compositional Summarization
• Alias Analysis
• State-space Explosion

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Language dc:language.iso

en

Dc Identifier Other

vt_gsexam:42511

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/124700