System and method for modeling, abstraction, and analysis of software
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.
1. 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; b i denotes an element of a Boolean predicate vector; B R is a set of Boolean variables computed on the basis of all predicates; p i is a single predicate being considered p j 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.
2. 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; b i denotes the Boolean predicate vector; B R is a set of Boolean variables computed on the basis of all predicates; p i is a single predicate being considered; p j 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.