Symbolic execution builds predicates that characterize the conditions under which execution paths can be taken and the effect of the execution on program state. Extracting predicates through symbolic execution is the essential bridge from the complexity of program behavior to the simpler and more orderly world of logic. This chapter presents the symbolic execution and proof of properties. | Symbolic Execution and Proof of Properties (c) 2007 Mauro Pezzè & Michal Young Ch 7, slide 1 Learning objectives • Understand the goal and implication of symbolically executing programs • Learn how to use assertions to summarize infinite executions • Learn how to reason about program correctness • Learn how to use symbolic execution to reason about program properties • Understand limits and problems of syombilc execution (c) 2007 Mauro Pezzè & Michal Young Ch 7, slide 2 Symbolic Execution • Builds predicates that characterize – Conditions for executing paths – Effects of the execution on program state • Bridges program behavior to logic • Finds important applications in – program analysis – test data generation – formal verification (proofs) of program correctness (c) 2007 Mauro Pezzè & Michal Young Ch 7, slide 3 Formal proof of properties • Relevant application domains: – Rigorous proofs of properties of critical subsystems • Example: safety kernel of a medical device – Formal verification of critical properties particularly resistant to dynamic testing • Example: security properties – Formal verification of algorithm descriptions and logical designs • less complex than implementations (c) 2007 Mauro Pezzè & Michal Young Ch 7, slide 4 Symbolic state Values are expressions over symbols Executing statements computes new expressions Execution with concrete values before low high mid 12 15 - mid = (high+low)/2 after low high mid Execution with symbolic values before low high mid L H - mid = (high+low)/2 after 12 15 13 (c) 2007 Mauro Pezzè & Michal Young Low high mid L H (L+H)/2 Ch 7, slide .
