A general-purpose algorithm for analyzing concurrent programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A general-purpose algorithm for analyzing concurrent programs

Full text

Pdf (1.61 MB)

Source

Communications of the ACM archive
Volume 26 , Issue 5 (May 1983) table of contents

Pages: 361 - 376

Year of Publication: 1983

ISSN:0001-0782

Author

Richard N. Taylor

Univ. of California, Irvine

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 60, Citation Count: 97

Additional Information:

abstract references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/69586.69587 What is a DOI?

ABSTRACT

Developing and verifying concurrent programs presents several problems. A static analysis algorithm is presented here that addresses the following problems: how processes are synchronized, what determines when programs are run in parallel, and how errors are detected in the synchronization structure. Though the research focuses on Ada, the results can be applied to other concurrent programming languages such as CSP.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
	2	Per Brinch Hansen, Distributed processes: a concurrent programming concept, Communications of the ACM, v.21 n.11, p.934-941, Nov. 1978 [doi>10.1145/359642.359651]
	3	Buxton, J. N., and Stanning, V. Requirements for Ada programming support environments: "Stoneman." Department of Defense, Feb. 1980.
	4	Gallucci, Michael A. SAM/SAL User Manual and Report. University of Colorado Technical Report #CU-CS-198-81, Department of Computer Science, Feb. 1981.
	5	Matthew S. Hecht, Flow Analysis of Computer Programs, Elsevier Science Inc., New York, NY, 1977
	6	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	7	Howden, W. E. Symbolic Testing and the DISSECT symbolic evaluation system. IEEE Trans. Software Engineering, SE-3, 4 (July 1977), 266-278.
	8	Ichbiah, J. D., Krieg-Bmeckner, B., Wichmann, B. A., Ledgard, H. F., and Heliard, J. Reference manual for the Ada programming language: Proposed standard document. Report AD-A090 709/7, Department of Defense, July 198o.
	9	Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
	10	Donald E. Knuth, The art of computer programming, volume 3: (2nd ed.) sorting and searching, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1998
	11	Martin, F. HAL/S-The avionics programming system for shuttle. Proc. AIAA Conference on Computers in Aerospace. Los Angeles, CA (November 1977}, 308-318.
	12	Osterweil, L. J., and Fosdick, L. D. DAVE--A validation, error detection, and documentation system for Fortran programs. Soflware---Prac0ce and Experience, 6 (1976), 473--486.
	13	Taylor, R. N., and Osterweil, L. J, Anomaly detection in concurrent soitware by static data flow analysis. IEEE Tmns SoJtware Engineering, SE-6, 3 (May 1980), 265-278.
	14	Taylor, R. N. Complexity of Analyzing Concurrent Programs. Department of Computer Science Technical Report #DC.S-9-IR, University of Victoria (May, 1981).

