{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T21:15:11Z","timestamp":1672434911823},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T00:00:00Z","timestamp":1167350400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2007,4,11]]},"DOI":"10.1007\/s10703-006-0029-7","type":"journal-article","created":{"date-parts":[[2006,12,28]],"date-time":"2006-12-28T15:54:09Z","timestamp":1167321249000},"page":"249-273","source":"Crossref","is-referenced-by-count":5,"title":["An abstract interpretation toolkit for \u03bcCRL"],"prefix":"10.1007","volume":"30","author":[{"given":"Miguel Valero","family":"Espada","sequence":"first","affiliation":[]},{"given":"Jaco van de","family":"Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,12,29]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Ball T, Majumdar R, Millstein T, Rajamani SK (2001) Automatic predicate abstraction of C programs. In: Proceedings of Conference on Programming Language Design and Implementation (PLDI), ACM, pp 203\u2013213","DOI":"10.1145\/378795.378846"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2000) BeBop: a symbolic model checker for Boolean programs. In: Proceedings of SPIN model checking and software verification, LNCS, vol 1885, Springer, pp 113\u2013130","DOI":"10.1007\/10722468_7"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: Proceedings of SPIN model checking and software verification, LNCS, vol 2057. Springer, pp 103\u2013122","DOI":"10.1007\/3-540-45139-0_7"},{"key":"29_CR4","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"JA Bergstra","year":"1985","unstructured":"Bergstra JA, Klop JW (1985) Algebra of communicating processes with abstraction. Theor Comput Sci 37:77\u2013121","journal-title":"Theor Comput Sci"},{"key":"29_CR5","unstructured":"Blom S, Fokkink W, Groote JF, van Langevelde I, Lisser B, van de Pol JC (2001) \u03bcCRL: a toolset for analysing algebraic specifications. In: Proceedings of Computer Aided Verification (CAV), LNCS, vol 2102. Springer, pp 250\u2013254"},{"key":"29_CR6","unstructured":"Blom S, Groote JF, van Langevelde I, Lisser B, van de Pol JC (2003) New developments around the \u03bcCRL tool set. ENTCS 80"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Bruns G, Godefroid P (1999) Model checking partial state spaces with 3-valued temporal logics. In: Proceedings of Computer Aided Verification (CAV), LNCS, vol 1877. Springer, pp 274\u2013287","DOI":"10.1007\/3-540-48683-6_25"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Long DE (1992) Model checking and abstraction. J ACM, pp 343\u2013354","DOI":"10.1145\/143165.143235"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. J ACM 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"29_CR10","unstructured":"Dams D (1996) Abstract interpretation and partition refinement for model checking. PhD thesis, Eindhoven University of Technology"},{"key":"29_CR11","unstructured":"Dams D (2002) Abstraction in software model checking: principles and practice (tutorial overview and bibliography). In: Proceedings of SPIN model checking and software verification, LNCS, vol 2318, Springer, pp 14\u201321"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Dams D, Gerth R (2000) The bounded retransmission protocol revisited. ENTCS 9","DOI":"10.1016\/S1571-0661(05)80425-6"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Dams D, Hesse W, Holzmann G (2002) Abstracting C with abC. In: Proceedings of the Computer Aided Verification (CAV), LNCS, vol 2404, Springer, pp 515\u2013520","DOI":"10.1007\/3-540-45657-0_43"},{"key":"29_CR14","unstructured":"Long DE (1993) Model checking, abstraction, and compositional verification. PhD thesis, Carnegie Mellon University"},{"issue":"2\u20133","key":"29_CR15","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s10009-003-0122-9","volume":"5","author":"MM Gallardo","year":"2004","unstructured":"Gallardo MM, Mart\u00ednez J, Merino P, Pimentel E (2004) \u03b1SPIN: a tool for abstract model checking. Int J Softw Tools for Technol Transf (STTT) 5(2\u20133):165\u2013184","journal-title":"Int J Softw Tools for Technol Transf (STTT)"},{"key":"29_CR16","first-page":"13","volume":"4","author":"H Garavel","year":"2002","unstructured":"Garavel H, Lang F, Mateescu R (2002) An overview of CADP 2001. Eur Assoc Softw Sci Technol Newsl 4:13\u201324","journal-title":"Eur Assoc Softw Sci Technol Newsl"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid P, Huth M, Jagadeesan R (2001) Abstraction-based model checking using modal transition systems. In: Proceedings of the concurrency theory (CONCUR), LNCS, vol 2154, Springer, pp 426\u2013440","DOI":"10.1007\/3-540-44685-0_29"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Groote JF, van de Pol JC (1996) A bounded retransmission protocol for large data packets. In: Proceedings of the Algebraic Methodology and Software Technology (AMAST), LNCS, vol 1101. Springer, pp 536\u2013550","DOI":"10.1007\/BFb0014338"},{"key":"29_CR19","unstructured":"Groote JF, Ponse A (1994) The syntax and semantics of \u03bcCRL. In: Algebra of communicating processes, workshops in computing. pp 26\u201362"},{"issue":"1\u20132","key":"29_CR20","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S1567-8326(01)00005-4","volume":"48","author":"JF Groote","year":"2001","unstructured":"Groote JF, Ponse A, Usenko Y (2001) Linearization in parallel pCRL. J Logic Algebraic Programm 48(1\u20132):39\u201370","journal-title":"J Logic Algebraic Programm"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Hatcliff J, Dwyer M, Pasareanu C, Robby (2002) Foundations of the Bandera abstraction tools. In: Proceedings of the essence of computation, LNCS, vol 2566, Springer, pp 172\u2013203","DOI":"10.1007\/3-540-36377-7_9"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Havelund K, Skakkebaek J (1999) Applying model checking in Java verification. In: Proceedings of the SPIN model checking and software verification, LNCS, vol 1680, Springer, pp 216\u2013232","DOI":"10.1007\/3-540-48234-2_17"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Smith MH (1999) A practical method for verifying event-driven software. In: Proceedings of International Conference on Software Engineering (ICSE). ACM, pp 597\u2013607","DOI":"10.1145\/302405.302710"},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"Huth M, Jagadeesan R, Schmidt D (2001) Modal transition systems: a foundation for three-valued program analysis. In: Proceedings of the programming languages and systems (ESOP), LNCS, vol 2028, Springer, pp 155\u2013169","DOI":"10.1007\/3-540-45309-1_11"},{"key":"29_CR25","unstructured":"Jones ND, Nielson F (1995) Abstract interpretation: a semantics-based tool for program analysis. In: Handbook of logic in computer science. Oxford Science Publications, pp 527\u2013636"},{"key":"29_CR26","doi-asserted-by":"crossref","unstructured":"Kozen D (1982) Results on the propositional \u03bc-calculus. In: Proceedings of the International Conference on Automata, Languages and Programming (ICALP), LNCS, vol 140. Springer, pp 348\u2013359","DOI":"10.1007\/BFb0012782"},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"Kroening D, Groce A, Clarke EM (2004) Counterexample guided abstraction refinement via program execution. In: Proceedings of the international conference on formal engineering methods (ICFEM), LNCS, vol 3380. Springer, pp 224\u2013238","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"29_CR28","doi-asserted-by":"crossref","unstructured":"Larsen KG, Thomsen B (1988) A modal process logic. In: Proceedings of the logic in computer science (LICS). IEEE, pp 203\u2013210","DOI":"10.1109\/LICS.1988.5119"},{"key":"29_CR29","unstructured":"Manna Z, Colon M, Finkbeiner B, Sipma H, Uribe TE (1997) Abstraction and modular verification of infinite-state reactive systems. In: Proceedings of the requirements targeting software and systems engineering (RTSE), LNCS, vol 1526. Springer, pp 273\u2013292"},{"key":"29_CR30","unstructured":"Mateescu R (1998) Verification des proprietes temporelles des programmes paralleles. PhD thesis, Institut National Polytechnique de Grenoble"},{"key":"29_CR31","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1090\/S0002-9947-1944-0010555-7","volume":"55","author":"O Ore","year":"1944","unstructured":"Ore O (1944) Galois connexions. Trans. Am Math Soc 55:493\u2013513","journal-title":"Trans. Am Math Soc"},{"key":"29_CR32","first-page":"35","volume":"128","author":"S Orzan","year":"2005","unstructured":"Orzan S, van de Pol JC, Valero Espada M (2005) A state space distribution policy based on abstract interpretation. ENTCS 128:35\u201345","journal-title":"ENTCS"},{"key":"29_CR33","unstructured":"van de Pol JC (2001) A prover for the \u03bcCRL toolset with applications. Technical Report SEN-R0106, CWI"},{"key":"29_CR34","doi-asserted-by":"crossref","unstructured":"van de Pol JC, Valero Espada M (2004) Modal abstraction in \u03bcCRL. In: Proceedings of the Algebraic Methodology and Software Technology (AMAST), LNCS, vol 3116, Springer, pp 409\u2013425","DOI":"10.1007\/978-3-540-27815-3_32"},{"key":"29_CR35","doi-asserted-by":"crossref","unstructured":"Schmidt D (2002) Structure-preserving binary relations for program abstraction. In: Proceedings of the essence of computation, LNCS, vol 2566, Springer, pp 245\u2013268","DOI":"10.1007\/3-540-36377-7_12"},{"key":"29_CR36","unstructured":"Usenko Y (2002) Linearization in \u03bcCRL. PhD thesis, Eindhoven University of Technology"},{"key":"29_CR37","unstructured":"Valero M (2005) Modal abstraction and replication of processes with data. PhD thesis, Free University Amsterdam"},{"key":"29_CR38","unstructured":"Willemse T (2003) Semantics and verification in process algebras with data and timing. PhD thesis, Eindhoven University of Technology"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0029-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0029-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0029-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:01:02Z","timestamp":1559239262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0029-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12,29]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,4,11]]}},"alternative-id":["29"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0029-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12,29]]}}}