Back to results
US 2010/0251222 A1Published application
Completeness determination in smt-based bmc for software programs
AssigneeNEC Laboratories America, Inc.
InventorMalay Ganai
Life of this patent
Estimating the term…
Abstract
A computer implemented method for obtaining a completeness threshold (CT) in Bounded Model Checking systems for software programs.
Claims3
In a computer comprising a Central Processor, a Memory, and or more Input/Output devices, a bounded model checking method comprising the steps of:
- loading a computer program to be checked into the memory;
- generating a model of the program so loaded;
- determining the longest non-terminating path in the model by
- encoding the reachability of a sink control state into a SAT/SMT formula having a size linearly proportional to a sequential depth;
- and
- outputting an indication of that longest non-terminating path via the one or more Input/Output devices.
3 more elements
A computer-implemented bounded model checking method for software comprising the steps of:
- loading the software into a memory of a computer;
- generating a model of the software in the memory through the effect of a processor;
- determining a recurrence diameter of the model corresponding to a terminating program by encoding the reachability of a sink control stat into a SAT/SMT formula having a size proportional to a sequential depth;
- and
- outputting an indication of that recurrence diameter.
2 more elements
In a computer comprising a Processor, Memory and Input/Output, a computer-implemented bounded model checking method for a software program comprising the steps of:
- loading the program into the memory of the computer;
- determining the reachability of the program through the effect of a SAT/SMT formula operating therein, wherein said SAT/SMT formula is reduced in size as a result of combining context-sensitive components with control-state reachability simplification;
- and
- outputting the indication of that reachability.
1 more element
Dependencies are inferred from the claim text.