An Evidential Tool Bus

Abstract. Theorem provers, model checkers, static analyzers, test generators. . . all of these and many other kinds of formal methods tools can contribute to the analysis and development of computer systems and software. It is already quite common to use several kinds of tools in a loose combination: for example, we might use static analysis and then model checking to help find and eliminate design flaws prior to undertaking formal verification with a theorem prover. And some modern tools, such as test generators, are built using model checkers, predicate abstractors, decision procedures and constraint solvers as components in tight combination. But we can foresee a different kind of combination where many tools and methods are used in ad hoc combination within a single analysis. For example, static analysis might yield invariants that enable decision es to build a predicate abstraction whose reachable states are calculated as a BDD and then concretized to yield a strong invariant ...

• Type: Conference
• Year: 2005
• Where: ICFEM
• Authors: John M. Rushby
• Keywords: ICFEM 2005, Model Checkers, Test Generators, Theorem Prover