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