Data processing: structural design – modeling – simulation – and em – Modeling by mathematical expression
Reexamination Certificate
2008-07-29
2008-07-29
Frejd, Russell (Department: 2128)
Data processing: structural design, modeling, simulation, and em
Modeling by mathematical expression
C703S014000, C716S030000, C716S030000
Reexamination Certificate
active
10357585
ABSTRACT:
A design verifier includes a bounded model checker, an abstractor and an unbounded model checker. The bounded model checker verifies a property to a depth K and either finds a counterexample, or generates a proof in the form of a directed acyclic graph. If no counterexample is found, the abstractor generates an abstracted design description using a proof generated by the bounded model checker. The unbounded model checker verifies the property of the abstracted design description. If a counterexample is found, the bounded model checker increases K and verifies the property to the new larger depth. If no counterexample is found, the design is verified.
REFERENCES:
patent: 5440568 (1995-08-01), Foster
patent: 2002/0138812 (2002-09-01), Johannsen
patent: 2003/0225552 (2003-12-01), Ganai et al.
patent: 2004/0019468 (2004-01-01), De Moura et al.
Li et al., A Satisfiability-Based Approach to Abstraction Refinement in Model Checking, Electronic Notes in Theoretical Computer Science, vol. 89, No. 4, 2003, pp. 608-622.
Wing et al., A Case Study in Model Checking Software Systems, Science of Computer Programming, vol. 28, Nos. 2-3, Apr. 1997, pp. 273-299.
Cabodi, Gianpiero et al., “Can BDDs Compete With SAT Solvers on Bounded Model Checking?”, DAC 2002, Jun. 10-14, 2002, New Orleans, Louisiana, USA, Copyright 2002 ACM 1-58113-461-04/02/0006, Abstract.
Biere, Armin, “Verifying Sequential Behavior With Model Checking”, Computer Systems Institute, ETH Zürich, Switzerland, Abstract.
Clarke, Edmund et al., “Bounded Model Checking Using Satisfiability Solving”, Computer Science Department, CMU, Abstract.
A. Biere, C. Artho, V. Schuppan, “Liveness Checking as Safety Checking,” Electronic Notes in Theoretical Computer Science 66 No. 2 (2002), 18 pages.
D. A. Plaisted, S. Greenbaum, “A Structure-preserving Clause Form Translation,” J. Symbolic Computation (1986) 2, Academic Press Inc. (London Ltd.), pp. 293-304.
K. L. McMillan, N. Amla, “Automatic Abstraction with Counterexamples,” Cadence Design Systems, LNCS 2619, 2003, pp. 2-17.
M. W. Moskewicz, C. F. Madigan, “Chaff: Engineering an Efficient SAT Solver,” in Design Automation Conference, 2001, pp. 530-535.
P. Pudlak, “Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations, ”The Journal of Symbolic Logic, vol. 62, No. 3, Sep. 1997, pp. 981-998.
M. Sheeran, S. Singh, G. Stalmarck, “Checking Safety Properties Using Induction and a SAT-Solver,” in Formal Methods in Computer Aided Design, 2000, pp. 108-125.
L. Zhang, S. Malik, “Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications,” In Date '03, pp. 880-885, 2003.
J. R. Burch, E. M. Clark, K. L. McMillan, D. L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking,” Proc. Design Automation Conf. Orlando, FL, Jun. 1990, pp. 46-51.
J. R. Burch, E. M. Clark, K. L. McMillan, D. L. Dill, L. J. Hwang, “Symbolic Model Checking: 1020 States and Beyond,” in Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1-33, Washington, D.C., 1990, IEEE Computer Society Press.
A. Gupta, Z. Yang, P. Ashar, A. Gupta, “SAT-Based Image Computation with Application in Reachability Analysis,” in FMCAD 2000, pp. 354-371, 2000.
J. Baumgartner, A. Kuehlmann, J. Abraham, “Property Checking via Structural Analysis,” in Computer-Aided Verification (CAV 2002), pp. 151-165.
A. Biere, A. Cimatti, E. Clark, Y. Zhu, “Symbolic Model Checking Without BDDs, ”in TACAS '99, vol. 1579 of LNCS, pp. 193-207.
P. Bjesse, “Symbolic Model Checking With Sets of States Represented as Formulas,” Technical Report CS-1999-100, Department of Computer Science, Chalmers Technical University, Mar. 1999, 17 pages.
P.A. Abdulla, P. Bjesse, N. Een, “Symbolic Reachability Anaysis Based on SAT-Solvers,” in TACAS 2000, vol. 1785 of LNCS, Springer-Verlag, pp. 411-425.
P. Bjesse, T. Leonard, A. Mokkedem, “Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers,” Chalmers University of Technology, Sweden, 2001, pp. 454-464.
R. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, vol. C-35, No. 8, Aug. 1986, pp. 677-691.
O. Courdert, C. Berthet, J. C. Madre, “Verification of Synchronous Sequential Machines Based on Symbolic Execution,” Bull Research Center, P.C. 58B, 68 Route de Versailles, 78430 Louveciennes, France, pp. 365-373.
F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, M. Y. Vardi, “Benefits of Bounded Model Checking at an Industrial Setting,” Formal Property Verifications, Intel Corporation, Haifa, Israel, CAV 2001, LNCS 2102, 2001, pp. 436-453.
E. Goldberg, Y. Novikov, “Berkmin: a Fast and Robust Sat-Solver,” 2002, pp. 142-149.
O. Kupferman, M.Y. Vardi, “Model Checking of Safety Properties,” Formal Methods in System Design, 19, 2001, pp. 291-314.
J.P.M. Silva, K.A. Sakallah, “Grasp A New Search Algorithm for Satisfiability,” 1996 IEEE, pp. 220-227.
M.Y. Vardi, P. Wolper, “An Automata-Theoric Approach to Automatic Program Verification (Preliminary Report),” IBM Research, AT&T Bell Laboratories, 1986 IEEE, pp. 332-344.
P.F. Williams, A. Biere, E.M. Clark, A. Gupta, “Combining Decision Diagrams and SAT pProcedures for Efficient Symbolic Model Checking,” Semiconductor Research Corporation, CAV 2000, LNCS 1855, pp. 124-138.
W. Craig, “Linear Reasoning, A New Form of the Herbrand-Gentzen Theorem.” Journal of Symbolic Logic, vol. 22, No. 3, Sep. 1957, pp. 250-268.
O. Lichtenstein, A. Pnueli, “Checking That Finite State Concurrent Programs Satisfy Their Linear Specification,” Principles of Programming Languages (POPL 85), 1985, pp. 97-107.
A. Pnueli, L. Zuck, “Probabilistic Verification by Tableaux,” Department of Computer Science, The Weizmann Institute of Science, Rehovot 76100, Israel, 1986 IEEE, pp. 322-331.
K.L. McMillan, “Interpolation and SAT-Based Model Checking,” Cadence Berkeley Labs, CAV 2003, Jul. 8, 2003, 13 pages.
K.L. McMillan, “Symbolic Model Checking,” Carnegie Mellon University, Kluwer Academic Publishers, 1993, pp. 25-39.
E.M. Clark, A. Biere, R, Raimi, Y. Zhu, “Bounded Model Checking Using Satisfiability Solving,” Semiconductor Research Corporation, National Science Foundation, pp. 1-20.
A. Biere, A. Cimatti, E.M. Clark, O.F. Strichman, Y. Zhu, “Bounded Model Checking,” Semiconductor Research Corporation, National Science Foundation, Army Research Office, Office of Naval Research, Naval Research Laboratory, 27 pages.
A. Biere, “Verifying Sequential Behavior with Model Checking,” Computer Systems Institute, ETH Zurich, ETH Zentrum, RZ H, CH-8092 Zurich, Switzerland, 4 pages.
Cabodi, Gianpiero et al., “Can BDDs Compete With SAT Solvers on Bounded Model Checking?”, Jun. 2002, Design Automation Conference, pp. 117-122.
McMillan et al., “Methods for Exploiting SAT Solvers in Unbounded Model Checking”, Jun. 2003, First ACM and IEEE International Conference, pp. 135-142.
Amla Nina
McMillan Kenneth L.
Alford William E.
Cadence Design Systems Inc.
Frejd Russell
Lycke Lawrence
Orion Law Group, PLC.
LandOfFree
Method and system for design verification using proof-based... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and system for design verification using proof-based..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for design verification using proof-based... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3913949