{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:22:22Z","timestamp":1725567742389},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232520"},{"type":"electronic","value":"9783540302322"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-30232-2_6","type":"book-chapter","created":{"date-parts":[[2010,10,24]],"date-time":"2010-10-24T15:56:19Z","timestamp":1287935779000},"page":"79-96","source":"Crossref","is-referenced-by-count":3,"title":["Localizing Program Errors for Cimple Debugging"],"prefix":"10.1007","author":[{"given":"Samik","family":"Basu","sequence":"first","affiliation":[]},{"given":"Diptikalyan","family":"Saha","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing error in counterexample traces. In: Proceedings of POPL (2003)","DOI":"10.1145\/604131.604140"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proceedings of SPIN Workshop (2000)","DOI":"10.1007\/10722468_7"},{"key":"6_CR4","unstructured":"Ball, T., Rajamani, S.K.: Slam (2003), http:\/\/research.microsoft.com\/slam"},{"key":"6_CR5","unstructured":"Basu, S., Saha, D., Smolka, S.A.: Getting to the root of the problem: Focus statements for the analysis of counter-examples. Technical report, SUNYSB (2004)"},{"key":"6_CR6","unstructured":"BLAST. Berkeley lazy abstraction software verification tool (2003), http:\/\/www-cad.eecs.berkeley.edu\/~rupak\/blast\/"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM TOPLAS\u00a08(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"6_CR8","volume-title":"Introduction to Algorithm","author":"T.H. Corman","year":"1990","unstructured":"Corman, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithm. MIT Press, Cambridge (1990)"},{"key":"6_CR9","unstructured":"Dwyer, M.B., Hatcliff, J.: Slicing software for model construction. In: Partial Evaluation and Semantic-Based Program Manipulation (1999)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Engler, D., Ashcraft, K.: RacerX: Effective, static detection of race conditions and deadlocks. In: Proceedings of SOSP (2003)","DOI":"10.1145\/945445.945468"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 324. Springer, Heidelberg (2001)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Proceedings of POPL (1997)","DOI":"10.1145\/263699.263717"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-24730-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Groce","year":"2004","unstructured":"Groce, A.: Error explanation with distance metrics. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 108\u2013122. Springer, Heidelberg (2004)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: Proceedings of SPIN Workshop on Model Checking of Software (2003)","DOI":"10.1007\/3-540-44829-2_8"},{"key":"6_CR15","unstructured":"Aristotle Research Group. Program analysis based software engineering (2003), http:\/\/www.cc.gatech.edu\/aristotle\/"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"CONCUR 2001 - Concurrency Theory","author":"J. Hatcliff","year":"2001","unstructured":"Hatcliff, J., Dwyer, M.: Using the bandera tool set to model-check properties of concurrent Java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, p. 39. Springer, Heidelberg (2001)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: Extracting verification models from source code. In: Proceedings of FORTE (1999)","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. In: Proceedings of PLDI (1988)","DOI":"10.1145\/53990.53994"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/3-540-46002-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2002","unstructured":"Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 445. Springer, Heidelberg (2002)"},{"key":"6_CR21","unstructured":"MOPED. A model checker for pushdown systems (2003), http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Proceedings of the ISP (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"6_CR23","unstructured":"RTCA. Minimum operational performance stardards for traffic alert and collision aviodance system (TCAS) airborne equipment consolidated edition (1990)"},{"key":"6_CR24","unstructured":"Rybalchenko, A.: A Model Checker based on Abstraction Refinement. PhD thesis, Universitt des Saarlandes (2002)"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45251-6_35","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"N. Sharygina","year":"2001","unstructured":"Sharygina, N., Peled, D.: A combined testing and verification approach for software reliability. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 611. Springer, Heidelberg (2001)"},{"key":"6_CR26","unstructured":"The XSB logic programming system (2003), http:\/\/xsb.sourceforge.net"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30232-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T21:00:50Z","timestamp":1559768450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30232-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232520","9783540302322"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30232-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}