25 - Symbolic Checking
Symbolic Checking is a technique of checking for program correctness, i.e. proving/verifying, by using symbolic inputs to represent set of states and transitions instead of enumerating individual states/transitions separately Symbolic checking
- Model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness)
- In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a structure satisfies a given logical formula.
- A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure
- Instead of enumerating reachable states one at a time, the state space can sometimes be traversed more efficiently by considering large numbers of states at a single step. When such state space traversal is based on representations of a set of states and transition relations as logical formulas, binary decision diagrams (BDD) or other related data structures, the model-checking method is symbolic.
- Model-checking tools face a combinatorial blow up of the state-space, commonly known as the state explosion problem, that must be addressed to solve most real-world problems
- Symbolic algorithms avoid explicitly constructing the graph for the finite state machines (FSM); instead, they represent the graph implicitly using a formula in quantified propositional logic
- Symbolic Inputs
- Set of States/Transitions
- Models & Properties
- Language & Logic
- E.g.: Manticore, Mythril