{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:11:30Z","timestamp":1794381090689,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540227915","type":"print"},{"value":"9783540278641","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27864-1_23","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T12:35:37Z","timestamp":1284640537000},"page":"312-327","source":"Crossref","is-referenced-by-count":36,"title":["The Octahedron Abstract Domain"],"prefix":"10.1007","author":[{"given":"Robert","family":"Claris\u00f3","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jordi","family":"Cortadella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"issue":"8","key":"23_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Claris\u00f3, R., Cortadella, J.: Verification of timed circuits with symbolic delays. In: Proc. of Asia and South Pacific Design Automation Conference, pp. 628\u2013633 (2004)","DOI":"10.1109\/ASPDAC.2004.1337668"},{"key":"23_CR5","first-page":"238","volume-title":"Proc. of the ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the ACM Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"23_CR6","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/512760.512770","volume-title":"Proc. of the ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of the ACM Symposium on Principles of Programming Languages, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/781131.781149","volume-title":"Proceedings of the ACM SIGPLAN 2003 conference on Programming lan guage design and implementation","author":"N. Dor","year":"2003","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Proceedings of the ACM SIGPLAN 2003 conference on Programming lan guage design and implementation, pp. 155\u2013167. ACM Press, New York (2003)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, M., Rasse, A.: Data structures for the verification of timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 346\u2013360. Springer, Heidelberg (1997)"},{"issue":"2\/3","key":"23_CR10","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M. Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.-Y.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design\u00a010(2\/3), 149\u2013169 (1997)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Formal Methods in System Design"},{"key":"23_CR12","unstructured":"Henzinger, T.A.: The Temporal Specification and Verification of Real-Time Systems. PhD thesis, Stanford University (August 1991)"},{"key":"23_CR13","unstructured":"Mauras, C.: Symbolic simulation of interpreted automata. In: 3rd Workshop on Synchronous Programming (December 1996)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Minato, S.: Zero-supressed BDDs for set manipulation in combinatorial problems. In: Proc. ACM\/IEEE Design Automation Conference, pp. 272\u2013277 (1993)","DOI":"10.1145\/157485.164890"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"key":"23_CR16","first-page":"310","volume-title":"Analysis, Slicing and Tranformation (in Working Conference on Reverse Engineering)","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Analysis, Slicing and Tranformation (in Working Conference on Reverse Engineering), October 2001, pp. 310\u2013319. IEEE CS Press, Los Alamitos (2001)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, J., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: Computer Science Logic, The IT University of Copenhagen, Denmark (1999)","DOI":"10.1007\/3-540-48168-0_9"},{"issue":"3","key":"23_CR18","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1109\/TAC.1977.1101509","volume":"22","author":"T. Murata","year":"1977","unstructured":"Murata, T.: State equation, controllability and maximal matchings of Petri nets. IEEE Transactions on Automatic Control\u00a0 AC-22(3), 412\u2013416 (1977)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"23_CR19","unstructured":"New Polka: Convex Polyhedra Library, http:\/\/www.irisa.fr\/prive\/bjeannet\/newpolka.html"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Piguet, C., et al.: Memory element of the Master-Slave latch type, constructed by CMOS technology. US Patent 5,748,522 (1998)","DOI":"10.1016\/S0958-2118(98)90297-X"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proc. International Conf. Computer-Aided Design (ICCAD), pp. 42\u201347 (1993)","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/3-540-45013-0_7","volume-title":"Logic Based Program Synthesis and Transformation","author":"A. Simon","year":"2003","unstructured":"Simon, A., King, A., Howe, J.M.: Two Variables per Linear Inequality as an Abstract Domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664, pp. 71\u201389. Springer, Heidelberg (2003)"},{"key":"23_CR23","unstructured":"Somenzi, F.: CUDD: Colorado university decision diagram package, Available online at http:\/\/vlsi.colorado.edu\/~fabio\/CUDD"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-27813-9_23","volume-title":"Computer Aided Verification","author":"F. Wang","year":"2004","unstructured":"Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like datastructures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 295\u2013307. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27864-1_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:24:42Z","timestamp":1605741882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27864-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540227915","9783540278641"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27864-1_23","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b99688","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}