← 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(βˆ€(A U B)) = Smallest T βŠ† S:


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.