Abstracting programs and models

Programs are too complex for model checkers, to be modeled and verified as such.

  • Model checkers don’t take real “programs” as input
  • Model checkers typically work on finite state systems
  • Abstraction therefore solves two problems
  1. It allows model checkers to analyze a notation they couldn’t deal with before, and,
  2. Cuts the state space size to something manageable

Types of abstaction

Hence, abstracting is needed. Abstraction comes in three flavors
  1. Over-approximations, i.e. more behaviors are added to the abstracted system than are present in the original
  2. Under-approximations, i.e. less behaviors are present in the abstracted system than are present in the original
  3. Precise abstractions, i.e. the same behaviors are present in the abstracted and original program
Under-approximation, “Meat-Axe” Abstraction
  • Remove parts of the program deemed “irrelevant” to the property being checked
    • Limit input values to 0..10 rather than all integer values
    • Vector size 5 instead of unbounded, etc.
  • The abstraction of choice in the early days of program model checking – used during the translation of code to a model checker’s input language
  • Typically manual, with no guarantee that the right behaviors are removed.
  • Precise abstraction, w.r.t. the property being checked, may be obtained if the behaviors being removed are indeed not influencing the property
    • –Program slicing is an example of an automated under-approximation that will lead to a precise abstraction w.r.t. the property being checked

Over-approximation, Abstract Interpretation

  • Maps sets of states in the concrete program to one state in the abstract program
    • Reduces the number of states, but increases the number of possible transitions, and hence the number of behaviors
    • Can in rare cases lead to a precise abstraction
  • Type-based abstractions
    • Replace int by Signs abstraction {neg,pos,zero}
  • Predicate abstraction
    • Replace predicates in the program by boolean variables, and replace each instruction that modifies the predicate with a corresponding instruction that modifies the boolean.
  • Automated (conservative) abstraction
  • Eliminating spurious errors is the big problem
    • Abstract program has more behaviors, therefore when an error is found in the abstract program, is that also an error in the original program?
    • Most research focuses on this problem, and its counter-part the elimination of spurious errors, often called abstraction refinement

Precise Abstraction, Bringing Model Checking to Programs

  • Allow model checkers to take modern programming languages as input, or, notations that are of similar expressive power
  • Major hurdle is how to encode the state of the system efficiently
  • Alternatively state-less model checking
    • No state encoding or storing
  • Almost exclusively explicit-state model checking
  • Abstraction can still be used as well
    • Source to source abstractions

Principles of abstraction of symbolic analysis

Symbolic analysis uses precise abstraction in a way, although it converts the program clauses into a higher-abstraction language, Symbolic. From Symbolic it is possible to generate original code, under certain conditions.
  • Symbolic analysis removes the hurdle of how to encode the state of the system efficiently (th major problem of precise abstraction), by using object system of the tool. Every state is an independent object, capable to present itself and bi-directional references to its creator.
Some links: