Software Verification and Validation (VIMMD052)

Software model checking with

abstraction-based methods

Ákos Hajdu,
István Majzik

Budapest University of Technology and Economics

Dept. of Artificial Intelligence and Systems Engineering

Budapest University of Technology and Economics

Dept. of Artificial Intelligence and Systems Engineering 1
Where are we now in the development process?
Requirement
analysis

System
specification

Architecture
design

Component
design

Component
implementation • Source code verification by static analysis
• Proof of program correctness by theorem proving
System • Software model checking with abstraction-based methods
integration

System
delivery

Operation,
maintenance

2
Introduction

3
 Introduction: Model Checking
 This lecture: focus on software and abstraction
Control Flow Assertions
Automata
Program
source code
Formal Formalized
model property
Abstraction
Model checking + CEGAR
algorithm

Ok Counterexample
Violating
execution

6
 Introduction: Model and property
 Formal model: Control-Flow Automaton
o Set of control locations
o Set of edges with operations
over a set of variables
• E.g., guard, assignment …

x : int
0: x = 0
1: while (x < 5) {
2: x = x + 1
}
3: assert (x <= 5)

 Checked property: “error” location (violation of the assertion)

should not be reachable

7
 Introduction: CFA states and transitions
 State: CFA location + valuation of variables (L, x1, x2, …, xn)
 Transition: operations
 Problem: state space explosion caused by data variables
o E.g., 10 locations and 2 integers: 10·232·232 possible states
 Goal: reduce the state space representation by abstraction

8
 Counterexample-Guided
Abstraction Refinement (CEGAR)

9
 CEGAR introduction: abstract states
Transition Abstract state
State

Error state
Concrete state space Abstraction Abstract state space
Over-approximation

Refined state space Spurious counterexample Abstract counterexample

Property holds
OK Counterexample

Model, Abstraction Abstract counterex

Check Concretize Concrete
property
Init Refine
10
 Recap: Mathematical logic
 Propositional logic (PL) ¬𝑝 ∧ (𝑝 ∨ 𝑞)
o Boolean variables and operators
o SAT problem: Is the formula satisfiable?
• (SAT solvers are used also in bounded model checking)
o Expressive power sometimes not enough
 First order logic (FOL) ∀𝑥, 𝑦 ∃𝑧: 𝑝(𝑓 𝑥, 𝑦 , 𝑔 𝑧 )

o Functions, predicates, quantifiers

o Satisfiability is not decidable in general
 Satisfiability Modulo Theories (SMT) (𝑥 ≤ 𝑦 + 1) ∧ (𝑦 ≥ 3)

o “Restricted” FOL formulas

o Only interpreted symbols, e.g., integer arithmetic
o Satisfiability can be decided
11
 Abstraction: Introduction
 Abstraction
o General mathematical concept
o Goal: Hide details
o Get an easier problem to solve
 Examples of abstraction
o Location abstraction:
Only locations considered
𝑙, 𝑥1 , 𝑥2 , … , 𝑥𝑛 → 𝑙
• Usually not precise enough:
Easy to find trivial
counterexamples
o Predicate abstraction:
CFA Abstract state space
Locations with predicates

12
 Predicate abstraction: Initial attempt
 Predicate abstraction
o Keep track of predicates instead of concrete values for variables
o Abstract state: formed by the concrete states that correspond
to the same location and satisfy the same predicates
 Performing abstraction: Initial attempt
o Enumerate and join concrete states
o 3x3 concrete states in the example  5 abstract states
o Enumeration and then joining is not efficient 
Example: Variables and predicates 𝑦\x 0 1 2

Variables: 0 (𝑥 = 𝑦) (none) (none)

𝑥, 𝑦; 𝐷𝑥 = 𝐷𝑦 = 0,1,2 1 (𝑥 < 𝑦) (𝑥 = 𝑦) (none)
Predicates: (𝑥 < 𝑦) (𝑥 < 𝑦) (𝑥 = 𝑦)
(𝑥 = 𝑦), (𝑥 < 𝑦), (𝑦 = 2) 2
(𝑦 = 2) (𝑦 = 2) (𝑦 = 2)

13
 Predicate abstraction: Efficient approach
 Performing abstraction: A more efficient attempt
o Enumerate abstract states only
• Predicate set 𝑃: there are 𝐿 ∙ 2 𝑃 possible abstract states
o Checking the feasibility of abstract states
and then the state transitions as well
𝑥=𝑦 𝑥<𝑦 𝑦=2
 Example for Dx=Dy={0,1,2} domain: 1 - - -
o Enumerating abstract states: 2 - - 
3 predicates  8 abstract states 3 -  -
possible for each location in L 4 -  

o Checking feasibility of abstract states 5  - -

