| 摘要 |
In one embodiment, a computer system identifies a portion of software code that is to be verified using invariants. The computer system infers invariants from the software code portion at a join point. The linear inequalities of the invariants include a first abstract domain that includes linear equalities among variables, and a second, different abstract domain that includes intervals for variables. The computer system selects variables that are to be applied within the linear inequalities to form a linear equality and an interval based on the linear inequality and performs a reduction operation on the variables to determine the substantially tightest numerical bounds for the variable's interval. The computer system also performs a join operation of the first and second abstract domains, where the join results in a precise abstraction of various possible software program states at the join point in the software program.
|
