[2-26]Verifiers are Programs

Date:2008-02-25

Title: Verifiers are Programs
Speaker: Dr. Chen Yifeng
             Dept. of Computer Science, University of Durham, UK
Time: 3:30pm, Tuesday Feb. 26, 2008
Venue: Lecture room, Lab. of Computer Science, ISCAS

Abstract:

This talk will report our recent results on the relation between execution and verification. A simple imperative language with execution and verification commands is introduced. A machine only executes execution commands of a program, while the compiler only performs the verification commands. Common commands in other languages can be defined as a combination of execution and verification commands. Design of verifiers then becomes program design using  verification commands. It is shown  that type checking, abstract interpretation, modeling checking and Hoare Logic are all special verification programs, so are many of their combinations.