Automatic Testing-Based Formal Verification: Bridging Testing and Formal Verification for Program Correctness
Title: Automatic Testing-Based Formal Verification: Bridging Testing and Formal Verification for Program Correctness
Speaker: Shaoying Liu ( http://cis.k.hosei.ac.jp/~sliu/ )
Time: 10:00am, Sept.11, 2013
Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
Formal verification for programs based on Floyd-Hoare logic aims to establish the correctness of the program for all of the specified inputs, but face various challenges and is almost impossible for full automation in general. Testing of programs to detect errors in the program is likely to be fully automated, but unlikely to establish the correctness of the program. To achieve an automatic formal verification technique for programs, an effective integration of the above two techniques may provide a practical solution. In this talk, I will present a novel technique that utilizes Floyd-Hoare logic to strengthen the effectiveness of a specification-based testing approach in error detection. This new technique can be fully automated in the sense that a software tool can be constructed to support the entire process of the formal verification. An example is used to explain the process of applying the new technique. Further challenges to this technique are also discussed, which is expected to inspire more researches on this topic in the future.
Formal verification for programs based on Floyd-Hoare logic aims to establish the correctness of the program for all of the specified inputs, but face various challenges and is almost impossible for full automation in general. Testing of programs to detect errors in the program is likely to be fully automated, but unlikely to establish the correctness of the program. To achieve an automatic formal verification technique for programs, an effective integration of the above two techniques may provide a practical solution. In this talk, I will present a novel technique that utilizes Floyd-Hoare logic to strengthen the effectiveness of a specification-based testing approach in error detection. This new technique can be fully automated in the sense that a software tool can be constructed to support the entire process of the formal verification. An example is used to explain the process of applying the new technique. Further challenges to this technique are also discussed, which is expected to inspire more researches on this topic in the future.