System and method for modeling, abstraction, and analysis of software

• US 7,346,486 B2
• Filed: 01/21/2005
• Issued: 03/18/2008
• Est. Priority Date: 01/22/2004
• Status: Active Grant

• Current Assignee: NEC Corporation
• Original Assignee: NEC Laboratories America Inc (NEC Corporation)
• Inventors: Ashar, Pranav N., Yang, Zijiang, Gupta, Aarti, Ivancic, Franjo, Ganai, Malay
• Primary Examiner(s): Jones; Hugh
• Assistant Examiner(s): Saxena; Akash
• Application Number:
  US11/040,409
• Publication Number:
  US 20050166167A1
• Time in Patent Office: 1,152 Days
• Field of Search: 716 4- 5, 703/2, 703/22
• US Class Current: 703/22
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

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.

Claims

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;

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;