• E.g. (𝑥 = 𝑦) ∧ (𝑥 < 𝑦) ∧ ¬(𝑦 = 2) 6  - 

is not feasible (not satisfiable) 7   -
• Use SMT solver to check whether a 8   
combination of predicates is satisfiable
14
 Predicate abstraction: Definition (1)
 Abstract states with predicate abstraction
Concrete Abstract

o (𝑙, 𝑥1 , … , 𝑥𝑛 ) → (𝑙, 𝑏1 , … , 𝑏𝑚 )
o 𝑏𝑖 : Boolean variable, its value gives if predicate pi holds or not
𝑝𝑖 if 𝑏𝑖 is true
o Notation: 𝑝(𝑏𝑖 ) =
¬𝑝𝑖 otherwise
Concrete Abstract
 Example:
𝑙𝑥𝑦 𝑙 𝑏1 𝑏2 𝑏 3
Variables:
𝑥, 𝑦; 𝐷𝑥 = 𝐷𝑦 = 0,1,2 0,0,0 → 0, 𝑇, 𝐹, 𝐹
Predicates: 6,1,2 → 6, 𝐹, 𝑇, 𝑇
(𝑥 = 𝑦), (𝑥 < 𝑦), (𝑦 = 2)
𝑙 𝑥=𝑦 𝑥<𝑦 𝑦=2
15
 Predicate abstraction: Definition (2)
 Abstract initial states and error states:
o Abstract initial state: (𝑙, 𝑏1 , … , 𝑏𝑚 ), where 𝑙 = 𝑙0
o Abstract error state: (𝑙, 𝑏1 , … , 𝑏𝑚 ), where 𝑙 = 𝑙𝐸
 Abstract transition: at least one concrete transition may
exist between contained concrete states
o (𝑙, 𝑏1 , … , 𝑏𝑚 )  𝑙 ′ , 𝑏 ′1 , … , 𝑏 ′ 𝑚 abstract transition exists if
• ∃ 𝑙, 𝑜𝑝, 𝑙 ′ ∈ 𝐺
i.e., there is an edge with op between locations l and l’ in the CFA,
• and 𝑝 𝑏1 ∧ ⋯ ∧ 𝑝 𝑏𝑚 ∧ 𝑜𝑝 ∧ 𝑝 𝑏′1 ∧ ⋯ ∧ 𝑝 𝑏′𝑚 is satisfiable
o Feasibility check by SMT solver (without enumerating concrete states)

Existential abstraction:
Such transition exists in the abstract state space,
but not necessarily reachable in the concrete state space
16
 Predicate abstraction (5)
 Example:
𝑃= 𝑥≤5

 Abstract states: 6 locations, 1 predicate  12 abstract states

17
 Predicate abstraction (6)
 Example:
𝑃= 𝑥≤5

 Abstract transitions: checking feasibility along edges of the CFA

o E.g., (2, true)  1, true is feasible
• 2, 𝑜𝑝, 1 ∈ 𝐺, where the operation 𝑜𝑝 is 𝑥 = 𝑥 + 1
• 𝑥 ≤ 5 ∧ (𝑥 ′ = 𝑥 + 1) ∧ 𝑥′ ≤ 5 is satisfiable, for example with 𝑥 = 0, 𝑥 ′ = 1
o E.g., (1, true)  (2, false) is not feasible
• (1, 𝑜𝑝, 2) ∈ 𝐺, where 𝑜𝑝 is the guard [𝑥 < 5]
• 𝑥 ≤ 5 ∧ ( 𝑥 < 5 𝑥 ′ = 𝑥) ∧ ¬ 𝑥′ ≤ 5 is not satisfiable
18
 Model checking
 Traversing the abstract state space
o Searching for error state
o With some search strategy, e.g., DFS, BFS, symbolic
 Optimizations
o On-the-fly
• Calculate abstract states
during the search
o Incremental
• Do not explore
unchanged parts
after refinement

19
 Model checking: Properties
 Properties of existential abstraction
o Over-approximates the original model
• For each concrete path, there is a corresponding abstract path
• If Error state is not reachable in the abstract state space (¬EF Error),
then it is not reachable in the original state space
o What about abstract counterexamples (reaching Error state)?
• Not all abstract paths have corresponding concrete paths!

20
 Abstract counterexample
 Form of abstract counterexample
o Sequence of locations and predicates
o 𝑙1 , 𝑏1,1 , … , 𝑏1,𝑚 , 𝑙2 , 𝑏2,1 , … , 𝑏2,𝑚 , … , 𝑙𝑛 , 𝑏𝑛,1 , … , 𝑏𝑛,𝑚
 Finding a concrete path: trying to traverse the concrete
