author = {Wolfgang Schreiner},
title = {{Computer-Assisted Proving for the Analysis of Systems and Specifications }},
language = {english},
abstract = {Nowadays the formal methods landscape is dominated by model checking, an approach to the verification of programs/systems that is fully automatic but limited in its scope, in particular with respect to verifiable properties. In this talk, we discuss the alternative and more general direction of computer-assisted interactive proving which in the last decade (due to the development of automatic "Satisfiability Modulo Theories" solvers as supporting components) has made tremendous progress; consequently practical formal reasoning on more general system models and system properties has become viable. Furthermore, while not fully automatic and depending on human assistance, this approach has the potential of increasing a programmer's understanding (why is a system correct or what are the fundamental reasons of its failure) much more than the plain yes/no answers and counterexample executions produced by fully automatic model checkers. As an example of this direction, we present the "RISC ProofNavigator", an interactive proving assistant developed for education in reasoning about programs and specifications. Finally, we argue why modern computer science curricula should teach the use of proving assistants for formal specification and verification as an integral part of developing correct software. },
year = {2009},
month = {March 17},
note = {Invited colloquium talk at Seminar "Advanced topics in Distributed and Component-based Systems", Distributed Systems Research Group, Charles University, Prague},
institution = {Seminar "Advanced topics in Distributed and Component-based Systems", Distributed Systems Research Group, Charles University, Prague}