Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Software program
Reexamination Certificate
2005-01-21
2008-03-18
Jones, Hugh (Department: 2128)
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Software program
C703S002000, C717S124000, C717S141000, C714S038110
Reexamination Certificate
active
07346486
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.
REFERENCES:
patent: 6292916 (2001-09-01), Abramovici et al.
patent: 6539345 (2003-03-01), Jones et al.
patent: 6665848 (2003-12-01), Ben-David et al.
patent: 6944848 (2005-09-01), Hartman et al.
patent: 7031896 (2006-04-01), Yang
patent: 7047139 (2006-05-01), Shtrichman
patent: 2002/0062463 (2002-05-01), Hines
patent: 2002/0087953 (2002-07-01), Hines
patent: 2003/0208351 (2003-11-01), Hartman et al.
patent: 2003/0225552 (2003-12-01), Ganai et al.
patent: 2004/0019468 (2004-01-01), De Moura et al.
patent: 2004/0123254 (2004-06-01), Geist et al.
patent: 2005/0229044 (2005-10-01), Ball
patent: 2006/0190865 (2006-08-01), Yu et al.
patent: 2006/0282807 (2006-12-01), Ivancic et al.
patent: 2007/0011671 (2007-01-01), Kahlon et al.
Williams, R. et al. “Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking,” Carnegie Mellon University Feb. 2000.
Rugina, R., et al., “Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions,”PLDI 2000.
Ganai, M.K. et al, “Combining Strength of circuit-based and CNF-based algorithms for a high performance SAT solver,” Design Automation Conference, 2002.
Goldberg, E. and Novikov, Y., “Berkmin: A fast and robust SAT solver,” in Design Automation and Test in Europe, pp. 132-139, 2002.
Marques-Silva, J.P. and Sakallah, K.A., “GRASP: A search algorithm for prepositional satisfiability,” IEEE Transactions on Computers, vol. 48, pp. 506-521, 1999.
Moskewicz, M. et al, “Chaff: Engineering an efficient SAT solver,” in Design Automation Confernece, 2001.
Gupta, A. et al, “Iterative absrtraction using SAT-based BMC with proof analysis,” International Conference on Computer-Aided Design (ICCAD), pp. 416-423, Nov. 2003.
Necula, G.C. et al, “CIL: Intermediate language . . . of C Programs,” Proc. of the 11th Int.Conf. on Computer Construction, LNCS, pp. 213-228, Springer-Verlag, 2002.
Tip, F., “A survey of programe slicing techniques,” J. of Programming Languages, vol. 3, No. 3, pp. 121-189, Sep. 1995.
McMillan, K., “Applying SAT Methods In Unbounded Model Checking,”CAV 2002, pp. 250-264, 2002.
Ashar Pranav N.
Ganai Malay
Gupta Aarti
Ivancic Franjo
Yang Zijiang
Jones Hugh
NEC Laboratories America, Inc.
Saxena Akash
LandOfFree
System and method for modeling, abstraction, and analysis of... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with System and method for modeling, abstraction, and analysis of..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System and method for modeling, abstraction, and analysis of... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3967200