{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T07:45:57Z","timestamp":1743752757623},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283096"},{"type":"electronic","value":"9783540319344"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11539452_38","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:54:50Z","timestamp":1127829290000},"page":"503-517","source":"Crossref","is-referenced-by-count":12,"title":["A Practical Application of Geometric Semantics to Static Analysis of Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Eric","family":"Goubault","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanuel","family":"Haucourt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"Fajstrup, L., Goubault, E., Haucourt, E., Raussen, M.: Components of the fundamental category. Applied Categorical Structures (2004)","DOI":"10.1023\/B:APCS.0000013812.75342.de"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.: Cooperating Sequential Processes. Academic Press, London (1968)","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"38_CR3","unstructured":"Nachbin, L.: Topology and Order. Van Nostrand, Princeton (1965)"},{"key":"38_CR4","volume-title":"Stone Spaces","author":"P.T. Johnstone","year":"1982","unstructured":"Johnstone, P.T.: Stone Spaces. Cambridge University Press, Cambridge (1982)"},{"key":"38_CR5","unstructured":"Fajstrup, L., Goubault, E., Raussen, M.: Algebraic topology and concurrency. Submitted to Theoretical Computer Science, also technical report, Aalborg University (1999)"},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"Goubault, E.: Some geometric perspectives in concurrency theory. Homology Homotopy and Applications (2003)","DOI":"10.4310\/HHA.2003.v5.n2.a5"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-45995-2_8","volume-title":"LATIN 2002: Theoretical Informatics","author":"E. Goubault","year":"2002","unstructured":"Goubault, E., Raussen, M.: Dihomotopy as a tool in state space analysis. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol.\u00a02286, pp. 16\u201337. Springer, Heidelberg (2002)"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"Gabriel, P., Zisman, M.: Calculus of fractions and homotopy theory. Ergebnisse der Mathematik und ihrer Grenzgebiete, vol.\u00a035. Springer, Heidelberg (1967)","DOI":"10.1007\/978-3-642-85844-4"},{"key":"38_CR9","unstructured":"Haucourt, E.: A framework for component categories. ENTCS (2005) (to appear)"},{"key":"38_CR10","doi-asserted-by":"crossref","unstructured":"Mac Lane, S.: Categories for the working mathematician. Springer, Heidelberg (1971)","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"38_CR11","unstructured":"Gaucher, P., Goubault, E.: Topological deformation of higher dimensional automata. Technical report, arXiv:math.AT\/010760, to appear in HHA (2001)"},{"key":"38_CR12","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1109\/32.538606","volume":"22","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P., Peled, D., Staskauskas, M.: Using partial-order methods in the formal validation of industrial concurrent programs. IEEE Transactions on Software Engineering\u00a022, 496\u2013507 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"38_CR13","first-page":"1","volume-title":"Formal Methods and System Design","author":"P. Godefroid","year":"1995","unstructured":"Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. In: Formal Methods and System Design, vol.\u00a07, pp. 1\u201315. Kluwer Academic Publishers, Dordrecht (1995)"},{"key":"38_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A. Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531. Springer, Heidelberg (1991)"},{"key":"38_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-51285-3_35","volume-title":"PARLE \u201989 - Parallel Architectures and Languages Europe","author":"A. Valmari","year":"1989","unstructured":"Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol.\u00a0366, pp. 89\u2013103. Springer, Heidelberg (1989)"},{"key":"38_CR16","volume-title":"Proc. of Computer Aided Verification","author":"S. Melzer","year":"1997","unstructured":"Melzer, S., Roemer, S.: Deadlock checking using net unfoldings. In: Proc. of Computer Aided Verification. Springer, Heidelberg (1997)"},{"key":"38_CR17","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: Basic notions of trace theory. Lecture notes for the REX summer school in temporal logic. Springer, Heidelberg (1988)","DOI":"10.1007\/BFb0013025"},{"key":"38_CR18","first-page":"238","volume":"4","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages\u00a04, 238\u2013252 (1977)","journal-title":"Principles of Programming Languages"},{"key":"38_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-60973-3_102","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"B. Boigelot","year":"1996","unstructured":"Boigelot, B., Godefroid, P.: Model checking in practice: An analysis of the access bus protocol using spin. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 465\u2013478. Springer, Heidelberg (1996)"},{"key":"38_CR20","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1109\/LICS.1990.113767","volume-title":"Proc. of the Fifth Annual IEEE Symposium on Logic and Computer Science","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proc. of the Fifth Annual IEEE Symposium on Logic and Computer Science, pp. 428\u2013439. IEEE Press, Los Alamitos (1990)"},{"key":"38_CR21","unstructured":"Garavel, H., Jorgensen, M., Mateescu, R., Pecheur, C., Sighireanu, M., Vivien, B.: Cadp 1997 \u2013 status, applications and perspectives. Technical report, Inria Alpes (1997)"},{"key":"38_CR22","unstructured":"Raussen, M.: Deadlocks and dihomotopy in mutual exclusion models. Technical report, Aalborg University (2005), Available at http:\/\/www.math.aau.dk\/index_en.html"},{"key":"38_CR23","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/9758.9759","volume":"9","author":"S. Carson","year":"1987","unstructured":"Carson, S., Reynolds, P.: The geometry of semaphore programs. ACM TOPLAS\u00a09, 25\u201353 (1987)","journal-title":"ACM TOPLAS"},{"key":"38_CR24","unstructured":"Gaucher, P.: A convenient category for the homotopy theory of concurrency preprint available at math. AT\/0201252 (2002)"},{"key":"38_CR25","unstructured":"Grandis, M.: Directed homotopy theory, I. the fundamental category. Cahiers Top. Gom. Diff. Catg, to appear, Preliminary version: Dip. Mat. Univ. Genova, Preprint 443 (2001)"},{"key":"38_CR26","volume-title":"Algebraic Topology","author":"E.J. Spanier","year":"1966","unstructured":"Spanier, E.J.: Algebraic Topology. McGraw-Hill, New York (1966)"},{"key":"38_CR27","doi-asserted-by":"crossref","unstructured":"Goubault, E.: Geometry and concurrency: A users\u2019 guide. Mathematical Structures in Computer Science (2000)","DOI":"10.1017\/S0960129500003133"},{"key":"38_CR28","unstructured":"Goubault, E.: Cubical sets are generalized transition systems. Technical report, pre-proceedings of CMCIM 2002 (2001), also available at http:\/\/www.di.ens.fr\/~goubault"},{"key":"38_CR29","doi-asserted-by":"crossref","unstructured":"Fahrenberg, U.: A category of higher-dimensional automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 187\u2013201. Springer, Heidelberg (2005) (to appear)","DOI":"10.1007\/978-3-540-31982-5_12"},{"key":"38_CR30","doi-asserted-by":"crossref","unstructured":"Boehm, H.: Bounding space usage of conservative garbage collector. In: Principles of Programing Language (2002), see http:\/\/www.hpl.hp.com\/personal\/Hans_Boehm\/gc\/","DOI":"10.1145\/503272.503282"},{"key":"38_CR31","volume-title":"SPIN Model Checker : The Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"38_CR32","unstructured":"Cousot, P., Cousot, R.: Comparison of the Galois connection and widening\/ narrowing approaches to abstract interpretation. In: JTASPEFL 1991, Bordeaux, BIGRE, vol. 74, pp. 107\u2013110 (1991)"},{"key":"38_CR33","unstructured":"Demartini, C., Iosif, R., Sisto, R.: Modeling and validation of java multithreading applications using spin. In: SPIN Workshop (1998)"},{"key":"38_CR34","series-title":"Lecture Notes in Computer Science","first-page":"417","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1992","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 417\u2013428. Springer, Heidelberg (1992)"},{"key":"38_CR35","unstructured":"Grandis, M.: The shape of a category up to directed homotopy. Technical Report preprint 509, Dip. Mat. Univ. Genova (2004), available at http:\/\/www.dima.unige.it\/~grandis\/rec.public_grandis.html"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2005 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11539452_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T22:43:29Z","timestamp":1586472209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11539452_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283096","9783540319344"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/11539452_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}