{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:47:15Z","timestamp":1743043635460,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642244421"},{"type":"electronic","value":"9783642244438"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24443-8_21","type":"book-chapter","created":{"date-parts":[[2011,10,6]],"date-time":"2011-10-06T04:34:12Z","timestamp":1317875652000},"page":"186-199","source":"Crossref","is-referenced-by-count":2,"title":["An Evolutionary Approach for Program Model Checking"],"prefix":"10.1007","author":[{"given":"Nassima","family":"Aleb","sequence":"first","affiliation":[]},{"given":"Zahia","family":"Tamen","sequence":"additional","affiliation":[]},{"given":"Nadjet","family":"Kamel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","first-page":"1","volume-title":"Proc. POPL","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM, New York (2002)"},{"key":"21_CR2","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking of C. Tech.Rep.MSR-TR-2001-21, Microsoft Research (2002)"},{"issue":"6","key":"21_CR3","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng.\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR4","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":"2000","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 (2000)"},{"key":"21_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumber, O., Peled, D.: Model Checking. MIT, Cambridge (1999)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SatAbs: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"21_CR7","first-page":"439","volume-title":"Proc. ICSE","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Pasareanu, C., Robby, L.S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. ICSE, pp. 439\u2013448. ACM, New York (2000)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A Unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principales of Programming Languages, POPL 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR9","volume-title":"A discipline of programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A discipline of programming. Prentice Hall, Englewood Cliffs (1976)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumda, R.: The software model cheker Blast. Int. J. Softw. Tools Technol. Transfer (2007)","DOI":"10.1007\/s10009-007-0044-z"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11691372_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2006","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 489\u2013503. Springer, Heidelberg (2006)"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/263699.263717","volume-title":"Proc. POPL","author":"P. Godefroid","year":"1997","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. POPL, pp. 174\u2013186. ACM, New York (1997)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"4","key":"21_CR14","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. STTT\u00a02(4), 366\u2013381 (2000)","journal-title":"STTT"},{"key":"21_CR15","unstructured":"Hao, J.K.: Memetic algorithms. A book chapter"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-39910-0_16","volume-title":"Verification: Theory and Practice","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 332\u2013358. Springer, Heidelberg (2004)"},{"key":"21_CR18","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proc. POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM, New York (2002)"},{"key":"21_CR19","volume-title":"Adaptation in natural and artificial systems","author":"J. Holland","year":"1975","unstructured":"Holland, J.: Adaptation in natural and artificial systems. The University of Michigan Press, Ann Arbor (1975)"},{"issue":"5","key":"21_CR20","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Spin model checker. IEEE Trans. Softw. Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivancic","year":"2005","unstructured":"Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F- Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-540-30482-1_23","volume-title":"Formal Methods and Software Engineering","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Groce, A., Clarke, E.M.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 224\u2013238. Springer, Heidelberg (2004)"},{"key":"21_CR23","volume-title":"Software Testing and Analysis: Process, Principles and Techniques","author":"M. Young","year":"2005","unstructured":"Young, M., Pezze, M.: Software Testing and Analysis: Process, Principles and Techniques. Wiley, New York (2005)"}],"container-title":["Lecture Notes in Computer Science","Model and Data Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24443-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,10]],"date-time":"2023-06-10T08:20:48Z","timestamp":1686385248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24443-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642244421","9783642244438"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24443-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}