{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T04:05:33Z","timestamp":1782878733290,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540442356","type":"print"},{"value":"9783540457893","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45789-5_28","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T09:50:10Z","timestamp":1186825810000},"page":"395-410","source":"Crossref","is-referenced-by-count":8,"title":["Refinement of LTL Formulas for Abstract Model Checking"],"prefix":"10.1007","author":[{"given":"Mar\u03afa del Mar","family":"Gallardo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ernesto","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,9,5]]},"reference":[{"key":"28_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer-Aided Verification CAV\u201998","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, S. Owre, Computing abstractions of infinite state systems compositionally and automatically. In Computer-Aided Verification CAV\u201998, LNCS-1427, pp. 319\u2013331, (1998)."},{"key":"28_CR2","unstructured":"E.M. Clarke, O. Grumberg, D. Peled. Model Checking (The MIT Press, 2000)."},{"issue":"2","key":"28_CR3","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E. A. Emerson, A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. on Programming Languages and Systems, 8(2) (1986) 244\u2013263.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"5","key":"28_CR4","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, D.E. Long. Model Checking and Abstraction. ACM Transaction on Languages and Systems, 16(5) (1994) 1512\u20131245.","journal-title":"ACM Transaction on Languages and Systems"},{"key":"28_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer-Aided Verification CAV\u201900","author":"E.M. Clarke","year":"2000","unstructured":"E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-guided abstraction refinement. In Computer-Aided Verification CAV\u201900, LNCS-1855, pp. 154\u2013169, (2000)."},{"key":"28_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/3-540-60360-3_32","volume-title":"Proceedings of Static Analysis Symposium","author":"R. Cleveland","year":"1995","unstructured":"R. Cleveland, P. Iyer, D. Yankelevich. Optimality in Abstractions of Model Checking. In Proceedings of Static Analysis Symposium LNCS-983, pp. 51\u201363, (1995)"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcliff, L. Shawn, C. Pasareanu, H. Zheng. Bandera: Extracting Finite-State Models from Java Source Code. In Proc. 22nd Int. Conf. On Software Engineering, pp. 439\u2013448, (2000).","DOI":"10.1145\/337180.337234"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot, R. Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conf. Record of the 4th ACM Symp. on Princ. of Prog. Languages, pp. 238\u2013252, (1977).","DOI":"10.1145\/512950.512973"},{"key":"28_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"P. Cousot, R. Cousot. Refining Model Checking by Abstract Interpretation. Automated Software Engineering\n                        6 (1999) 69\u201395.","journal-title":"Automated Software Engineering"},{"issue":"2","key":"28_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, R. Gerth, O. Grumberg. Abstract Interpretation of Reactive Systems. ACM Trans. on Programming Languages and Systems, 19(2) (1997) 253\u2013291.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-48234-2_15","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"M.M. Gallardo","year":"1999","unstructured":"M.M. Gallardo, P. Merino. A Framework for Automatic Construction of Abstract PROMELA Models. In Theoretical and Practical Aspects of SPIN Model Checking, LNCS-1680, pp. 184\u2013199, (1999)."},{"key":"28_CR12","unstructured":"M.M. Gallardo, P. Merino, E. Pimentel. Verifying Abstract LTL Properties on Concurrent Systems. In Proc. of the 6th World Conference on Integrated Design & Process Technology, (2002)."},{"key":"28_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/3-540-46017-9_24","volume-title":"Proc. of the 9th International SPIN Workshop on Model Checking of Software","author":"M. M. Gallardo","year":"2002","unstructured":"M. M. Gallardo, J. Mart\u03afnez, P. Merino, E. Pimentel. \u03b1SPIN: Extending SPIN with Abstraction. In Proc. of the 9th International SPIN Workshop on Model Checking of Software, LNCS 2318, pp. 254\u2013258, (2002)."},{"issue":"2","key":"28_CR14","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"R. Giacobazzi, F. Ranzato, F. Scozzari. Making abstract interpretation complete. In Journal of ACM, 47(2) (2000), 361\u2013416.","journal-title":"Journal of ACM"},{"key":"28_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"The 8th International Static Analysis Symposium SAS\u201901","author":"R. Giacobazzi","year":"2001","unstructured":"R. Giacobazzi, E. Quintarelli. Incompleteness, Counterexamples and Refinement in Abstract Model-Checking. In The 8th International Static Analysis Symposium SAS\u201901, LNCS 2126, pp. 356\u2013373, (2001)."},{"key":"28_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-58179-0_55","volume-title":"Computer Aided Verification CAV\u201994","author":"S. Graf","year":"1994","unstructured":"S. Graf. Verification of a distributed Cache Memory by using abstractions. In Computer Aided Verification CAV\u201994, LNCS-818, pp. 207\u2013219, (1994)."},{"key":"28_CR17","unstructured":"G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991."},{"issue":"5","key":"28_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering\n                        23(5) (1997) 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"28_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Boujjani, S. Bensalem. Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design\n                        6 (1995) 1\u201335.","journal-title":"Formal Methods in System Design"},{"key":"28_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems-Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, New York, (1992)."},{"key":"28_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/3-540-45319-9_20","volume-title":"Proc. of 7th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001","author":"C.S. Pasareanu","year":"2001","unstructured":"C.S. Pasareanu, M.B. Dwyer, W. Visser. Finding Feasible Counter-examples when Model Checking Abstracted Java Programs. In Proc. of 7th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, LNCS-2031, pp. 284\u2013298, (2001)."},{"key":"28_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer-Aided Verification CAV\u201999","author":"H. Sa\u00eddi","year":"1999","unstructured":"H. Sa\u00eddi, N. Shankar. Abstract and model check while you prove. In Computer-Aided Verification CAV\u201999 LNCS-1633, pp. 443\u2013454, (1999)."},{"key":"28_CR23","series-title":"Lect Notes Comput Sci","first-page":"377","volume-title":"Seventh Internationa Static Analysis Symposium (SAS\u201900)","author":"H. Sam\u00eddi","year":"2000","unstructured":"H. Sam\u00eddi. Model Checking guided abstraction and analysis. In Seventh Internationa Static Analysis Symposium (SAS\u201900), LNCS-1824, pp. 377\u2013396, (2000)."},{"key":"28_CR24","unstructured":"\u03b1Spin project. University of M\u00e1laga. \n                  http:\/\/www.lcc.uma.es~gisum\/fmse\/tools\n                  \n                ."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45789-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T13:03:28Z","timestamp":1550754208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45789-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442356","9783540457893"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45789-5_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}