state space
o Guided by the abstract counterexample
o Using SMT solver to check transitions
• Starting from the initial state
• Traversing: Similarly to bounded model checking (BMC)
• Considering locations and guards/statements for 𝑛 steps
 Concrete path exists: concrete model is faulty
 Concrete path does not exist: counterexample is spurious
21
 Abstract counterexample (example)
 Example Abstract state space Counterexample

𝑥1 ≤ 5
𝑥1 = 𝑎𝑛𝑦
𝑥2 = 0
𝑥2 = 0
𝑥3 = 0
𝑥2 ≤ 5
𝑥4 = 1
𝑥2 < 5 ∧ 𝑥3 = 𝑥2
𝑥3 ≤ 5 ¬(𝑥4 ≤ 5)
does not hold
𝑥4 = 𝑥3 + 1
¬(𝑥4 ≤ 5)
¬(𝑥4 < 5) ∧ 𝑥5 = 𝑥4
¬(𝑥5 ≤ 5)
¬(𝑥5 ≤ 5) ∧ 𝑥6 = 𝑥5
¬(𝑥6 ≤ 5)

𝑃= 𝑥≤5 Abstract counterexample Concrete Predicates

along feasible transitions operations on in the states
(6 states) transitions;
xi+1=xi if there
is no change
22
 Spurious counterexample in general
 A concrete path is “broken” in a so-called “failure” state
 Grouping concrete states mapped to
failure
the “failure” state
o D = “Dead-end”: reachable
o B = “Bad”: transition to next state
o IR = “Irrelevant”: others
o No transition from “dead-end” to “bad”
 Reason for spurious counterexample
o D and B are in the same abstract state
o Set of predicates does not distinguish D and B
(this is why these are in the same abstract state)

23
 Abstraction refinement
 Eliminating the spurious counterexample
o More predicates (finer abstraction) needed
o Separate D and B 𝜑
• Without enumerating concrete states
• Describe D and B with formulas over variables ¬𝜑
• SMT solver can generate a formula 𝜑
that separates D and B (interpolation):
𝜑 is true for D and false for B
o The predicate set 𝑃 ∪ 𝜑 will eliminate
this spurious counterexample
• Moreover it is enough to split only the
failure state (lazy abstraction)
 Additional spurious counterexamples
o More predicates may be needed
24
 Abstraction refinement (example)
 Example

Looking for the additional

predicate informally:
What are the concrete states
included in the abstract states?
What have to be separated?

If x<5: (2,true)  (1,true)

𝑃= 𝑥≤5 If x=5: (2,true)  (1,false)

𝑥 < 5 additional
predicate
is needed

25
 Abstraction refinement (example)
 Example

𝑃= 𝑥≤5 𝑃= 𝑥 ≤ 5 , (𝑥 < 5)

Error state is
not reachable

26
 CEGAR: Summary

Concrete state space Abstraction Abstract state space

Refined state space Spurious counterexample Abstract counterexample

Property holds
OK Counterexample

Model, Abstraction Abstract counterex

Check Concretize Concrete
property
Init Refine
27
 The algorithm
 Counterexample-Guided Abstraction Refinement (CEGAR)
o Tool-supported method
• Each step is automatic
• Deep knowledge of formal methods is not required
• Hidden steps: checking feasibility of abstract states and transitions
+ interpolation (using and SMT solver)
o How about the initial set of predicates?
• It can be an empty set (to be refined automatically)
• It can come from conditional statements in the software
• Other heuristics may also be used

Property holds
OK Counterexample

Model, Abstraction Abstract counterex

Check Concretize Concrete
property
Init Refine
28
 Summary
 Software model checking
o Common problem: state space explosion
o Solution: abstraction
• Location + predicates
• Properties of existential abstraction
o CEGAR: automatically obtain proper abstraction
1. Initial abstraction
2. Model checking
3. Examining the counterexample
4. Refining the abstraction
o Tools

29
Example tools

30
 Example tools: Overview
 SLAM2
o Part of the MS Static Driver Verifier Research Platform
o Structure
• Analyzed component: C code of device driver programs
• Analysis: adherence to platform + API usage rules
o Algorithms
• Create Boolean program with predicate abstraction
• Symbolic model checking: BEBOP tool
• CEGAR loop
o research.microsoft.com/en-us/projects/slam/

31
 Example tool: BLAST
 BLAST
o Berkeley Lazy Abstraction Software Verification Tool
o Input: C program + requirement (BLAST Query Lang.)
o Predicate abstraction
• Building abstract reachability tree (ART)
o Refinement: new predicate with interpolation
• Lazy abstraction: apply the new predicate only locally
o Limitations: multiplication, bit operations, overflow
o mtc.epfl.ch/software-tools/blast/index-epfl.php

