Automatic abstraction of software source

Details Automatic abstraction of software source Automatic abstraction of software source

2006-12-05

2006-12-05

Chaki, Kakali (Department: 2193)

Data processing: software development, installation, and managem

Software program development tool

Testing or debugging

C717S124000

Reexamination Certificate

active

07146605

ABSTRACT:
A method for verifying software source code that includes references to program variables includes processing the source code to derive a set of next-state functions representing control flow of the source code. The references to the program variables in the source code are replaced with non-deterministic choices in the next-state functions. The next-state functions including the non-deterministic choices are restricted to produce a finite-state model of the control flow. The finite-state model is then verified to find an error in the source code.

REFERENCES:
patent: 5394347 (1995-02-01), Kita et al.
patent: 5481717 (1996-01-01), Gaboury
patent: 5721926 (1998-02-01), Tamura
patent: 6209120 (2001-03-01), Kurshan et al.
patent: 6505342 (2003-01-01), Hartmann et al.
patent: 6694290 (2004-02-01), Apfelbaum et al.
patent: 6820256 (2004-11-01), Fleehart et al.
patent: 6853963 (2005-02-01), Apfelbaum et al.
patent: 2005/0204341 (2005-09-01), Broussard
Cousot et al. “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints” 1977, 4th ACM Symp. Principles of Programing Languages, p. 238-252.
Martens et al. “Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance” 1995, ICLP 95.
Anderson et al. “Model Checking Large Software Specifications” Oct. 1996 SIGSOFT'96, p. 156-166.
Dwyer et al. “Model Checking Graphical User Interfaces Using Abstractions” 1997, 5th AMC SIGSOFT, p. 244-261.
Wing et al. “Model Checking Software Systems: A Case Study” 1995, SIGSOFT '95, p. 128-139.
Jackson “Abstract Model Checking of Infinite Specifications” 1994, Lecture Notes on Computer Science vol. 873, p. 519-531.
Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proc. CAV'00, LNCS 1855, pp. 232-247. Springer, 2000.
Bouajjani, Esparza, Maler “Reachability Analysis of Pushdown Automata: Application to Model-Checking”; Lecture Notes In Computer Science; vol. 1243, 1997.
Esparza, Kucera, Schwoon “Model-Checking LTL with Regular Valuations for Pushdown Systems” Lecture Notes In Computer Science; vol. 2215, 2001.
C. Eisner, “Model Checking SMV”, IBM Haifa Research Laboratory, Matam Advanced Technology Center.
Clarke et al., “Model Checking”, Chapter 1, MIT Press (1999) pp. 4-6.
Beer et al., “RulesBase: an Industry-Oriented Formal Verification Tool”, Proceedings of the Design Automation Conference DAC'96 Las Vegas, Nevada 6 pages, (1996).
Beer et al., “The Temporal Logic Sugar”, Proceedings of the Thirteenth International Conference on Computers Aided Verification 13 Pages, (2001).
Beer et al., “On-The-Fly Model Checking of RCTL Formulas”, Proceedings of the Tenth International Conference on Computer Aided Verification 11 Pages, (2001).
Corbett et al., “Bandera: Extracting Finite-State Models from Java Source Code”, Proceedings of the 22ndInternational Conference of Software Engineering, 10 Pages (2000).
Holzmann, “Logic Verification of ANSI-C code with SPIN”, Proceedings of the Seventh International SPIN workshop, p. 224, (2000).
Havelund et al., “Model Checking Java Programs Using Java Pathfinder”, International Journal for Software Tools for Technology Transfer 17 Pages, (2000).
Esparza et al., “Efficient Algorithms for Model Checking Pushdown Systems”, Published in Proceedings of Twelfth International Conference on Computer Aided Verification, 16 Pages, (2000).
Demartini et al., “Modeling and Validation of Java Multithreading Application using SPIN”, Published in Proceedings of the Fourth International SPIN Workshop 15 Pages, (1998).
Holzmann et al., “Software Modeling Checking: Extracting Verification Models from Source Code”, Published in Proceedings of PSTV/FORTE99, 18 Pages, (1999).
McMillan, “Symbolic Model Checking”, Kluwer Academic Publishers, Chapter 2, 3, pp. 11-30, (1993).
Eisner, Cindy, “Model Checking the Garbage Collection Mechanism of SMV”, Electronic Notes in Theoretical Computer Science. (2001) 55(3):1-15. <URL: http//www.elserver.nl/locate/entcs/volume55.html>.

Affiliated with

Also associated with

Rating

Automatic abstraction of software source does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Automatic abstraction of software source, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic abstraction of software source will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3704367