This 2009 survey of software model checking covers a lot of ground from the roots in hardware model checking through to its application to software. A number of the key algorithms are described in pseudocode.
The sections give a good sense of what is covered
 Introduction
 Preliminary definitions
 Simple programs
 Properties
 Organization

Concrete enumerative model checking
(For small, finite state spaces)

Stateful search
Forward and backward algorithms, Partial order reduction, compositional techniques, assumeguarantee

Systematic execution exploration
Test amplification
 Stateless search

Executionbased tools
VeriSoft, JavaPathFinder, Cmc, MaceMC

 Concrete symbolic model checking

The region data structure
SymbolicReachability algorithm, reachability

Example: propositional logic
BDDs
 Example: first order logic with interpreted theories

Invariants and invariant synthesis
abstraction techniques for invariant synthesis, kinduction, templatebased synthesis


Model checking and abstraction

Abstract reachability analysis
Finite height domains; infinite height domains and widening operators
 Example: polyhedral domains

Example: predicate abstraction
SLAM verifier, BLAST verifier, cartesian predicate abstraction

Example: control abstraction
sequential programs, concurrent programs

Combined abstractions
Gulwani and Tiwari shows a general framework for combining abstract interpretations for different theories, analogous to the manner in which decision procedures for different theories are combined.


Abstraction refinement
 Counterexamples and refinement
 Counterexamples
 Trace formulas
 Syntaxbased refinement
 Interpolationbased refinement
 Relative completeness
 Refining multiple paths
 Refining other domains
 Abstractionrefinementbased model checkers
 SLAM verifier and BEBOP
 BLAST verifier and lazy refinement
 Magic and concurrent, messagepassing C programs
 FSoft
 IMPACT
 ARMC
 Counterexamples and refinement
 Procedural abstraction
 Programs with procedures

InterProcedural reachability
memoization
 Graphbased algorithms
 Symbolic algorithms
 Abstraction
 Topdown vs. Bottomup
 Saturn
 Houdini
 Concurrency and recursion
 Heap data structures
 Alias analysis
 Shape analysis
 Separation logic
 Reachability predicates
 Quantified loop invariants
 Liveness and termination

Finite state
Büchi automaton, LTL temporal logic, pushdown systems

Infinite state
Program termination, fairness conditions

Nontermination

 Model checking and software quality

Model checking and testing
underapproximation
 Test generation by symbolic evaluation

Model checking and type systems
 Typestates
 Dependent types
 Hybrid type checking

 Conclusion
Notes related to Software model checking
Bounded modelchecking, Model checking
Papers related to Software model checking
 Model checking [mcmillan:ecs:2003]