{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:48:55Z","timestamp":1760586535389},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213147"},{"type":"electronic","value":"9783540247326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_7","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"92-108","source":"Crossref","is-referenced-by-count":24,"title":["Minimization of Counterexamples in SPIN"],"prefix":"10.1007","author":[{"given":"Paul","family":"Gastin","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Moro","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Zeitoun","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2001)"},{"key":"7_CR2","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)"},{"issue":"5","key":"7_CR3","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"7_CR4","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms. McGraw-Hill Higher Education, New York (2001)"},{"key":"#cr-split#-7_CR5.1","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Computer-aided verification 1990, DIMACS Ser. Discrete Math. Theoret. Comput. Sci, New Brunswick, NJ. vol.\u00a03, pp. 207\u2013218 (1990);","DOI":"10.1090\/dimacs\/003\/15"},{"key":"#cr-split#-7_CR5.2","unstructured":"Amer. Math. Soc., Providence, RI (1991)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"7_CR7","first-page":"58","volume-title":"Proc. of POPL 2002","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of POPL 2002, pp. 58\u201370. ACM Press, New York (2002)"},{"issue":"5","key":"7_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997); Special issue on Formal Methods in Software Practice","journal-title":"IEEE Trans. on Software Engineering"},{"key":"7_CR9","volume-title":"The SPIN model-checker","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN model-checker. Addison-Wesley, Reading (2003)"},{"key":"7_CR10","first-page":"23","volume-title":"Proc. Second SPIN Workshop","author":"G. Holzmann","year":"1996","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. Second SPIN Workshop, Rutgers, Piscataway, NJ, pp. 23\u201332. American Mathematical Society, Providence (1996)"},{"key":"7_CR11","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, pp. 332\u2013344, Cambridge (June 1986)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:29:36Z","timestamp":1559330976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}