{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:56:25Z","timestamp":1747810585784,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642277047"},{"type":"electronic","value":"9783642277054"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_9","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T12:18:06Z","timestamp":1327493886000},"page":"98-113","source":"Crossref","is-referenced-by-count":9,"title":["Development and Evaluation of LAV: An SMT-Based Error Finding Platform"],"prefix":"10.1007","author":[{"given":"Milena","family":"Vujo\u0161evi\u0107-Jani\u010di\u0107","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Ackermann, W.: Solvable cases of the decision problem. North-Holland (1954)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Babi\u0107, D., Hu, A.J.: Calysto: Scalable and Precise Extended Static Checking. In: ICSE 2008, pp. 211\u2013220. ACM (2008)","DOI":"10.1145\/1368088.1368118"},{"key":"9_CR3","unstructured":"Balakrishnan, G., Ganai, M.K., Gupta, A., Ivancic, F., Kahlon, V., Li, W., Maeda, N., Papakonstantinou, N., Sankaranarayanan, S., Sinha, N., Wang, C.: Scalable and precise program analysis at nec. In: FMCAD (2010)"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108768.1108813","volume":"31","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. ACM Sigsoft Software Engineering Notes\u00a031, 82\u201387 (2006)","journal-title":"ACM Sigsoft Software Engineering Notes"},{"key":"9_CR5","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 825\u2013885. IOS Press (2009)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"9_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/11916277_38","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bruttomesso","year":"2006","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Santuari, A., Sebastiani, R.: To Ackermannize or Not to Ackermannize? In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 557\u2013571. Springer, Heidelberg (2006)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"9_CR10","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI (2008)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: S2e: a platform for in-vivo multi-path analysis of software systems. SIGARCH Comput. Archit. News\u00a039 (2011)","DOI":"10.1145\/1961295.1950396"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSL-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ansi-c software. In: ASE, pp. 137\u2013148 (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"9_CR14","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. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"9_CR15","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Tool paper at (August 2006), \n                  \n                    http:\/\/-yices.csl.sri.com\/tool-paper.pdf"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Proc.\u00a0ACM SIGPLAN POPL (January 2001)","DOI":"10.1145\/360204.360220"},{"issue":"7","key":"9_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":"9_CR18","doi-asserted-by":"crossref","unstructured":"Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: Proceedings of ASE 2007. ACM (2007)","DOI":"10.1145\/1321631.1321691"},{"key":"9_CR19","unstructured":"Sankaranarrayanan, S.: Necla static analysis benchmarks (2009), \n                  \n                    http:\/\/www.nec-labs.com\/research\/system"},{"key":"9_CR20","unstructured":"Sinz, C., Falke, S., Merz, F.: The low-level bounded model checker llbmc: A precise memory model for llbmc. In: SSV (2010)"},{"key":"9_CR21","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., Halleux, J.: Pex White Box Test Generation for.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. SIGSOFT Softw. Eng. Notes\u00a029 (2004)","DOI":"10.1145\/1041685.1029911"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T02:05:25Z","timestamp":1578535525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_9"}},"subtitle":["System Description"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}