Back to results
US 7,346,486 B2Granted
System and method for modeling, abstraction, and analysis of software
AssigneeNEC Laboratories America, Inc.
InventorsFranjo Ivancic, Pranav N. Ashar, Malay Ganai, Aarti Gupta, Zijiang Yang
Life of this patent
Estimating the term…
Abstract
A system and method is disclosed for formal verification of software programs that advantageously translates the software, which can have bounded recursion, into a Boolean representation comprised of basic blocks and which applies SAT-based model checking to the Boolean representation.
Claims2
A computer-implemented method of verifying a software program comprising:
- determining one or more properties of the software program to be verified;
- generating a model of the software program wherein said model comprises a Boolean representation having a plurialty of basic blocks, each basic block representing a sequence of one or more instructions in the software program as a set of parallel assignments and a set of transitions to other basic blocks;
- applying a SAT-based model checker to the Boolean representation of the software program;
- and
- determining whether the properities are correct and
- generating an output indicative of that correctness determination for the software program;
- wherein said model of the software program is one of a type selected from the group consisting of:
- bounded-recursive and non-recursive;
- wherein transition relations in the Boolean representation of the software program are enumerated and represented by:
- 𝒯
-
- (
- b
- ,
- b
- ′
- ,
- χ
- )
- :=
- ⩓
- b
- i
- ∈
- B
- R
-
- b
- i
- ⇔
- p
- i
- ⋀
-
- ⩓
- b
- i
- ∈
- B
- v
-
- b
- i
- ′
- ⇔
- p
- i
-
- [
- V
- ←
- e
- 1
- ,
- …
-
- ,
- e
- n
- ]
- ⋀
-
- ⩓
- b
- i
- ∉
- B
- v
-
- b
- i
- ′
- =
- b
- i
- where b,b′i are boolean variables in an abstract model;
- X is the set of all variables in the program;
- bi denotes an element of a Boolean predicate vector;
- BR is a set of Boolean variables computed on the basis of all predicates;
- pi is a single predicate being considered pj is an expression in terms of variables used in a concrete model;
- V is set to values of concrete variables and e are expressions of assignments made to those variables in a basic block.
78 more elements
A computer-implemented method of verifying a software program comprising:
- determining one or more propoerties of the software to be verified;
- generating a model of the software program wherein said model comprises a Boolean representation having a plurality of basic blocks, each basic block representing a sequence of one or more instructions in the software program as a set of parallel assignments and a set of transitions to other basic blocks;
- applying a SAT-based model checker to the Boolean representation of the software program;
- and
- determining whether the properties to be verified are correct;
- and
- generating an output indicative of that correctness determination for the software program;
- wherein said model of the software program is one of a type selected from the group consisting of:
- bounded-recursive and non-recursive;
- wherein transition relations in the Boolean representation of the software program are enumerated using SAT-based enumeration;
- and
- wherein transition relations in the Boolean representation of the software program are enumerated and represented by:
- 𝒯
-
- (
- b
- ,
- b
- j
- ′
- ,
- χ
- )
- :=
- ⩓
- b
- i
- ∈
- B
- R
-
- b
- i
- ⇔
- p
- i
- ⋀
- b
- j
- ′
- ⇔
- p
- j
-
- [
- V
- ←
- e
- 1
- ,
- …
-
- ,
- e
- n
- ]
- where b,b′j are boolean variables in an abstract model;
- X is the set of all variables in the program;
- bi denotes the Boolean predicate vector;
- BR is a set of Boolean variables computed on the basis of all predicates;
- pi is a single predicate being considered;
- pj is an expression in terms of variables used in a concrete model;
- V is set to values of concrete variables and e are expressions of assignments made to those variables in a basic block.
60 more elements
Dependencies are inferred from the claim text.