why software model checking?
want to analyze specs but
no commensurate analysis
only theorem proving and type checking?
formal specifications are write-only
model checking offers
automation of deep analysis
focus on presence not absence of errors
rich property language