Skip to content

Soundness VS Completeness

Soundness: All its answers are correct.

Unsoundness: Some of the answers may incorrect.

Completeness: For each input, the algorithm can produce a result

Incompleteness: For some input, there is no answer from the algorithm

Combination of Soundness and Completeness

Sound + complete: correct answer for each input

Sound + incomplete: all answers are correct, but no answer for some inputs

Unsound + complete: For each input, there is a answer, but some answers may be incorrect

Intractability and Undecidability

Intractability

A problem for which no effect algorithm is known.

For example, 3SAT problem.

Undecidability

A problem for which no sound and complete algorithm can exist

For example, Turing halting problem

Workflow for Specification and Analysis

  1. Modelling: Specification for the problems at hand
  2. Encoding: Translate model to input
  3. Decision: Use general purpose technology, e.g., theorem prover, SAT solver...

The workflow is in the circle 1-2-3-1-2-3-...

Modelling

We have program counter pc, state variables.

Symbolic programs:

  1. Assertion: assert, condition that can not be violated. It is used to express safety.
  2. Non-determinism: nondet, consider every possible value allowed by data type. (Think about the wild cards in card games)
  3. Assumption: assume, discard any trace that violates assertion. It is used to control the non-determinism.

Safety and Liveness

Safety: Noting bad ever happens

Liveness: Something good eventually happens

Safe VS Unsafe

Error trace: execution that leads to a violated assertion.

Safe: a program that generates no error trace.

Unsafe: a program that can generates error trace.

Some examples:

int x=nondet(),y=nondet();
assume(x<0);
assume(y>0);
assert(x*y>0);// Unsafe! Because the assertion is always violated.

int x=0;
while(true){
    x=x+1;
}
assert(false);// Safe! Becuase this line will never be reached.

assume(0);// All the trace are deleted.
assert(0);// Safe! Since there is no trace, there can not be an error trace.

int x=nondet();
assume(x==1||x==0);
if(x==1){
    //...
}
else{
    assert(0);// Unsafe! Because there exist a error trace from x==0.
}

How to express safety?

  • Overflow check
  • Pointer check
  • Array bounds
  • Lock acquisition

Encoding

Program unfolding

For loop: we just expand the loop.

We sometimes need to bound the steps of program. To get feasible analysis results.

SAT

Propositional satisfiability

Propositional variable: \(x_1,x_2,\cdots\) (literals)

logical connectives \(\neg,\and,\or\).

Solvers: SAT solvers, SMT solvers, LP/ILP/MILP solvers...

Valid: \(\varphi=\) true, for every possible assignment

Satisfiable: \(\varphi=\) true, for at least one possible assignment

Falsifiable: \(\varphi=\) false, for at least one possible assignment

Unsatisfiable: \(\varphi=\) false, for every possible assignment

Equisatisfiability: \(\varphi'=\) true \(\Leftrightarrow\varphi''=\) true

SAT Solver

Simplify, decide, backtrack