Transcript PPT
CSE-321 Programming Languages Introduction to Logic in Computer Science 박성우 POSTECH June 11, 2013 Formal Verification Key Question in Software Development Is there an automated tool that locates errors in your software, or confirms the absence of errors in your software? – static analysis tool – formal verification tool 3 Market for Error-free Software • 2010 in the US: – software market: – cost of correcting errors: – cost of software errors: 310 billion dollars 20 billion dollars 60 billion dollars • "Product quality = Software quality" – in every arena: 4 Holy Grail in Software Development Software MRI / fMRI / PET 5 1st Generation - Testing • Methodology: 1. automatically generate test cases 2. run your software on each test case 3. analyze the result • Pros and cons: [+] relatively easy to implement [+] easy to comprehend test cases [-] low level of assurance • The most popular in industry 6 2nd Generation - Static Analysis [1/3] • Methodology: 1. analyze the source code of your software 2. approximate/emulate its run-time behavior 3. detect potential errors * image from http://ropas.snu.ac.kr/sparrow/wpaper.pdf 7 2nd Generation - Static Analysis [2/3] * image from http://ropas.snu.ac.kr/sparrow/wpaper.pdf 8 2nd Generation - Static Analysis [3/3] • Pros and cons: [+] easy to use • little user intervention [+] high level of assurance • If it says 'no bugs,' there are indeed no bugs. [+] can detect fatal bugs • buffer overrun, memory leak, double free, etc. [-] usually produces many false alarms • may not be so helpful to developers in practice. • Currently the most powerful technology 9 3rd Generation - Formal Verification [1/3] • Methodology: 1. write the specification for your software • Ex. "My software computes a solution to the equation ..." 2. formally prove that the source code meets the specification • automatically, using theorem provers • manually, using proof assistants • or using both 10 3rd Generation - Formal Verification [2/3] * image from http://frama-c.com/download/user-manual-Nitrogen-20111001.pdf 11 3rd Generation - Formal Verification [3/3] • Pros and cons [+] the highest level of assurance • A formal proof is produced. [+] can even prove the functional correctness • "The program correctly sorts a given array." [-] requires expertise in formal verification • MS degree at least! • The most advanced technology that is still evolving 12 Coq Programming in CSE-433 LICS Paper-and-Pencil Proof 14 Proof in Coq • Strings of matched parentheses Inductive T : Set := | eps : T | cons : E -> T -> T. Inductive mparen : T -> Prop := ... Inductive lparen : T -> Prop := ... Theorem mparen2lparen : forall s:T, mparen s -> lparen s. Proof. intros s H. induction H. apply Leps. rewrite <- concat_eps. auto using Leps, Lseq. auto using lparenConcat. Qed. 15 Coq Programming in LICS 2010 • Proof of the Pythagoras' theorem Theorem even_is_even_times_even: forall (n : nat), even (n * n) -> even n. Theorem main_thm: forall (n p : nat), n * n = double (p * p) -> p = 0. Definition irrational (x : R) : Prop := forall (p : Z) (q : nat), q <> 0 -> x <> (p / q)%R. Theorem irrational_sqrt_2: irrational (sqrt 2%nat). 16 Coq Programming in LICS 2010 • Proof of determinism of evaluations Theorem eval_deterministic : forall t t' t'', eval t t' -> eval t t'' -> t' = t''. • Proof of type safety in simply-typed lambda-calculus 17 Proof Theory in CSE-433 LICS 19 20 21 감사합니다 [email protected]