32
 Example tool: CPAchecker
 CPAchecker
o (Continuation of BLAST)
o The Configurable Software-Verification Platform
o Input: C program + specification
• Assertion, error label, deadlock, null dereference, …
o Highly configurable
• Different kinds of abstractions (not only predicate)
• Chooses from different refinements (refinement strategy)
o cpachecker.sosy-lab.org/

33
 Example tool: Theta
 Theta
o Generic, modular, configurable model checking
framework
o Developed at BME MIT
o Generic: various kinds of formal models
• Transition systems, control flow automata, timed automata
o Modular: reusable and combinable modules for
abstraction and refinement
o Configurable: different algorithms and strategies
o github.com/FTSRG/theta

34
 Competition of tools
 Competition on Software Verification (SV-COMP)
o https://sv-comp.sosy-lab.org/2022/
o 47 tools, 15.648 input tasks (C program + requirement)
o Categories: Find the best tool in a given category
• Arrays (ArraysReach, ArraysMemSafety)
• Bit Vectors (BitVectorsReach, Overflows)
• Heap Data Structures (HeapReach, HeapMemSafety)
• Floats
• Integers and Control Flow (ControlFlow, Simple, ECA, Loops, Recursive,
ProductLines, Sequentialized)
• Termination
• Concurrency
• Software Systems (DeviceDriversLinux64, BusyBox)
o Results provide hints about the capabilities of tools
35
 Tool demo:
CPAchecker

Model checking of C programs

36
Software model checking with CPAchecker
 The Configurable Software-Verification Platform
o http://cpachecker.sosy-lab.org/ Java based
o http://cpachecker.appspot.com/ online
 Input: C program + specification (verification options)
o Checks: Assertions, reachability of error labels, deadlock,
null dereference, …
 Goals integrated
o Program analysis: Simple properties of complex programs
o Model checking: Behavioral properties of simple programs
 Highly configurable
o Several checkers and abstractions
o Abstraction refinement: CEGAR
37
 Supported verification methods
 CEGAR, Predicate abstraction, Lazy abstraction, Interpolation
 Bounded model checking, k-induction
 Symbolic execution

38
 Input of CPAchecker
 C program after preprocessing
o #define, #include, etc. resolved
o gcc -E program.c > program.i
 Supported language constructs depend on the
applied SMT solver
(e.g., Linux: MathSAT5, Windows: SMTInterpol)
o Integer, float
o Array, bitvector, list
o Pointer, heap
o Dynamic memory allocation
o Recursion, multiple concurrent threads, …
 Handling multiple source files
39
 Output of CPAchecker
 HTML report (interactive)
o CFA: Control Flow Automaton
o ARG: Abstract Reachability Graph
o Source code (jumping to statements from the CFA)
o Counterexample:
• Program execution path:
presented on source code,
on CFA, or ARG
• Step-by-step execution
interactively
(on CFA and source code)
• Values of variables
presented (see -V-)
o Statistics
40
 Configurability
 Command line interface
o cpa.bat -spec <spec> -config <config> <prog.c>
 Specifications and configurations (there is no ”best option”)

• Specifications: what is to be checked

• Assertion.spc: assertion violation in the code
• ErrorLabel.spc: ERROR label reachability in the code
• TerminatingFunctions.spc: terminating function (e.g., exit, abort)
• Deadlock.spc: deadlock in a concurrent program
• Null-deref.spc: null-pointer dereference
• UninitilizedVariables.spc: uninitialized variable or return value
• Memory hadling: MemorySafety-deref (invalid derefencing of pointers),
MemorySafety-free (invalid freeing of allocations),
MemorySafety-memtrack (memory leaks)

41
 Configurability
 Command line interface
o cpa.bat -spec <spec> -config <config> <prog.c>
 Specifications and configurations (there is no ”best option”)

• Configurations: how to check the properties

• Abstractions (predicate, value, …) and refinements
• Default: default.properties, sequential analyses
• Predicate abstraction for overflow checking
• Lasso analysis for termination checking
• Using BDD for concurrent programs
• Using predicate abstraction for recursive programs
• Using k-induction for other cases
• Other recommended configurations
• predicateAnalysis.properties (CEGAR)
• predicateAnalysis-bitprecise.properties

42
 Short demo
 Assertion checking
o Successful and erroneous output (after modification)
o Presentation of the counterexample: Source code,
variables, CFA
 ERROR label checking
o Counterexample on source code and CFA
 Bubbleshort algorithm verification
o Several CFA (for the functions)
 Linux Driver Verification Project
o Problems in Linux Kernel Found by CPAchecker
http://linuxtesting.org/results/ldv-cpachecker

44