Program verification aims at proving that programs meet their specifications, i.e., that the actual program behaviour coincides with the desired one. Abstract interpretation is a method for designing and comparing semantics of programs, expressing varius types of programs properties. In particular, it has been successfully used to infer run-time program properties that can be valuable to optimize programs. Model checking is a specific approach to the verification of temporal properties of reactive and concurrent systems, which has proven successful in the area of finite-state programs.
展开▼
