You are currently browsing the category archive for the ‘Model Checking’ category.

**Automated theorem proving** (**ATP**) or **automated deduction**, currently the most well-developed subfield of *automated reasoning* (AR), is the proving of mathematical theorems by a computer program.

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but NP-complete, and hence only exponential-time algorithms are believed to exist for general proof tasks. For a first order predicate calculus, with no (“proper”) axioms, Gödel’s completeness theorem states that the theorems (provable statements) are exactly the logically valid well-formed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.

However, *invalid* formulas (those that are *not* entailed by a given theory), cannot always be recognized.

A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.

### Some techniques for theorem proving

- First-order resolution with unification
- Lean theorem proving
- Model elimination
- Method of analytic tableaux
- Superposition and term rewriting
- Model checking
- Mathematical induction
- Binary decision diagrams
- DPLL
- Higher-order unification

————————————

## Further reading

## How to make it as easily as possible?

A **lean theorem prover** is an automated theorem prover implemented in a minimum amount of code. Lean provers are generally^{[citation needed]} implemented in Prolog, and make proficient use of the backtracking engine and logic variables of that language. Lean provers can be as small as a few hundred bytes of source code.

The following is a small Prolog implementation:

propexp=

not_(propexp);

or_(propexp,propexp);

and_(propexp,propexp);

implies_(propexp,propexp);

s_(symbol); a ; b ; c.

**The beef is that this procedural definition for a theorem can be converted into an atomistic model so that each domain will be transformed into a symbolic element. **

**Therefore**, proving the theorem means running the top element of the theorem. The principle is exactly the same as in source code simulation (see SimulationWare).

When those variable a, b and c will be captured from the original code, this work will enable proving source code sequences written in Java or similar languages.

### Some links:

A **binary decision diagram** (**BDD**) or **branching program**, like a negation normal form (NNF) or a propositional directed acyclic graph (PDAG), is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Unlike other compressed representations, operations are performed directly on the compressed representation, i.e. without decompression.

A Boolean function can be represented as a rooted, directed, acyclic graph, which consists of decision nodes and two terminal nodes called 0-terminal and 1-terminal. Each decision node is labeled by a Boolean variable and has two child nodes called low child and high child. The edge from a node to a low (high) child represents an assignment of the variable to 0 (1). Such a **BDD** is called ‘ordered’ if different variables appear in the same order on all paths from the root. A BDD is said to be ‘reduced’ if the following two rules have been applied to its graph:

- Merge any isomorphic subgraphs.
- Eliminate any node whose two children are isomorphic.

In popular usage, the term **BDD** almost always refers to **Reduced Ordered Binary Decision Diagram** (**ROBDD** in the literature, used when the ordering and reduction aspects need to be emphasized). The advantage of an ROBDD is that it is canonical (unique) for a particular functionality.^{[citation needed]} This property makes it useful in functional equivalence checking and other operations like functional technology mapping.

Below an example for a function** f **with three variables:

BDDs are useful for modeling software logic. By using them it is possible to evaluate test coverage and to generate tests for the program, bottom-up.

### Symbolic Analysis and BDDs

For the reductionist implementation for Symbolic Analysis, there is only one global method for AHOs. It is the * run*-method intended for simulating each AHO atom.

It is rather easy to write another method to generate all possible paths for each AHO, because all branches happen in a path Clause (see book Symbolic Analysis). Lets our new method be * bdd*. We have a program P with the contents X1 • X2 • X3. After making an atomistic model, we have a model M, where the start element M0 is a model element with the contents meta(set([X1, X2, X3])). When we call M:bdd, then it call successively X1:bdd, X2:bdd and X3:bdd. Each of them returns a subtree as the

*formalism. In the main level the whole tree will be collected.*

**clause**Summary: *BDD can be seen as a small easy subset of simulation*. BDD can be either static or partially dynamic, using method invokations as far as possible.

Some links:

- BDDs at Wiki: http://en.wikipedia.org/wiki/Binary_decision_diagram

The **SLAM project**, which was started by Microsoft Research, aimed at verifying some software safety properties using model checking techniques. It is implemented in Ocaml, and has been used to find many bugs in Windows Device Drivers. It is distributed as part of the Microsoft Windows Driver Foundation development kit as the Static Driver Verifier (SDV).

**SLAM uses a technique called counterexample-guided abstraction refinement**, which uses progressively better models of the program under test.

“SLAM originally was an acronym but we found it too cumbersome to explain. We now prefer to think of ‘slamming’ the bugs in a program.” It probably stood for “Software, Languages, Analysis, and Modeling.” Note that Microsoft has since re-used SLAM to stand for “Social Location Annotation Mobile”

### About Abstraction Methods:

There are three ways to abstract programs.

- Over-abstract like abstract interpretation
- Under-abstraction like SLAM, also called meat-axe – abstraction, which cuts of some information
- Precise abstraction which is the best description for Symbolic Analysis (Laitila), which uses the Symbolic language for that.

Because SLAM removes some information, it is not complete to describe program comprehension features of the program, which include: control flow, data flow, state flow, operations and full functionality (Pennington, Wiedenbeck, von Mayrhauser et al.).

