{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T14:43:51Z","timestamp":1649083431708},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1995,12,1]],"date-time":"1995-12-01T00:00:00Z","timestamp":817776000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Software Eng"],"published-print":{"date-parts":[[1995,12]]},"DOI":"10.1007\/bf00871802","type":"journal-article","created":{"date-parts":[[2004,12,24]],"date-time":"2004-12-24T15:31:20Z","timestamp":1103902280000},"page":"265-309","source":"Crossref","is-referenced-by-count":0,"title":["A specification-based approach to concurrency analysis"],"prefix":"10.1007","volume":"2","author":[{"given":"Ugo","family":"Buy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Moll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"11","key":"CR1","doi-asserted-by":"crossref","first-page":"1204","DOI":"10.1109\/32.106975","volume":"17","author":"G.S. Avrunin","year":"1991","unstructured":"Avrunin, G.S., Buy, U.A., Corbett, J.C., Dillon, L.K., and Wileden, J.C. 1991. Automated analysis of concurrent systems with the constrained expression toolset.IEEE Trans. Softw. Eng., 17(11):1204?1222.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"CR2","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1109\/TSE.1986.6312944","volume":"12","author":"G.S. Avrunin","year":"1986","unstructured":"Avrunin, G.S., Dillon, L.K., Wileden, J.C., and Riddle, W.E. 1986. Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems.IEEE Trans. Softw. Eng., 12(2):278?292.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"CR3","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E. 1992. Symbolic boolean manipulation with ordered binary-decision diagrams.ACM Comput. Surv., 24(3):293?318.","journal-title":"ACM Comput. Surv."},{"key":"CR4","volume-title":"Automatic Synthesis of Resource Sharing Concurrent Programs","author":"U. Buy","year":"1990","unstructured":"Buy, U. 1990.Automatic Synthesis of Resource Sharing Concurrent Programs. PhD Thesis, University of Massachusetts, Amherst, Massachusetts."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Buy, U.A. and Moll, R. 1991a. Liveness analysis and the automatic generation of concurrent programs. In E.M. Clarke and R.P. Kurshan (Eds.),Computer-Aided Verification'90, DIMACS 3, pp. 535?550, American Mathematical Society.","DOI":"10.1090\/dimacs\/003\/33"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Buy, U.A. and Moll, R. 1991b. A proof lattice-based technique for analyzing liveness of resource controllers. In E.M. Clarke and R.P. Kurshan (Eds.),Computer-Aided Verification: 2nd Internat. Conf., CAV'90, LNCS 531, pp. 292?301, Springer-Verlag.","DOI":"10.1007\/BFb0023743"},{"issue":"4","key":"CR7","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1145\/63334.63337","volume":"32","author":"N. Carriero","year":"1989","unstructured":"Carriero, N. and Gelernter, D. 1989. Linda in context.Commun. ACM, 32(4):445?458.","journal-title":"Commun. ACM"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M. and Emerson, E.A. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. InProceedings of the Workshop on Logics of Programs, LNCS 131, pp. 52?71, Springer-Verlag.","DOI":"10.1007\/BFb0025774"},{"issue":"2","key":"CR9","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., and Sistla, A.P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Trans. Prog. Lang. Syst., 8(2):244?263.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"CR10","unstructured":"Cormen, T.H., Leiserson, C.E., and Rivest, R.L. 1990.Introduction to Algorithms. MIT Press\/McGraw-Hill."},{"key":"CR11","unstructured":"Desai, A. 1993. A specification based approach to concurrency analysis. Master's Thesis, University of Illinois at Chicago."},{"key":"CR12","series-title":"Technical Report","volume-title":"Cooperating sequential processes","author":"E.W. Dijkstra","year":"1965","unstructured":"Dijkstra, E.W. 1965. Cooperating sequential processes. Technical Report EWD-123, Technological University, Eindhoven, The Netherlands."},{"issue":"8","key":"CR13","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W. 1975. Guarded commands, nondeterminacy and formal derivation of programs.Commun. ACM, 18(8):453?457.","journal-title":"Commun. ACM"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Duri, S., Buy, U., Devarapalli, R., and Shatz, S.M. 1993. Using state space reduction methods for deadlock analysis in Ada tasking. InProc. 1993 Internat. Sympos. on Software Testing and Analysis, pp. 51?60, ACM.","DOI":"10.1145\/174146.154197"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A. and Lei, C.-L. 1987. Modalities for model checking: Branching time logic strikes back.Science of Computer Programming, 8:275?306.","journal-title":"Science of Computer Programming"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(81)90113-4","volume":"13","author":"H.J. Genrich","year":"1981","unstructured":"Genrich, H.J. and Lautenbach, K. 1981. System modelling with high-level Petri nets.Theoretical Computer Science 13, 13:109?136.","journal-title":"Theoretical Computer Science 13"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P. and Wolper, P. 1992. Using partial orders for the efficient verification of deadlock freedom and safety properties. In K.G. Larsen and A. Skou (Eds.),Computer-Aided Verification: 3rd Internat. Conf., CAV'91, LNCS 575, pp. 332?342, Springer-Verlag.","DOI":"10.1007\/3-540-55179-4_32"},{"issue":"4","key":"CR18","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., and Trakhtenbrot, M. 1990. STATEMATE: a working environment for development of complex reactive systems.IEEE Trans. Softw. Eng., 16(4):403?414.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"CR19","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1109\/MS.1985.230351","volume":"2","author":"D. Helmbold","year":"1985","unstructured":"Helmbold, D. and Luckham, D. 1985. Debugging Ada tasking programs.IEEE Software, 2(2):47?57.","journal-title":"IEEE Software"},{"key":"CR20","unstructured":"Hoare, C.A.R. 1985.Communicating Sequential Processes. Prentice-Hall International."},{"key":"CR21","unstructured":"Holzmann, G.J. 1991.Design and Validation of Computer Protocols. Prentice-Hall Software Series."},{"issue":"8","key":"CR22","doi-asserted-by":"crossref","first-page":"829","DOI":"10.1109\/32.57622","volume":"16","author":"G.M. Karam","year":"1990","unstructured":"Karam, G.M. and Buhr, R.J. 1990. Starvation and critical race analyzers for Ada.IEEE Trans. Softw. Eng., 16(8):829?843.","journal-title":"IEEE Trans. Softw. Eng."},{"key":"CR23","unstructured":"Long, D.L. and Clarke, L.A. 1989. Task interaction graphs for concurrency analysis. InProceedings of the 11th International Conference on Software Engineering. Pittsburgh, PA, pp. 44?52."},{"issue":"1","key":"CR24","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna, Z. and Wolper, P. 1984. Synthesis of communicating processes from temporal logic specifications.ACM Trans. Prog. Lang. Syst., 6(1):68?93.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"CR25","unstructured":"McDowell, C.E. 1989. A practical algorithm for static analysis of parallel programs.Journal of Parallel and Distributed Processing, pp. 515?536."},{"key":"CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L. 1993.Symbolic Model Checking. Boston, Massachusetts: Kluwer Academic Publishers."},{"key":"CR27","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R. 1989.Communication and Concurrency. Englewood Cliffs, New Jersey: Prentice-Hall."},{"issue":"10","key":"CR28","doi-asserted-by":"crossref","first-page":"1080","DOI":"10.1109\/TSE.1987.232850","volume":"13","author":"E.T. Morgan","year":"1987","unstructured":"Morgan, E.T. and Razouk, R.R. 1987. Interactive state-space analysis of concurrent systems.IEEE Trans. Softw. Eng., 13(10):1080?1091.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"CR29","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1109\/32.21759","volume":"15","author":"T. Murata","year":"1989","unstructured":"Murata, T., Shenker, B., and Shatz, S.M. 1989. Detection of Ada static deadlocks using Petri net invariants.IEEE Trans. Softw. Eng., 15(3):314?326.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"CR30","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"Owicki, S. and Lamport, L. 1982. Proving liveness properties of concurrent programs.ACM Trans. Prog. Lang. Syst., 4(3):455?495.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A. 1977. The temporal logic of programs. InProceedings 18th Annual Symposium on Foundations of Computer Science, pp. 46?57.","DOI":"10.1109\/SFCS.1977.32"},{"issue":"8","key":"CR32","doi-asserted-by":"crossref","first-page":"774","DOI":"10.1109\/TSE.1985.232526","volume":"11","author":"K. Ramamritham","year":"1985","unstructured":"Ramamritham, K. 1985. Synthesizing code for resource controllers.IEEE Trans. Softw. Eng., 11(8):774?783.","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"CR33","doi-asserted-by":"crossref","first-page":"722","DOI":"10.1109\/TSE.1983.235435","volume":"9","author":"K. Ramamritham","year":"1983","unstructured":"Ramamritham, K. and Keller, R.M. 1983. Specification of synchronizing processes.IEEE Trans. Softw. Eng., 9(6):722?733.","journal-title":"IEEE Trans. Softw. Eng."},{"key":"CR34","unstructured":"Ramamritham, K. and Sundarrajan, P. 1983. Automatic generation of code for resource controller tasks in Ada. InProceedings of the IEEE Symposium on Application and Assessment of Automated Tools for Software Development, pp. 133?142."},{"key":"CR35","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0304-3975(88)90049-7","volume":"20","author":"A.W. Roscoe","year":"1988","unstructured":"Roscoe, A.W. and Hoare, C.A.R. 1988. The laws of Occam programming.Theoretical Computer Science, 20:177?229.","journal-title":"Theoretical Computer Science"},{"key":"CR36","first-page":"293","volume":"8","author":"P.H. Starke","year":"1991","unstructured":"Starke, P.H. 1991. Reachability analysis of Petri nets using symmetries.Syst. Anal. Model. Simul., 8:293?303.","journal-title":"Syst. Anal. Model. Simul."},{"issue":"5","key":"CR37","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/69586.69587","volume":"26","author":"R.N. Taylor","year":"1983","unstructured":"Taylor, R.N. 1983. A general-purpose algorithm for analyzing concurrent programs.Commun. ACM, 26(5):362?376.","journal-title":"Commun. ACM"},{"key":"CR38","doi-asserted-by":"crossref","unstructured":"Tu, S., Shatz, S.M., and Murata, T. 1990. Applying Petri net reduction to support Ada-tasking deadlock analysis. InProc. Eleventh Internat. Conference on Distributed Computing Systems, Paris, France, pp. 96?103.","DOI":"10.1109\/ICDCS.1990.89289"},{"key":"CR39","unstructured":"U.S. Department of Defense, Washington, D.C.Reference Manual for the Ada Programming Language, ANSI\/MIL-STD-1815A edition, Jan. 1983."},{"key":"CR40","doi-asserted-by":"crossref","unstructured":"Valmari, A. 1991. A stubborn attack on state explosion. In E.M. Clarke and R.P. Kurshan (Eds.),Computer-Aided Verification: 2nd Internat. Conf., CAV'90, LNCS 531, pp. 156?165, Springer-Verlag.","DOI":"10.1007\/BFb0023729"},{"issue":"10","key":"CR41","doi-asserted-by":"crossref","first-page":"1499","DOI":"10.1109\/32.6195","volume":"14","author":"M. Young","year":"1988","unstructured":"Young, M. and Taylor, R.N. 1988. Combining static concurrency analysis with symbolic execution.IEEE Trans. Softw. Eng., 14(10):1499?1511.","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00871802.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00871802\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00871802","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:06:08Z","timestamp":1586041568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00871802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["BF00871802"],"URL":"https:\/\/doi.org\/10.1007\/bf00871802","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}