### ← Home

# Computer Aided Formal Verification

## Contents

Bring the formalism. Formality is key ππ

It's in the name, this is **formal** verification, not computer-aided
casual-maybe-on-the-weekend verification.

## Transition System

Transition System is a 5 tuple: < S, ==>, I, AP, L >.

Only consider non-blocking TS's.

Deterministic iff |I| = 1 And βs.|Post(s)| = 1

Initial-Path-Fragment - starts state in I.

## Linear Temporal Logic

Traces are in (2^AP^Ο)

TS implies P means: traces(TS) β traces(P)

TS is a refinemet of TS' if traces(TS) β traces(TS')

traces(TS) β traces(TS') <====> TS' impies P ===> TS impies P

### Invariants

P is an invariant if it has an invariant condition ΙΈ st:

P = {A0A1A2...β 2^AP^Ο | βj>=0 Aj implies ΙΈ}

There is some invariant condition such that P can be expressed as a list of infinite words where each state implies the invariant.

### Safety Properties

Nothing bad happens.

βs β (2^AP^Ο) \ P, βs'< s st

P β© {t β (2^AP^Ο) | t < s' } = ΙΈ

There exists a finite prefixes of bad words

## CTL*

LTL is all path formulae - All **PATHS** from the given state.

CTL is all state formulae- For the given state we examine either:

all it's paths,

a single path,

what properties hold now,

etc etc.

Sat(β(A U B)) = Smallest T β S:

- Sat(B) β T
- s β Sat(A) and Post(s) intersects T ===THEN===> s β T

Sat(β(A U B)) = Smallest T β S:

- Sat(B) β T
- s β Sat(A) and Post(s) β T ===THEN===> s β T

## GNBA

(Q, Sigma, delta, Q0, F) - 5 tuple

d: Q x Sigma ---> 2^Q

Input to a GNBA is an infinite word.

Accepts if all f in F come up infinitely often in the infinite word.

If F is the empty set, all states are considered accepting, so the language of G is all words with an infinite run in G.

## Witnesses and Counterexamples

A witness for a "β" is a sufficiently long prefix of a path pi st pi impies what we are seeking to find exists... #deep.

## Reduced Order Binary Decision Diagrams

A tree

Two leaves 0 and 1.

one type of internal node: x -> t1, t0

t1 and t0 successor nodes or one of the two leaves.

Reduced - No two distinct nodes have the same variable, high and low successors.

Ordered - There exists a variable ordering such that any path through the tree follows this given variable order.

Canonicity lemma - For all boolean expressions t there is some ROBDD.

NP-Hard if a given variable ordering is optimal.

Encoding of jazz.