关键词：程序验证；算法设计；属性指示可达性
摘 要：In this dissertation, we explore the potential of using PDR for program verification and - as product of this endeavor - present a sound and complete algorithm for intraprocedural verification of programs with static memory allocation that is based on Property Directed Reachability.