中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 01 Theorem Proving

Theorem Proving CS294-8 Lecture 9 Prof.Necula CS 294-8 Lecture 9 1

Prof. Necula CS 294-8 Lecture 9 1 Theorem Proving CS 294-8 Lecture 9

Theorem Proving:Historical Perspective Theorem proving (or automated deduction) logical deduction performed by machine At the intersection of several areas Mathematics:original motivation and techniques Logic:the framework and the meta-reasoning techniques One of the most advanced and technically deep fields of computer science Some results as much as 75 years old Automation efforts are about 40 years old Prof.Necula CS 294-8 Lecture 9 2

Prof. Necula CS 294-8 Lecture 9 2 Theorem Proving: Historical Perspective • Theorem proving (or automated deduction) = logical deduction performed by machine • At the intersection of several areas – Mathematics: original motivation and techniques – Logic: the framework and the meta-reasoning techniques • One of the most advanced and technically deep fields of computer science – Some results as much as 75 years old – Automation efforts are about 40 years old

Applications Software/hardware productivity tools Hardware and software verification (or debugging) Security protocol checking Automatic program synthesis from specifications Discovery of proofs of conjectures A conjecture of Tarski was proved by machine(1996) There are effective geometry theorem provers Prof.Necula CS 294-8 Lecture 9 3

Prof. Necula CS 294-8 Lecture 9 3 Applications • Software/hardware productivity tools – Hardware and software verification (or debugging) – Security protocol checking • Automatic program synthesis from specifications • Discovery of proofs of conjectures – A conjecture of Tarski was proved by machine (1996) – There are effective geometry theorem provers

Program Verification o Fact:mechanical verification of software would improve software productivity,reliability,efficiency Fact:such systems are still in experimental stage After 40 years! Research has revealed formidable obstacles Many believe that program verification is dead Prof.Necula CS 294-8 Lecture 9 4

Prof. Necula CS 294-8 Lecture 9 4 Program Verification • Fact: mechanical verification of software would improve software productivity, reliability, efficiency • Fact: such systems are still in experimental stage – After 40 years ! – Research has revealed formidable obstacles – Many believe that program verification is dead

Program Verification ·yth: "Think of the peace of mind you will have when the verifier finally says "Verified",and you can relax in the mathematical certainty that no more errors exist" ·Answer: Use instead to find bugs (like more powerful type checkers) We should change "verified"to "Sorry,I can't find more bugs" Prof.Necula CS 294-8 Lecture 9 5

Prof. Necula CS 294-8 Lecture 9 5 Program Verification • Myth: – “Think of the peace of mind you will have when the verifier finally says “Verified”, and you can relax in the mathematical certainty that no more errors exist” • Answer: – Use instead to find bugs (like more powerful type checkers) – We should change “verified” to “Sorry, I can’t find more bugs

Program Verification 。Fact: Many logical theories are undecidable or decidable by super- exponential algorithms There are theorems with super-exponential proofs ·Answer: Such limits apply to human proof discovery as well If the smallest correctness argument of program P is huge then how did the programmer find it? Theorems arising in PV are usually shallow but tedious Prof.Necula CS 294-8 Lecture 9 6

Prof. Necula CS 294-8 Lecture 9 6 Program Verification • Fact: – Many logical theories are undecidable or decidable by super￾exponential algorithms – There are theorems with super-exponential proofs • Answer: – Such limits apply to human proof discovery as well – If the smallest correctness argument of program P is huge then how did the programmer find it? – Theorems arising in PV are usually shallow but tedious

Program Verification Opinion: Mathematicians do not use formal methods to develop proofs Why then should we try to verify programs formally ·Answer: In programming,we are often lacking an effective formal framework for describing and checking results Compare the statements The area bounded by y=0,x=1 and y=x2 is 1/3 By splicing two circular lists we obtain another circular list with the union of the elements Prof.Necula CS 294-8 Lecture 9 7

Prof. Necula CS 294-8 Lecture 9 7 Program Verification • Opinion: – Mathematicians do not use formal methods to develop proofs – Why then should we try to verify programs formally ? • Answer: – In programming, we are often lacking an effective formal framework for describing and checking results – Compare the statements • The area bounded by y=0, x=1 and y=x2 is 1/3 • By splicing two circular lists we obtain another circular list with the union of the elements

Program Verification 。Fact: Verification is done with respect to a specification Is the specification simpler than the program What if the specification is not right ·Answe: Developing specifications is hard Still redundancy exposes many bugs as inconsistencies We are interested in partial specifications An index is within bounds,a lock is released Prof.Necula CS 294-8 Lecture 9 8

Prof. Necula CS 294-8 Lecture 9 8 Program Verification • Fact: – Verification is done with respect to a specification – Is the specification simpler than the program ? – What if the specification is not right ? • Answer: – Developing specifications is hard – Still redundancy exposes many bugs as inconsistencies – We are interested in partial specifications • An index is within bounds, a lock is released

Theorem Proving and Software Program Semantics Meets spec/Found Bug Specification Validity VC generation Provability (theorem proving) Theorem in a logic ·Soundness: If the theorem is valid then the program meets specification If the theorem is provable then it is valid Prof.Necula CS 294-8 Lecture 9 9

Prof. Necula CS 294-8 Lecture 9 9 Theorem Proving and Software Meets spec/Found Bug Theorem in a logic Program Specification Semantics VC generation Validity Provability (theorem proving) • Soundness: – If the theorem is valid then the program meets specification – If the theorem is provable then it is valid

Theorem Proving Program Analysis Start from real code and face head-on issues like: aliasing and side-effects ·looping data types and recursion ·exceptions Most often used for sequential programs Ambitious: Modest: -Complex properties Simple properties Flow sensitive Flow insensitive -Inter-procedural -Intra-procedural Semi-automatic Automatic Requires invariants and Discovers simple invariants validates them

Theorem Proving Program Analysis Start from real code and face head-on issues like: • aliasing and side-effects • looping • data types and recursion • exceptions Most often used for sequential programs Ambitious: – Complex properties – Flow sensitive – Inter-procedural Modest: – Simple properties – Flow insensitive – Intra-procedural Semi-automatic Automatic Requires invariants and validates them Discovers simple invariants