Matthew B. Dwyer
Lori A. Clarke
- ABC+91.G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, and J.C. Wileden. Automated anal-ysis of concurrent systems with the con-strained expression t oolset. IEEE Transac-tions on Sojhoae Engineering, 17(11):1204- 1222, November 1991. Google Scholar
Digital Library
- And91.G.R. Andrews. Paradigms for process interaction in distributed programs. ACM Computing Surveys, 23(1):49-90, mar 1991. Google ScholarDigital Library
- BCM+90.J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking : 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428-439, 1990.Google ScholarCross Ref
- CK93.S.C. Cheung and J. Kramer. Tractable flow analysis for anomaly detection in distributed programs. In Proceedings of the European Softwa?'e Engineering Conference, 1993. Google ScholarDigital Library
- Cor94.J. C. Corbett. An empirical evaluation of three methods for deadlock analysis of Ada tasking programs. SoftwaTe Engznee?'zng Notes, pages 204-2 15, August 1994. Proceedings of the International Symposium on Software Testing and Analysis. Google ScholarDigital Library
- DBDS93.S. Duri, U. Buy, R. Devarapalli, and S.M. Shatz. Using state space methods for deadlock analysis in Ada tasking. SoftwaTe Engineering Notes, 18(3):51-60, July 1993. Proceedings of the International Symposium on Software Testing and Analysis. Google ScholarDigital Library
- DC94.M.B. Dwyer and L.A. Clarke. Data flow analysis for verifying properties of concurrent programs. Soft waTe Engineering Notes, 19(5):62-75, December 1994. Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering. Google ScholarDigital Library
- DS91.E. Duesterwald and M. L. Soffa. Concurrency analysis in the presence of procedures using a data flow framework. In Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis and Verification, Victoria, Canada, October 1991. Google ScholarDigital Library
- For91.K. Forester. TIG-based Petri nets for modeling Ada tasking. Master's thesis, University of Massachusetts, Amherst, MA, June 1991.Google Scholar
- GW91.P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of the Third WoTkshop on Computer Aided Verification, pages 417-428, July 1991. Google ScholarDigital Library
- LC89.D.L. Long and L.A. Clarke. Task interaction graphs for concurrency analysis. In Proceedings of the 1 lth International Conference on SoftwaTe Engineering, pages 44-52, Pittsburgh, May 1989. Google ScholarDigital Library
- MR87.E.T. Morgan and R.R. Razouk. Interac-tive state-space analysis of concurrent sys-tems. IEEE Transactions of Software Engineering, 13(10):1080-1091, 1987. Google ScholarDigital Library
- MR91.S.P. Masticola and B.G. Ryder. A model of Ada programs for static deadlock detection in polynomial time. In Proceedings of Workshop on Parallel and Distributed Debugging. ACM, May 1991. Google ScholarDigital Library
- Mur89.T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(44):541-580, April 1989.Google ScholarCross Ref
- MZGT85.D. Mandrioli, R. Zicari, C. IGhezzi, and F. Tisato. Modeling the Ada task system by Petri nets. ComputeT Languages, lo(l):43- 61, 1985. Google ScholarDigital Library
- PTY92.M. Pezz&, R.N. Taylor, and M. Young. Graph models for reachability analysis of concurrent programs. Techmlical Report TR-92-27, Department of Information and Computer Science, University of California, Irvine, January 1992.Google Scholar
- Sha93.S.M. Shatz. Personal Communication, February 1993.Google Scholar
- SMBT90.S.M. Shatz, K. Mai, C. Black,, and S. Tu. Design and implementation of a Petri net based toolkit for Ada tasking analysis. IEEE Transactions on PaTallel and Distributed System, 1(4):424-441, October 1990. Google ScholarDigital Library
- ST+94.S.M. Shatz, S. Tu, , T. Murata, and S. Duri. Theory and application of Petri net re-duction for Ada tasking deadlock analysis. Technical report, Department of Electrical Engineering and Computer Science, Univer-sit y of Illinois, Chicago, 1994.Google Scholar
- Tay83.R.N. Taylor. A general-purpose algorithm for analyzing concurrent programs. Communications of the A CM, 26(5) :3162-376, May 1983. Google ScholarDigital Library
- YTL+92.M. Young, R.N. Taylor, D.L. Levine, K. Forester, and D. Brodbeck. A concurrency analysis tool suite: Raticmale, design, and preliminary experience. Technical Report TR-128-P, SERC, Purdue University, October 1992.Google Scholar
- YY91.W.J. Yeh and M. Young. Compositional reachability analysis using process algebra. In Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis and Verification,pages 49-59, Victoria, Cimada, October 1991. Google ScholarDigital Library
Index Terms
- A compact Petri net representation for concurrent programs
Recommendations
Verification of Concurrent Programs Using Petri Net Unfoldings
Verification, Model Checking, and Abstract InterpretationAbstractGiven a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be ...
Comments