The Verification method with proof scores is an interactive
theorem proving method based on algebraic specifications. We
have been developing verifications with proof scores in
CafeOBJ algebraic specification language for more than ten
years. This talk explains theoretical foundations of
verification with proof scores using simple and insightful
examples. The focuses of the talk are (1) Model based
verification, (2) Quasi-complete proof rules, (3) Analyses of
relations between specifications and proofs.
|