{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T20:45:15Z","timestamp":1792961115954,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642203978","type":"print"},{"value":"9783642203985","type":"electronic"}],"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-20398-5_6","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T19:29:49Z","timestamp":1302118189000},"page":"58-72","source":"Crossref","is-referenced-by-count":14,"title":["Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Jason","family":"Belt","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"family":"Robby","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrice","family":"Chalin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Hardin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xianghua","family":"Deng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6_CR1","volume-title":"High Integrity Software \u2013 the SPARK Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software \u2013 the SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"6_CR3","unstructured":"Belt, J., Hatcliff, J., Robby, Chalin, P., Hardin, D., Deng, X.: Bakar Kiasan: Flexible contract checking for critical systems using symbolic execution. Technical Report SAnToS-TR2011-01-03, Kansas State University (2011), http:\/\/people.cis.ksu.edu\/~belt\/SAnToS-TR2011-01-03.pdf"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Belt, J., Robby, Deng, X.: Sireum\/Topi LDP: A lightweight semi-decision procedure for optimizing symbolic execution-based analyses. In: Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 355\u2013364 (2009)","DOI":"10.1145\/1595696.1595762"},{"key":"6_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 209\u2013224. USENIX Association (2008)"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.entcs.2005.01.023","volume":"131","author":"B.-Y.E. Chang","year":"2005","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Inferring object invariants: Extended abstract. Electr. Notes Theor. Comput. Sci.\u00a0131, 63\u201374 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"6_CR8","unstructured":"Deng, X., Lee, J., Robby: Efficient symbolic execution algorithms for programs manipulating dynamic heap objects. Technical Report SAnToS-TR2009-09-25, Kansas State University (September 2009)"},{"key":"6_CR9","unstructured":"Deng, X., Walker, R., Robby: Program behavioral benchmarks for evaluating path-sensitive bounded verification techniques. Technical Report SAnToS-TR2010-08-20, Kansas State University (2010)"},{"key":"6_CR10","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (August 2006), Tool paper at http:\/\/yices.csl.sri.com\/-tool-paper.pdf"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1065010.1065036","volume-title":"ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI), pp. 213\u2013223. ACM Press, New York (2005)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Grieskamp, W., Tillmann, N., Schulte, W.: XRT\u2013exploring runtime for .NET: Architecture and applications. In: Workshop on Software Model Checking (2005)","DOI":"10.1016\/j.entcs.2006.01.002"},{"issue":"3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1145\/356674.356677","volume":"8","author":"S.L. Hantler","year":"1976","unstructured":"Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Computing Surveys (CSUR)\u00a08(3), 331\u2013353 (1976)","journal-title":"ACM Computing Surveys (CSUR)"},{"issue":"2","key":"6_CR14","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"6_CR15","unstructured":"Jackson, P., Passmore, G.: Proving SPARK verification conditions with SMT solvers (2009), Draft journal article, http:\/\/homepages.inf.ed.ac.uk\/pbj\/papers\/vct-dec09-draft.pdf"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"issue":"7","key":"6_CR17","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of the ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Communications of the ACM"},{"key":"6_CR18","volume-title":"Decision Procedures \u2013 An Algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures \u2013 An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/11575467_9","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 119\u2013134. Springer, Heidelberg (2005)"},{"key":"6_CR20","unstructured":"Rossebo, B., Oman, P., Alves-Foss, J., Blue, R., Jaszkowiak, P.: Using SPARK-Ada to model and verify a MILS message router. In: Proceedings of the International Symposium on Secure Software Engineering (2006)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Rushby, J.: The design and verification of secure systems. In: 8th ACM Symposium on Operating Systems Principles, vol.\u00a015(5), pp. 12\u201321 (1981)","DOI":"10.1145\/1067627.806586"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Sen, K., Agha, G.: CUTE: A concolic unit testing engine for C. In: ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pp. 263\u2013272 (2005)","DOI":"10.1145\/1095430.1081750"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013white box test generation for.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"6_CR24","unstructured":"Frama-C website, http:\/\/frama-c.com\/"},{"key":"6_CR25","unstructured":"Victor website, http:\/\/homepages.inf.ed.ac.uk\/pbj\/spark\/victor.html"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T06:48:26Z","timestamp":1637477306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}