Data processing: software development – installation – and managem – Software program development tool – Code generation
Reexamination Certificate
2006-06-06
2006-06-06
Dam, Tuan (Department: 2192)
Data processing: software development, installation, and managem
Software program development tool
Code generation
C717S104000, C717S131000, C717S136000
Reexamination Certificate
active
07058925
ABSTRACT:
Described is a method that enables the automatic generation of a boolean program that is a predicate abstraction of a program written using a general programming language. The method is capable of abstracting code statements within the program that include procedure calls, assignments, goto statements, conditionals, and pointers. In accordance with the invention, predicates of interest are identified for each code statement in the program. For each particular code statement, the process generates predicate statements that describe an effect that the statement has on the predicates of interest. If the effect of a particular code statement is indeterminable, non-deterministic predicate statements are included in the boolean program to model the indeterminable nature of the code statement. In addition, if a particular code statement includes a procedure call, the arguments and return value of the procedure call are translated to associated predicates in the calling context.
REFERENCES:
“Checking Temporal Properties of Software with Boolean Programs”, by Thomas Ball and Sriram K. Rajamani, “Proceedings of the Workshop on Advances in Verification”, Jul., 2000.
P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model For Static Analysis of Programs By Construction or Approximation of Fixpoints”, POPL, Principles of Programming Languages, p. 238-252, ACM, 1977.
S. Graf and H. saidi, “Construction of Abstract State Graphs with PVS”, CAV 97, Computer-aided Verification, LNCS 1254, pp. 72-83, Jun. 22-25, 1997.
B. Pell, E. Gat, R. Keesing, N. Muscettola, and B. Smith, “Plan Execution For Autonomous Spacecraft”, In Proceedings of the International Joint Conference on Aritficial Intelligence, pp. 1233-1239, Aug. 1997.
W. Chan, R. Anderson, P. Bearne, D. Jones, D. Notkin, and W. Warner, “Decoupling Synchronization from Local Control for Efficient Symbolic Model Checking of Statecharts”, Proceedings of the 21st International Conference on Software Engineering, pp. 142-151, May 16-22, 1999.
H. Saidi, “Modular and Incremental Analysis of Concurrent Software Systems”, In Proceedings of the 14th IEEE International Conference on Automated Software Engineering, pp. 92-101, Oct. 1999.
W. Visser, SeungJoon Park, and John Penix, “Using Predicate Abstraction To Reduce Object-Oriented Programs For Model Checking”, FMSP 2000, The Third Woorkshop on Formal Methods in Software Practice, pp. 3-12, Aug. 24-25, 2000.
Guillaume Brat, Klaus Havelund, SeungJoon Park, and Willem Visser, “Model Checking Programs”, In Proceedings of the 15th IEEE International Automated Software Engineering Conference, pp. 3-11, Sep. 2000.
T. Ball, A. Podelski, and S.K. Rajamani, “Boolean and Cartesian Abstractions for Model Checking C Programs”, In TACAS 2001, Tools and Algorithms for Construction and Analysis of Systems, LNCS, 268-283, Apr. 2-6, 2001.
M. Dwyer, J. Hatcliff, R. Joehanes, S. Lauback, C. Pasareanu, Robby, W. Visser, and H. Zheng, “Tool-supported Program Abstraction for Finite-state Verification”, In ICSE 2001, Software Engineering, pp. 177-187, May 12-19, 2001.
T. Ball, T. Millstein, and S. Rajamani, “Polymorphic Predicate Abstraction”, Technical Report, MSR Technical Report-2001-10, Jun. 17, 2002.
Ball Thomas J.
Majumdar Rupak
Millstein Todd D.
Rajamani Sriram K.
Chow Chih-Ching
Dam Tuan
Merchant & Gould P,C,
Microsoft Corporation
LandOfFree
System and method for generating a predicate abstraction 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 generating a predicate abstraction of..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System and method for generating a predicate abstraction of... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3673793