Paper X describes counterexample-guided abstraction refinement with some methods:

There is a traffic light example in it to model states.

Some algorithms in the paper are SPLITPath, PolyRefine and SPLITLoop.

### Precice abstraction in Symbolic Analysis

We define precise abstraction as a formula M <– –> M’, where M is the original model (or code) containing Java, C++ or other language and M’ is the abstracted model with AHO objects, where the command from each AHO has been transformed according to the original grammar term of the corresponding program element. The abstracted model can be transformed back into the original language. Thus, the model is reversible.

### Some links:

- SLAM at Wiki: http://en.wikipedia.org/wiki/SLAM_project
- SLAM: http://research.microsoft.com/en-us/projects/slam/
- Counterexample-guided Abstraction Refinement: http://www.aladdin.cs.cmu.edu/papers/pdfs/y2000/counterex.pdf
- A reversible reaction (and model): http://en.wikipedia.org/wiki/Reversible_reaction

### Symbolic Analysis Laboratory (SAL)

SAL is a project established by Berkeley and Standford Universities used for automated formal methods.

Motivation for SAL is the following (the link):

To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification.

SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems.

SAL defines symbolis analysis as follows:

Symbolic analysis is simply the computation of fixed point properties of programs through a combination of deductive and explorative techniques.

- Automated deduction, in computing property preserving abstractio9ns and propagating the consequences of known properties.
- Model checking, as a means of computing global properties of by means od systematic symbolic exploration. For this purpose, model checking is used for actually computing fixed points such as the reachable state set, in addition to verifying given temporal properties.
- Invariant generation, as a technique for computing useful properties and propagating known properties.
- SAL 3.0 is the current the tool suite for SAL SAL tutorial can be downloaded from here: http://sal.csl.sri.com/doc/salenv_tutorial.pdf

### Principles of SAL 3.0

The “motor” of SAL is its language.

The SAL language is not that different from the input languages used by various other verification tools such as SMV, Murphi, Mocha, and SPIN. Like these languages, SAL describes transition systems in terms of initialization and transition commands. These can be given by variable-wise definitions in the style of SMV or as guarded commands in the style of Murphi.

A complete description of the SAL language is available online at http://sal.csl.sri.com/.

short: CONTEXT = 1 BEGIN State: TYPE = {ready, busy}; main: MODULE = BEGIN INPUT request : BOOLEAN OUTPUT state : State INITIALIZATION state = ready TRANSITION state’ IN IF (state = ready) AND request THEN {busy} ELSE {ready, busy} ENDIF END; END

*sal > (start-simulation! “main”)*

*Some observations considering reverse engineering and program comprehension (Laitila’s approach):*- SALenv contains a symbolic model checker called sal-smc. It allows users to specify properties in linear temporal logic (LTL), and computation tree logic (CTL). One typical command for sal-smc is:
**THEOREM main |- AG(request => AF(state = busy));** - Some other featrures are Peterson protocol, Bakery protocol and Syncronous bus arbiter etc.
**Some examples.**

*Some comments: *

- That kind of language specific approach leads to a procedural paradigm via a program which indirectly describes the model. In that approach the model to be verified is data, which tries to model the code.
- The implementation language SAL 3.0 is very far from the programming languages.
**Therefore, SAL is not useful for reverse engineering or for program comprehension.**

### Some links:

- Symbolic Analysis Laboratory, home: http://sal.csl.sri.com/
- Examples for SAL: http://sal.csl.sri.com/examples.shtml

A **Kripke structure** is a type of nondeterministic finite state machine used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.

Let *A**P* be a set of *atomic propositions*, i.e. boolean expressions over variables, constants and predicate symbols.

A Kripke structure is a 4-tuple consisting of

- a finite set of states
- a set of initial states
- a transition relation where such that
- a labeling (or
*interpretation*) function

Since *R* is left-total, it is always possible to construct an infinite path through the Kripke structure. Thus a deadlock state has a single outgoing edge back to itself.

The labeling function *L* defines for each state *s* ∈ *S* the set *L*(*s*) of all atomic propositions that are valid in *s*. In the Kripke structure, the transition function should be complete,i.e each and every state should have transition.In other words there should not be any dead states in the graph.

### Combining the Semantics of the Atomistic Model and the Kripke Structure with each other

If we use the notation of the Kripke structure for the Atomistic Model we get the definitions:

The atomistic model is a Kripke structure, a 4-tuple consisting of

- a finite set of states implemented as symbols in the model illustrating clauses of the original clause and side effects caused by the simulation/evaluation processes.
- a set of initial states implemented as symbols of the models: either clauses or side effects.
- a transition relation where such that implemented as links of the symbols.
- a labeling (or
*interpretation*) function implemented as a command-fact in each symbol.

### Summary about the correspondece

**The atomistic model is downwards compatible with the Kripke structure. It leads to a conculsion (by inspection) that all functions and mathematical processes intended for the Kripke structure, e.g. model checking, can be borrowed for the use of the atomistic model.** Only a simple transformation is needed.