Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Software program
Reexamination Certificate
2003-12-19
2009-06-30
Shah, Kamini S (Department: 2128)
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Software program
Reexamination Certificate
active
07555418
ABSTRACT:
Procedure summaries can be generated and used for multithreaded software. A set of actions for a software procedure can be identified as atomically modelable with respect to multithreaded execution of the software. Such actions can be considered a transaction and deemed to have occurred one after another without interruption by other threads. Thus, multithreaded execution of the software can be modeled to detect programming flaws. For example, reachability analysis can be used in concert with the procedure summaries to determine if specified invariants fail.
REFERENCES:
patent: 6546443 (2003-04-01), Kakivaya et al.
patent: 2002/0166032 (2002-11-01), Qadeer
patent: 2002/0178401 (2002-11-01), Ball et al.
patent: 2003/0204570 (2003-10-01), Rehof et al.
patent: 2003/0204641 (2003-10-01), Rehof et al.
patent: 2003/0204834 (2003-10-01), Ball et al.
Tyrrell et al. “CSP Methods for Identifying Atomic Actions in the Design of Fault Tolerant Concurrent Systems” IEEE 1995.
Reps et al. “Precise Interprocedural Dataflow Analysis via Graph Reachability”, 1995 ACM.
Alur et al., “Modular Refinement of Hierarchic Machines,”In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pp. 390-402, 2000.
Ball et al., “Parameterized Verification of Multithreaded Software Libraries,”In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 2031, pp. 158-173, Springer-Verlag, 2001.
Ball et al., “Bebop: A Symbolic Model Checker for Boolean Programs,”In SPIN 00: SPIN Workshop, SPIN Model Checking and Software Verification, Lecture Notes in Computer Science, vol. 1885, pp. 113-130, Springer-Verlag, 2000.
Bouajjani et al., “A Generic Approach to the Static Analysis of Concurrent Programs with Procedures,”Annual Symposium on Principles of Programming Languages Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 62-73, ACM Press, Jan. 2003.
Das et al., “ESP: Path-Sensitive Program Verification in Polynomial Time,”In Proceedings of the ACM SIGPLAN, 12 pages; 2002.
Delzanno et al., “Towards the Automated Verification of Multithreaded Java Programs,”International Conference on Tools and Algorithms for Construction and Analysis of Systems, Grenoble, France, 16 pages, 2002.
Duesterwald et al., “Concurrency Analysis in the Presence of Procedures Using Data-Flow Framework,”International Symposium on Software Testing and Analysis, Proceedings of the Symposium Testing, Analysis, and Verification, pp. 36-48, 1991.
Dwyer et al., “Data Flow Analysis for Verifying Properties of Concurrent Programs,”In Proceedings of the ACM SIGSOFT Symposium on foundations of Software Engineering, pp. 62-75, Dec. 1994.
Esparza et al., “Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs,”Annual Symposium on Principles of Programming Languages, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1-11, 2000.
Esparza, “A BDD-based Model Checker for Recursive Programs,”In CAV'01, Proceedings of the 13th International Conference on Computer Aided Verification, pp. 324-336, 2001.
Flanagan et al., “Thread-Modular Model Checking,”Model Checking Software: 10th International SPIN Worskop, Lecture Notes in Computer Science, vol. 2648; pp. 213-225, Springer-Verlag, May 2003.
Flanagan et al., “Transactions for Software Model Checking,”Electronic Notes in Theoretical Computer Science, vol. 89, No. 3, 22 pages, Sep. 2003.
Flanagan et al., “A Type and Effect System for Atomicity,”Conference on Programming Language Design and Implementation, Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 338-349, ACM, Jun. 2003.
Flanagan et al., “Types for Atomicity,”Types In Languages Design And Implementation, Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 1-12, ACM, Jan. 2003.
Henzinger et al., “Decomposing, Refinement Proofs Using Assume-Guarantee Reasoning,”Proceedings of the IEEE/ACM International Conference on Computer-aided Design(ICCAD 2000), pp. 245-252, 2000.
Lipton, “Reduction: A Method of Proving Properties of Parallel Programs,”Communications of the ACM, vol. 18, No. 12, pp. 717-721, Dec. 1975.
Ramalingam, “Research Report: Context-Sensitive Synchronization-Sensitive Analysis Undecidable,”ACM Transactions on Programming Languages and Systems, vol. 22, No. 2, pp. 416-430, Mar. 2000.
Reps et al., “Precise Interprocedural Dataflow Analysis via Graph Reachability,”In Conference Record of the 22nd Annual Symposium on Principles of Programming Languages(POPL'95), pp. 49-61, ACM, 1995.
Rinard, “Analysis of Multithreaded Programs,”In SAS 01: Static Analysis, Lecture Notes in Computer Science, vol. 2126, pp. 1-19, Springer-Verlag, 2001.
U.S. Appl. No. 60/450,982, filed Feb. 28, 2003, Rehof et al.
U.S. Appl. No. 10/659,221, filed Dec. 10, 2003, Rehof et al.
Flanagan et al., “Thread-Modular Verification for Shared-Memory Programs,” HP Labs Technical Reports, SRC Technical Note 2001-003, Compaq Computer Corporation, 20 pages, Nov. 19, 2001.
Flanagan et al., “Thread-Modular Verification for Shared-Memory Programs,” Lecture Notes in Computer Science, Proceedings of the 11thEuropean Symposium on Programming Languages and Systems, Springer-Verlag, London, UK, 15 pages, Apr. 2002.
Freund et al., “Checking Concise Specifications for Multithreaded Software,” Williams College Technical Note 01-2002, 16 pages, Dec. 2002.
Freund et al., “Checking Concise Specifications for Multithreaded Software,” FTfJP'2003, Proceedings of the Fifth ECOOP Workshop on Formal Techniques for Java-like Programs, Darmstadt, Germany, 10 pages, Jul. 21, 2003.
Freund et al., “Checking Concise Specifications for Multithreaded Software,” Williams College Technical Note 01-2002 (revised Dec. 2003), 18 pages, Dec. 12, 2003.
Larsen, et al., “Bisimulation Through Probabilistic Testing (Preliminary Report),” Proceedings of the 16th ACM SIGPLAN-AIGACT Symposium on Principles of Programming Languages, pp. 344-352, 1989.
Per Cederqvist et al., “Version Management with CVS (for CVS 1.11.10),” 184 pages, Dec. 4, 2003.
Sharir et al., “Two Approaches to Interprocedural Data Flow Analysis,”Program Flow Analysis: Theory and Applications, Prentice-Hall, Inc., pp. 189-233, 1981.
Steffen and Burkart, “Composition, Decomposition and Model Checking of Pushdown Processes,”Nordic Journal of Computing, vol. 2, pp. 89-125, 1995.
Whaley et al., “Compositional Pointer and Escape Analysis for Java Programs,” Proceedings of the 14thACM SIGPLAN, Conference on Object-Oriented Programming, Systems, Languages, and Applications, Denver, Colorado, ACM Press, New York, NY, pp. 187-206, 1999.
Flanagan et al., “Thread-Modular Verification for Shared-Memory Programs,” HP Labs Technical Reports, SRC Technical Note 2001-003, Compaq Computer Corportion, 20 pages, Nov. 19, 2001.
Flanagan et al., “Thread-Modular Verification for Shared-Memory Programs,” Lecture Notes in Computer Science, Proceedings of the 11thEuropean Symposium on Programming Languages and Systems, Springer-Verlag, London, UK, 15 pages, Apr. 2002.
Freund et al., “Checking Concise Specifications for Multithreaded Software,” Williams College Technical Note Jan. 2002, 16 pages, Dec. 2002.
Freund et al., “Checking Concise Specifications for Multithreaded Software,” FTfJP'2003, Proceedings of the Fifth ECOOP Workshop on Formal Techniques for Java-like Programs, Darmstadt, Germany, 10 pages, Jul. 21, 2003.
Freund et al., “Checking Concise Specifications for Multithreaded Soft
Qadeer Shaz
Rajamani Sriram K.
Rehof Niels Jakob
Alhija Saif A
Klarquist & Sparkman, LLP
Microsoft Corporation
Shah Kamini S
LandOfFree
Procedure summaries for multithreaded software does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Procedure summaries for multithreaded software, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Procedure summaries for multithreaded software will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-4086231