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 superexponential 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