Quote: eliminate spurious paths in a Boolean program by automatically adding boolean control variables; e.g., resource allocation within loops and conditionals

Quotation Skeleton

Slam uses a counterexample-driven refinement technique to eliminate … [corresponding to a C program]. … Slam uses symbolic execution to determine if [an erroneous path] is feasible in the original C program. … If infeasible, Slam identifies a small predicate set … Slam uses this predicate to refine its model … [For example, Slam can verify resource acquisition/release inside while loops and conditionals, by adding boolean control variables.]   Google-1   Google-2

Copyright clearance needed for quotation.

Related Topics

Topic: model checker (49 items)
Topic: owned resources and data objects (12 items)