Data flow analysis for checking properties of concurrent Java programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Data flow analysis for checking properties of concurrent Java programs

Full text

Pdf (1.43 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 21st international conference on Software engineering table of contents

Los Angeles, California, United States

Pages: 399 - 410

Year of Publication: 1999

ISBN:1-58113-074-0

Authors

Gleb Naumovich	University of Massachusetts, Department of Computer Science, Amherst, MA
George S. Avrunin	University of Massachusetts, Department of Mathematics and Statistics, Amherst, MA
Lori A. Clarke	University of Massachusetts, Department of Computer Science, Amherst, MA

Sponsors

IEEE-CS : Computer Society
IEEE-CS\TCSE : TC on Software Engineering
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGSOFT: ACM Special Interest Group on Software Engineering
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 39, Citation Count: 21

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	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/302405.302663 What is a DOI?

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	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 [doi>10.1109/32.310668]
	2	James C. Corbett, Constructing compact models of concurrent Java programs, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.1-10, March 02-04, 1998, Clearwater Beach, Florida, United States
	3	James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
	4	C. Demartini , R. Sisto, Static Analysis of Java Multithreaded and Distributed Applications, Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, p.215, April 20-21, 1998
	5	Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
	6	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 [doi>10.1145/263699.263717]
	7	D. Helmbold and D. Luckham. Debugging Ada tasking programs. IEEE Software, 2(2):47-57, March 1985.
	8	Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	9	William Landi , Barbara G. Ryder, Pointer-induced aliasing: a problem taxonomy, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-103, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99599]
	10	T. J. Marlowe , B. G. Ryder, Properties of data flow frameworks: a unified model, Acta Informatica, v.28 n.2, p.121-163, Dec. 1990 [doi>10.1007/BF01237234]
	11	S. P Masticola and B. G. Ryder. Static infinite wait anomaly detection in polynomial time. In D. A. Padua, editor, Proceedings of the 1990 International Conference on Parallel Processing. Volume 2: Software, pages 78-87, Urbana-Champaign, IL, Aug. 1990. Pennsylvania State University Press.
	12	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	13	Gleb Naumovich , George S. Avrunin, A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.24-34, November 01-05, 1998, Lake Buena Vista, Florida, United States
	14	G. Naumovich , G. S. Avruin , L. A. Clarke, Data Flow Analysis for Checking Properties of Concurrent Java Programs, University of Massachusetts, Amherst, MA, 1998
	15	G. Naumovich , G. Avrunin , L. Clarke, An Efficient Algorithm for Computing MHP Information for Concurrent Java Programs, University of Massachusetts, Amherst, MA, 1998
	16	Gleb Naumovich , Lori A. Clarke , Leon J. Osterweil, Efficient composite data flow analysis applied to concurrent programs, Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.51-58, June 16-16, 1998, Montreal, Quebec, Canada
	17	John Plevyak , Andrew A. Chien, Precise concrete type inference for object-oriented languages, Proceedings of the ninth annual conference on Object-oriented programming systems, language, and applications, p.324-340, October 23-28, 1994, Portland, Oregon, United States
	18	John H. Reif , Scott A. Smolka, Data flow analysis of distributed communicating processes, International Journal of Parallel Programming, v.19 n.1, p.1-30, Feb. 1990 [doi>10.1007/BF01407862]
	19	R. N. Taylor and L. J. Osterweil. Anomaly detection in concurrent software by static data Aow analysis. IEEE Transactions on Software Engineering, 6(3):265-278, May 1980.

CITED BY 21

	Gleb Naumovich , Lori A. Clarke , Jamieson M. Cobleigh, Using partial order techniques to improve performance of data flow analysis based verification, ACM SIGSOFT Software Engineering Notes, v.24 n.5, p.57-65, Sept. 1999
	Gleb Naumovich , George S. Avrunin , Lori A. Clarke, An efficient algorithm for computing MHP information for concurrent Java programs, ACM SIGSOFT Software Engineering Notes, v.24 n.6, p.338-354, Nov. 1999
	Jamieson M. Cobleigh , Lori A. Clarke , Leon J. Osterweil, The right algorithm at the right time: comparing data flow analysis algorithms for finite state verification, Proceedings of the 23rd International Conference on Software Engineering, p.37-46, May 12-19, 2001, Toronto, Ontario, Canada
	Dean F. Sutherland , Aaron Greenhouse , William L. Scherlis, The code of many colors: relating threads to code and shared state, ACM SIGSOFT Software Engineering Notes, v.28 n.1, January 2003
	Gleb Naumovich, Using the observer design pattern for implementation of data flow analyses, ACM SIGSOFT Software Engineering Notes, v.28 n.1, January 2003
	James C. Corbett, Using shape analysis to reduce finite-state models of concurrent Java programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.1, p.51-93, Jan. 2000
	William Visser , SeungJoon Park , John Penix, Using predicate abstraction to reduce object-oriented programs for model checking, Proceedings of the third workshop on Formal methods in software practice, p.3-182, August 2000, Portland, Oregon, United States
	Jamieson M. Cobleigh , Lori A. Clark , Leon J. Osterweil, Verifying properties of process definitions, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.96-101, Sept. 2000
	Premkumar T. Devanbu , Stuart Stubblebine, Software engineering for security: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.227-239, June 04-11, 2000, Limerick, Ireland
	Gleb Naumovich, A conservative algorithm for computing the flow of permissions in Java programs, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	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
	Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, ACM SIGPLAN Notices, v.36 n.3, p.27-40, March 2001
	Abhik Roychoudhury , Tulika Mitra, Specifying multithreaded Java semantics for program verification, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
	Dennis Brylow , Jens Palsberg, Deadline Analysis of Interrupt-Driven Software, IEEE Transactions on Software Engineering, v.30 n.10, p.634-655, October 2004
	Jianbin Tan , George S. Avrunin , Lori A. Clarke , Shlomo Zilberstein , Stefan Leue, Heuristic-guided counterexample search in FLAVERS, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	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
	S. Boroday , A. Petrenko , J. Singh , H. Hallal, Dynamic analysis of java applications for multithreaded antipatterns, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	Barbara Staudt Lerner, Verifying process models built using parameterized state machines, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
	Stephen J. Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008
	Jianbin Tan , George S. Avrunin , Lori A. Clarke, Heuristic-Based Model Refinement for FLAVERS, Proceedings of the 26th International Conference on Software Engineering, p.635-644, May 23-28, 2004