TAILIEUCHUNG - Lecture Software testing and analysis - Chapter 7: Symbolic execution and proof of properties

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 Pezze Michal Young Ch 7 slide 1 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 Pezze Michal Young Ch 7 slide 4 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 Pezze Michal Young Ch 7 slide 3 Symbolic state Values are expressions over symbols Executing statements computes new expressions Execution with concrete values Execution with symbolic values before low 12 high 15 mid before low L high H mid mid high low 2 mid high low 2 after low 12 high 15 mid 13 SOFTWARE TESTING ANO-ANALYSIS after Low L high H mid L HJ 2 2007 Mauro Pezze Michal Young Ch 7 slide 5 Dealing with branching statements a sample program char binarySearch char key char dictKeys char dictValues int dictsize int high dictsize - 1 int mid int comparison Branching stmt while high low ----------- mid high low 2 comparison strcmp dictKeys mid if comparison 0 low mid 1 else if comparison 0 high mid - 1 else return dictValues mid key return 0 c 2007 Mauro Pezze Michal Young Ch 7 slide 6 Summary information Symbolic representation of paths may become extremely complex We can simplify the representation by replacing a complex condition p with a weaker condition w such that p w w describes the path with less precision w is a summary of p c 2007 Mauro Pezze Michal Young Ch 7 slide 8 Executing while high low Add an expression that records the condition for the execution of .

• Kỹ thuật lập trình
• Software testing
• Software analysis
• Software testing and analysis
• Software product
• Software processes
• Symbolic execution
• Software process
• Testing object oriented software
• Component based software testing
• Lecture Software testing and quality assurance
• Lecture Software testing
• Quality assurance
• Web Base application testing
• Performance testing
• Coverage testing
• Functional testing
• Combinatorial testing
• Structural testing
• Data flow testing
• Model based testing
• Fault based testing
• System testing
• A testing workbench
• Kiểm thử beta
• Software qualities
• Software reliability engineering testing
• Assessing program qualities
• Phân hoạch tương đương
• Software Engineering
• Defect testing
• Testing process goals
• Assertion based Testing
• Model of program testing
• Quality process
• A Software Testing Primer
• Software Testing Primer
• Concepts of testing
• Non functional testing
• Test planning