{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:08Z","timestamp":1725903368464},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_2","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"8-25","source":"Crossref","is-referenced-by-count":2,"title":["Towards Logic-Based Verification of JavaScript Programs"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 Fragoso","family":"Santos","sequence":"first","affiliation":[]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[]},{"given":"Petar","family":"Maksimovi\u0107","sequence":"additional","affiliation":[]},{"given":"Daiva","family":"Naud\u017ei\u016bnien\u0117","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Andreasen, E., M\u00f8ller, A.: Determinacy in static analysis for jQuery. In: OOPSLA (2014)","DOI":"10.1145\/2660193.2660214"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115\u2013137. Springer, Heidelberg (2006). doi: 10.1007\/11804192_6"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: Slayer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178\u2013183. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_15"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Bodin, M., Chargu\u00e9raud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 87\u2013100. ACM Press (2014)","DOI":"10.1145\/2535838.2535876"},{"key":"2_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, 8\u201310 December 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2015","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Cham (2015). doi: 10.1007\/978-3-319-17524-9_1"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"\u015etef\u0103nescu, A., Park, D., Yuwen, S., Li, Y., Ro\u015fu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), pp. 74\u201391. ACM, November 2016","DOI":"10.1145\/3022671.2984027"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.: jStar: towards practical verification for Java. In: OOPSLA (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"2_CR10","unstructured":"ECMAScript Committee. The 5th edn. of the ECMAScript Language Specification. Technical report, ECMA (2011)"},{"key":"2_CR11","unstructured":"ECMAScript Committee. Test262 test suite (2017). https:\/\/github.com\/tc39\/test262"},{"key":"2_CR12","unstructured":"Fink, S., Dolby, J.: WALA \u2013 The T.J. Watson Libraries for Analysis (2015). http:\/\/wala.sourceforge.net\/"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Gardner, P., Maffeis, S., Smith, G.: Towards a program logic for JavaScript. In: Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 31\u201344. ACM Press (2012)","DOI":"10.1145\/2103656.2103663"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-14107-2_7","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"A Guha","year":"2010","unstructured":"Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of JavaScript. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126\u2013150. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14107-2_7"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_4"},{"key":"2_CR16","unstructured":"JaVerT Team. Javert (2017). http:\/\/goo.gl\/au69SV"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-03237-0_17","volume-title":"Static Analysis","author":"SH Jensen","year":"2009","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238\u2013255. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03237-0_17"},{"key":"2_CR18","unstructured":"Jones, J.: Priority queue data structure (2016). https:\/\/github.com\/jasonsjones\/queue-pri"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Kashyap, V., Dewey, K., Kuefner, E.A., Wagner, J., Gibbons, K., Sarracino, J., Wiedermann, B., Hardekopf, B.: JSAI: a static analysis platform for JavaScript. In: FSE, pp. 121\u2013132 (2014)","DOI":"10.1145\/2635868.2635904"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_26"},{"key":"2_CR21","unstructured":"Livshits, B.: JSIR, an intermediate representation for JavaScript analysis (2014). http:\/\/too4words.github.io\/jsir\/"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Park, D., Stef\u0103nescu, A., Ro\u015fu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, New York, USA, pp. 346\u2013356. ACM (2015)","DOI":"10.1145\/2737924.2737991"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Politz, J.G., Carroll, M.J., Lerner, B.S., Pombrio, J., Krishnamurthi, S.: A tested semantics for getters, setters, and eval in JavaScript. In: Proceedings of the 8th Symposium on Dynamic Languages (2012)","DOI":"10.1145\/2384577.2384579"},{"issue":"6","key":"2_CR24","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Logic Algebraic Program."},{"issue":"3","key":"2_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(3:21)2011","volume":"7","author":"J Schwinghammer","year":"2011","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. Logical Methods Comput. Sci. 7(3), 1\u201342 (2011)","journal-title":"Logical Methods Comput. Sci."},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-31057-7_20","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"M Sridharan","year":"2012","unstructured":"Sridharan, M., Dolby, J., Chandra, S., Sch\u00e4fer, M., Tip, F.: Correlation tracking for points-to analysis of JavaScript. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 435\u2013458. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31057-7_20"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Visser, W., P\u01ces\u01cereanu, C.S., Khurshid, S.: Test input generation with java pathfinder. In: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, New York, USA, pp. 97\u2013107. ACM (2004)","DOI":"10.1145\/1007512.1007526"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T08:26:17Z","timestamp":1569745577000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}