Verification, Least-Fixpoint Checking, Abstraction

  • Andreas Podelski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


We consider verification algorithms in a wide sense. The out-come of a verification algorithm can be a definite (yes or no) answer, a “don’t know” answer, or a conditional answer or no answer at all (divergence). We obtain these kinds of verification algorithms if we apply the existing technology of abstraction to least-fixpoint checking, i.e., checking whether the least fixpoint of a given operator in a given lattice is smaller than a given bound. The formulation of the verification algorithm as least-fixpoint checking is classical for the class of correctness properties that are reducible to non-reachability (validity of assertions, partial correctness, safety properties). We need to investigate the approach also for the class of correctness properties that are reducible to termination (validity of intermittent assertions, total correctness, liveness properties), for all classes of programs including procedural (recursive) programs and concurrent programs.

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Andreas Podelski
    • 1
  1. 1.University of Freiburg 

Personalised recommendations