Salsa: Beyond Model Checking

摘要

The Verification Problem: Given the following: * A system description * A set of environmental assumptions * A set of required properties (one-state or two-state) -- Verification is the process of: * Extracting models from the system description. Sufficient to establish the properties of interest. * Applying a verification tool to the model to verify/refute properties. Very likely that a property is not provable (or wrong).