CITED BY 97

	B. Shenker , T. Murata , S. M. Shatz, Use of Petri net invariants to detect static deadlocks in Ada programs, Proceedings of 1986 ACM Fall joint computer conference, p.1072-1081, November 1986, Dallas, Texas, United States
	John Mellor-Crummey, Compile-time support for efficient data race detection in shared-memory parallel programs, ACM SIGPLAN Notices, v.28 n.12, p.129-139, Dec. 1993
	D. Callahan , K. Kennedy , J. Subhlok, Analysis of event synchronization in a parallel programming tool, ACM SIGPLAN Notices, v.25 n.3, p.21-30, Mar. 1990
	Kaizhi Yue, Generating interesting scenarios from system descriptions, Proceedings of the 1st international conference on Industrial and engineering applications of artificial intelligence and expert systems, p.212-218, June 1988, Tullahoma, Tennessee, United States
	Matthew B. Dwyer , Lori A. Clarke , Kari A. Nies, A compact Petri net representation for concurrent programs, Proceedings of the 17th international conference on Software engineering, p.147-157, April 24-28, 1995, Seattle, Washington, United States
	W. E. Howden , G. M. Shi, Linear and structural event sequence analysis, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.98-106, May 1996
	William A. Josephson , James W. Armitage, Analysis tools for Ada concurrency designs, Proceedings of the seventh Washington Ada symposium on Ada, p.189-204, July 1990, McLean, Virginia, United States
	Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada
	Shing Chi Cheung , J. Kramer, Tractable Dataflow Analysis for Distributed Systems, IEEE Transactions on Software Engineering, v.20 n.8, p.579-593, August 1994
	David Callahan , Jaspal Sublok, Static analysis of low-level synchronization, ACM SIGPLAN Notices, v.24 n.1, p.100-111, Jan. 1989
	Tor E. Jeremiassen , Susan J. Eggers, Static Analysis of Barrier Synchronization in Explicitly Parallel Programs, Proceedings of the IFIP WG10.3 Working Conference on Parallel Architectures and Compilation Techniques, p.171-180, August 24-26, 1994
	Anneliese von Mayrhauser , Shao-Ming Simon Hsueh, An Ada deadlock testing algorithm based on control and communication flow graphs, Proceedings of the conference on TRI-Ada '92, p.450-457, November 16-20, 1992, Orlando, Florida, United States
	Shing Chi Cheung , Jeff Kramer, Checking safety properties using compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.1, p.49-78, Jan. 1999
	John Mellor-Crummey, On-the-fly detection of data races for programs with nested fork-join parallelism, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.24-33, November 18-22, 1991, Albuquerque, New Mexico, United States
	Sridhar Iyer , S. Ramesh, Apportioning: A Technique for Efficient Reachability Analysis of Concurrent Object-Oriented Programs, IEEE Transactions on Software Engineering, v.27 n.11, p.1037-1056, November 2001
	Douglas Long , Lori A. Clarke, Data flow analysis of concurrent systems that use the rendezvous model of synchronization, Proceedings of the symposium on Testing, analysis, and verification, p.21-35, October 08-10, 1991, Victoria, British Columbia, Canada
	M. Young , R. Taylor , K. Forester , D. Brodbeck, Integrated concurrency analysis in a software development enviornment, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.200-209, Dec. 1989
	S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Using state space reduction methods for deadlock analysis in Ada tasking, ACM SIGSOFT Software Engineering Notes, v.18 n.3, p.51-60, July 1993
	Shing C. Cheung , Jeff Kramer, Checking subsystem safety properties in compositional reachability analysis, Proceedings of the 18th international conference on Software engineering, p.144-154, March 25-29, 1996, Berlin, Germany
	Peter Ladkin , Barbara Simons, Compile-time analysis of communicating processes, Proceedings of the 6th international conference on Supercomputing, p.248-259, July 19-24, 1992, Washington, D. C., United States
	Eric Y. T. Juan , Jeffrey J. P. Tsai , Tadao Murata, Compositional verification of concurrent systems using Petri-net-based condensation rules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.5, p.917-979, Sept. 1998
	Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France
	K. Olender , L. Osterweil, Cesar: a static sequencing constraint analyzer, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.66-74, Dec. 1989
	A. T. Chamillard , Lori A. Clarke, Improving the accuracy of Petri net-based analysis of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.24-38, May 1996
	S. C. Cheung , J. Kramer, Enhancing compositional reachability analysis with context constraints, ACM SIGSOFT Software Engineering Notes, v.18 n.5, p.115-125, Dec. 1993
	Shing Chi Cheung , Jeff Kramer, Context constraints for compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.334-377, Oct. 1996
	Stephen P. Masticola , Barbara G. Ryder, Non-concurrency analysis, ACM SIGPLAN Notices, v.28 n.7, p.129-138, July 1993
	Suresh K. Damodaran-Kamal , Joan M. Francioni, Testing races in parallel programs with an OtOt strategy, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.216-227, August 17-19, 1994, Seattle, Washington, United States
	Michal Young , Richard N. Taylor , David L. Levine , Kari A. Nies , Debra Brodbeck, A concurrency analysis tool suite for Ada programs: rationale, design, and preliminary experience, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.1, p.65-106, Jan. 1995
	Mauro Pezzè , Richard N. Taylor , Michal Young, Graph models for reachability analysis of concurrent programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.171-213, April 1995
	Kurt M. Olender , Leon J. Osterweil, Interprocedural static analysis of sequencing constraints, ACM Transactions on Software Engineering and Methodology (TOSEM), v.1 n.1, p.21-52, Jan. 1992
	Jingde Cheng, Task-wait-for graphs and their application to handling tasking deadlocks, Proceedings of the conference on TRI-ADA '90, p.376-390, December 03-06, 1990, Baltimore, Maryland, United States
	Thomas A. Standish , Richard N. Taylor, Arcturus: A prototype advanced Ada@@@@ programming environment, ACM SIGPLAN Notices, v.19 n.5, p.57-64, May 1984
	Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.124-133, March 1998
	S. C. Cheung , J. Kramer, An integrated method for effective behaviour analysis of distributed systems, Proceedings of the 16th international conference on Software engineering, p.309-320, May 16-21, 1994, Sorrento, Italy
	E. W. Giering, III , T. P. Baker, Compile time scheduling of an Ada subset, Proceedings of the seventh Washington Ada symposium on Ada, p.143-155, July 1990, McLean, Virginia, United States
	Régis Cridlig, Semantic analysis of shared-memory concurrent languages using abstract model-checking, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.214-225, June 21-23, 1995, La Jolla, California, United States
	Stephen P. Masticola , Barbara G. Ryder, A model of Ada programs for static deadlock detection in polynomial times, ACM SIGPLAN Notices, v.26 n.12, p.97-107, Dec. 1991
	Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, ACM SIGPLAN Notices, v.33 n.5, p.345-357, May 1998
	Carol H. LeDoux , D. Stott Parker, Jr., Saving traces for Ada debugging, ACM SIGAda Ada Letters, v.V n.2, p.97-108, Sep., Oct. 1985
	Jong-Deok Choi , Sang Lyul Min, Race Frontier: reproducing data races in parallel-program debugging, ACM SIGPLAN Notices, v.26 n.7, p.145-154, July 1991
	Wuxu Peng , S. Puroshothaman, Data flow analysis of communicating finite state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.3, p.399-442, July 1991
	Charles E. McDowell , David P. Helmbold, Debugging concurrent programs, ACM Computing Surveys (CSUR), v.21 n.4, p.593-622, Dec. 1989
	D. Q. M. Fay, Experiences using Inmos proto-OCCAM (TM), ACM SIGPLAN Notices, v.19 n.9, p.5-11, September 1984
	Sang L. Min , Jong-Deok Choi, An efficient cache-based access anomaly detection scheme, ACM SIGARCH Computer Architecture News, v.19 n.2, p.235-244, Apr. 1991
	Rajiv Gupta , Mary Lou Soffa, SHAPE: a highly adaptable and parallel system, Proceedings of the 1986 ACM fourteenth annual conference on Computer science, p.107-114, February 1986, Cincinnati, Ohio, United States
	Simona Bernardi , Susanna Donatelli , José Merseguer, From UML sequence diagrams and statecharts to analysable petri net models, Proceedings of the 3rd international workshop on Software and performance, July 24-26, 2002, Rome, Italy
	Vasanth Balasundaram , Ken Kennedy, Compile-time detection of race conditions in a parallel program, Proceedings of the 3rd international conference on Supercomputing, p.175-185, June 05-09, 1989, Crete, Greece
	Laura K. Dillon , George S. Avrunin , Jack C. Wileden, Constrained expressions: toward broad applicability of analysis methods for distributed software systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.374-402, July 1988
	Sarita V. Adve , Mark D. Hill , Barton P. Miller , Robert H. B. Netzer, Detecting data races on weak memory systems, ACM SIGARCH Computer Architecture News, v.19 n.3, p.234-243, May 1991
	D. Schonberg, On-the-fly detection of access anomalies, ACM SIGPLAN Notices, v.24 n.7, p.285-297, July 1989
	William F. Appelbe , Charles E. McDowell, Integrating tools for debugging and developing multitasking programs, ACM SIGPLAN Notices, v.24 n.1, p.78-88, Jan. 1989
	George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985
	Kourosh Gharachorloo , Phillip B. Gibbons, Detecting violations of sequential consistency, Proceedings of the third annual ACM symposium on Parallel algorithms and architectures, p.316-326, July 21-24, 1991, Hilton Head, South Carolina, United States
	Radu Rugina , Martin C. Rinard, Pointer analysis for structured parallel programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.1, p.70-116, January 2003
	Bill Appelbe , Kevin Smith , Charlie McDowell, Start/Pat: A Parallel-Programming Toolkit, IEEE Software, v.6 n.4, p.29-38, July 1989
	Ahmed Bouajjani , Javier Esparza , Tayssir Touili, A generic approach to the static analysis of concurrent programs with procedures, ACM SIGPLAN Notices, v.38 n.1, p.62-73, January 2003
	Satish Chandra , Patrice Godefroid , Christopher Palm, Software model checking in practice: an industrial case study, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Leon J. Osterweil, Understanding process and the quest for deeper questions in software engineering research, ACM SIGSOFT Software Engineering Notes, v.28 n.5, p.6-14, September 2003
	W. Peng , S. Purushothaman, Towards dataflow analysis of communicating finite state machines, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.45-58, June 1989, Edmonton, Alberta, Canada
	Miguel Felder , Carlo Ghezzi , Mauro Pezzè, Analyzing refinements of state based specifications: the case of TB nets, ACM SIGSOFT Software Engineering Notes, v.18 n.3, p.28-39, July 1993
	Evelyn Duesterwald , Mary Lou Soffa, Concurrency analysis in the presence of procedures using a data-flow framework, Proceedings of the symposium on Testing, analysis, and verification, p.36-48, October 08-10, 1991, Victoria, British Columbia, Canada
	Douglas L. Long , Lori A. Clarke , Joseph Fialli, Ada language considerations for concurrency analysis, Proceedings of the sixth Washington Ada symposium on Ada, p.75-80, July 1989, McLean, Virginia, United States
	Alexander Aiken , David Gay, Barrier inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.342-354, January 19-21, 1998, San Diego, California, United States
	Christoph von Praun , Thomas R. Gross, Static conflict analysis for multi-threaded object-oriented programs, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Douglas L. Long , Lori A. Clarke, Task interaction graphs for concurrency analysis, Proceedings of the 11th international conference on Software engineering, p.44-52, May 1989, Pittsburgh, Pennsylvania, United States
	Sudharsan R. Iyengar , Narayan C. Debnath, A general abstract representation for the study of concurrent programs, Proceedings of the 1993 ACM conference on Computer science, p.131-136, February 16-18, 1993, Indianapolis, Indiana, United States
	Michael Young , Richard N. Taylor, Rethinking the taxonomy of fault detection techniques, Proceedings of the 11th international conference on Software engineering, p.53-62, May 1989, Pittsburgh, Pennsylvania, United States
	S. M. Shatz , K. Mai , C. Black , S. Tu, Design and Implementation of a Petri Net Based Toolkit for Ada Tasking Analysis, IEEE Transactions on Parallel and Distributed Systems, v.1 n.4, p.424-441, October 1990
	S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Application and experimental evaluation of state space reduction methods for deadlock analysis in Ada, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.340-380, Oct. 1994
	Jyh-Herng Chow , William Ludwell Harrison, III, Compile-time analysis of parallel programs that share memory, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 19-22, 1992, Albuquerque, New Mexico, United States
	Richard N. Taylor , Thomas A. Standish, Steps to an advanced ada programming environment, Proceedings of the 7th international conference on Software engineering, p.116-125, March 26-29, 1984, Orlando, Florida, United States
	H. Zedan, Safety decomposition of distributed programs, ACM SIGPLAN Notices, v.20 n.8, August 1985
	M. Young , R. M. Taylor, Combining Static Concurrency Analysis with Symbolic Execution, IEEE Transactions on Software Engineering, v.14 n.10, p.1499-1511, October 1988
	George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991
	Edith Schonberg, On-the-fly detection of access anomalies, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Gerald M. Karam , Raymond J. A. Buhr, Temporal Logic-Based Deadlock Analysis for Ada, IEEE Transactions on Software Engineering, v.17 n.10, p.1109-1125, October 1991
	Richard N. Taylor , David L. Levine , Cheryl D. Kelly, Structural Testing of Concurrent Programs, IEEE Transactions on Software Engineering, v.18 n.3, p.206-215, March 1992
	Leo Yuhsiang Liu , R. K. Shyamasundar, Static Analysis of Real-Time Distributed Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.373-388, April 1990
	Sol M. Shatz , Shengru Tu , Tadao Murata , Sastry Duri, An Application of Petri Net Reduction for Ada Tasking Deadlock Analysis, IEEE Transactions on Parallel and Distributed Systems, v.7 n.12, p.1307-1322, December 1996
	Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004
	James C. Corbett, Timing Analysis of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.22 n.7, p.461-483, July 1996
	Anne R. Brindle , Richard N. Taylor , David F. Martin, A Debugger for Ada Tasking, IEEE Transactions on Software Engineering, v.15 n.3, p.293-304, March 1989
	M. Notomi , T. Murata, Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis, IEEE Transactions on Software Engineering, v.20 n.5, p.325-336, May 1994
	Radu Rugina , Martin C. Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.185-235, March 2005
	G. M. Karam , R. J. A. Buhr, Starvation and Critical Race Analyzers for Ada, IEEE Transactions on Software Engineering, v.16 n.8, p.829-843, August 1990
	William E. Howden, Comments Analysis and Programming Errors, IEEE Transactions on Software Engineering, v.16 n.1, p.72-81, January 1990
	Tadao Murata , Sol M. Shatz , Boris Shenker, Detection of Ada Static Deadlocks Using Petri Net Invariants, IEEE Transactions on Software Engineering, v.15 n.3, p.314-326, March 1989
	Scotte Zinn , Michael Coffin, Efficient event generation for detecting races, Proceedings of the 1993 conference of the Centre for Advanced Studies on Collaborative research: software engineering, October 24-28, 1993, Toronto, Ontario, Canada
	Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
	Matthew B. Dwyer , Lori A. Clarke, A Compact Petri Net Representation and Its Implications for Analysis, IEEE Transactions on Software Engineering, v.22 n.11, p.794-811, November 1996
	Jingde Cheng, A survey of tasking deadlock detection methods, ACM SIGAda Ada Letters, v.XI n.1, p.82-91, Jan./Feb. 1991
	Harry Koehnemann , Timothy Lindquist, Towards target-level testing and debugging tools for embedded software, Proceedings of the conference on TRI-Ada '93, p.288-298, September 18-23, 1993, Seattle, Washington, United States
	Cherri M. Pancake , Sue Utter, A bibliography of parallel debuggers, 1990 edition, ACM SIGPLAN Notices, v.26 n.1, p.21-37, Jan. 1991
	Yu Lei , Richard H. Carver, Reachability Testing of Concurrent Programs, IEEE Transactions on Software Engineering, v.32 n.6, p.382-403, June 2006
	Sharon Simmons , Dennis Edwards , Phil Kearns, Communication analysis of distributed programs, Scientific Programming, v.14 n.2, p.151-170, April 2006
	Zuohua Ding , Kao Zhang , Jueliang Hu, A rigorous approach towards test case generation, Information Sciences: an International Journal, v.178 n.21, p.4057-4079, November, 2008

INDEX TERMS

Primary Classification:
D. Software
D.2 SOFTWARE ENGINEERING

Additional Classification:
D. Software
D.2 SOFTWARE ENGINEERING
D.3 PROGRAMMING LANGUAGES
D.3.2 Language Classifications

Nouns: Ada
D.3.3 Language Constructs and Features
Subjects: Concurrent programming structures

F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Documentation, Languages, Verification

REVIEW

"Jorgen Staunstrup : Reviewer"

This paper outlines an algorithm for a static analysis of the concurrency aspects of Ada programs. It is proposed that dynamic properties (e.g., posssible synchronizations) are verified by a static analysis which yields all potential behaviors. more...

Collaborative Colleagues:

Richard N. Taylor: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player