{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:00:09Z","timestamp":1760043609321,"version":"3.40.3"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452360"},{"type":"electronic","value":"9783030452377"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":107,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.<\/jats:p>","DOI":"10.1007\/978-3-030-45237-7_6","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"98-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Highly Automated Formal Proofs over Memory Usage of Assembly Code"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6625-1123","authenticated-orcid":false,"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1055-8003","authenticated-orcid":false,"given":"Joshua A.","family":"Bockenek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8663-739X","authenticated-orcid":false,"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: International Conference on Computer Aided Verification. pp. 515\u2013518. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_49"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: International Conference on Computer Aided Verification. pp. 298\u2013302. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Baumann, C., N\u00e4slund, M., Gehrmann, C., Schwarz, O., Thorsen, H.: A high assurance virtualization platform for armv8. In: 2016 European Conference on Networks and Communications (EuCNC). pp. 210\u2013214. IEEE (2016)","DOI":"10.1109\/EuCNC.2016.7561034"},{"issue":"4","key":"6_CR4","first-page":"519","volume":"5","author":"WR Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit and the short stack. Journal of Automated Reasoning 5(4), 519\u2013530 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5(4), 411\u2013428 (Dec1989). 10.1007\/BF00243131","DOI":"10.1007\/BF00243131"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Bockenek, J.A., Verbeek, F., Lammich, P., Ravindran, B.: Formal verification of memory preservation of x86-64 binaries (Sep 2019)","DOI":"10.1007\/978-3-030-26601-1_3"},{"key":"6_CR7","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, Inc. (1979)"},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"RS Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. Journal of the ACM 43(1), 166\u2013192 (1996)","journal-title":"Journal of the ACM"},{"key":"6_CR9","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: A binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) International Conference on Computer Aided Verification. pp. 463\u2013469. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). 10.1007\/978-3-642-22110-1_37"},{"key":"6_CR10","unstructured":"Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods. pp. 459\u2013465. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). 10.1007\/978-3-642-20398-5_33, https:\/\/fbinfer.com\/"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 289\u2013300. POPL \u201909 (2009)","DOI":"10.1145\/1480881.1480917"},{"key":"6_CR12","unstructured":"Carr\u00e9, B.A., O\u2019Neill, I.M., Clutterbuck, D.L., Debney, C.W.: SPADE\u2014the southampton program analysis and development environment. In: Software Engineering Environments. Peter Peregrinus, Ltd., Stevenage (1986)"},{"key":"6_CR13","unstructured":"Chisnall, D.: The Definitive Guide to the Xen Hypervisor. Pearson Education (2008)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Clutterbuck, D.L., Carr\u00e9, B.A.: The verification of low-level code. SoftwareEngineering Journal 3(3), 97\u2013111 (May 1988). 10.1049\/sej.1988.0012","DOI":"10.1049\/sej.1988.0012"},{"key":"6_CR15","unstructured":"Cowan, C., Pu, C., Maier, D., Walpole, J., Bakke, P., Beattie, S., Grier, A., Wagle, P., Zhang, Q., Hinton, H.: Stackguard: Automatic adaptive detection and prevention of buffer-overflow attacks. In: USENIX Security Symposium. vol. 98, pp. 63\u201378. San Antonio, TX (1998)"},{"key":"6_CR16","unstructured":"Dam, M., Guanciale, R., Nemati, H.: Machine code verification of a tiny ARM hypervisor. In: Proceedings of the 3rd International Workshop on Trustworthy Embedded Devices. pp. 3\u201312. TrustED \u201913, ACM Press, New York, NY, USA (2013). 10.1145\/2517300.2517302"},{"key":"6_CR17","unstructured":"Dawson, J., Graunke, P., Huffman, B., Klein, G., Matthews, J.: Machine words in Isabelle\/HOL (Aug 2018)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software 19(1), 42\u201351 (Jan 2002). 10.1109\/52.976940","DOI":"10.1109\/52.976940"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. Tech. Rep. YALEU\/DCS\/TR-1336, Dept. of Computer Science, Yale University, New Haven, CT (Nov 2005), http:\/\/flint.cs.yale.edu\/publications\/sbca.html","DOI":"10.1145\/1133981.1134028"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI\u201906, vol. 41, pp. 401\u2013414. ACM Press, New York, NY, USA (Jun 2006)","DOI":"10.1145\/1133255.1134028"},{"issue":"1","key":"6_CR21","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Mathematical Aspects of Computer Science 19(1), 19\u201332 (1967)","journal-title":"Mathematical Aspects of Computer Science"},{"key":"6_CR22","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving. pp. 243\u2013258. Springer Berlin Heidelberg, Berlin, Heidelberg (2010). 10.1007\/978-3-642-14052-5_18"},{"key":"6_CR23","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification. pp. 519\u2013531. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). \/10.1007\/978-3-540-73368-3_52"},{"key":"6_CR24","unstructured":"Goel, S.: Formal Verification of Application and System Programs Based on a Validated x86 ISA Model. Ph.D. thesis (2016), http:\/\/hdl.handle.net\/2152\/46437"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Goel, S., Hunt, W.A., Kaufmann, M., Ghosh, S.: Simulation and formal verification of x86 machine-code programs that make system calls. In: 2014 Formal Methods in Computer-Aided Design (FMCAD). pp. 91\u201398 (Oct 2014). 10.1109\/FMCAD.2014.6987600","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) International Conference on Interactive Theorem Proving. pp. 99\u2013115. ITP 2012, Springer-Verlag, Berlin, Heidelberg (Aug 2012)","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Heule, S., Schkufza, E., Sharma, R., Aiken, A.: Stratified synthesis: Automatically learning the x86\u201364 instruction set. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 237\u2013250. PLDI \u201916, ACM, New York, NY, USA (2016)","DOI":"10.1145\/2908080.2908121"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576\u2013580 (Oct 1969)","DOI":"10.1145\/363235.363259"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (Aug 1978). 10.1145\/359576.359585","DOI":"10.1145\/359576.359585"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39(12),92\u2013106 (Dec 2004). 10.1145\/1052883.1052895, http:\/\/findbugs.sourceforge.net\/","DOI":"10.1145\/1052883.1052895"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems 32(1), 2:1\u20132:70 (Feb 2014). 10.1145\/256053710.1145\/2560537","DOI":"10.1145\/2560537"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: European Symposium on Programming. pp. 696\u2013723. Springer (2017)","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"6_CR34","unstructured":"Kruegel, C., Kirda, E., Mutz, D., Robertson, W., Vigna, G.: Automating mimicry attacks using static binary analysis. In: USENIX Security Symposium. vol. 14,\n  pp.  11\u201311 (2005)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 179\u2013191. POPL \u201914, ACM, New York, NY, USA (2014), https:\/\/cakeml.org\/","DOI":"10.1145\/2535838.2535841"},{"key":"6_CR36","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: Embedded Real Time Software and Systems, 8th European Congress. ERTS 2016, SEE, HAL, Toulouse, France (Jan 2016), https:\/\/hal.inria.fr\/hal-01238879"},{"issue":"3","key":"6_CR37","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T., Wenzel, M.: Eisbach: A proof method language for Isabelle. Journal of Automated Reasoning 56(3), 261\u2013282 (2016)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. 362\u2013376. Springer-Verlag (2006)","DOI":"10.1007\/11916277_25"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer-Verlag (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine\n  code. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the\n  Construction and Analysis of Systems. pp. 568\u2013582. Springer-Verlag, Berlin,\n  Heidelberg (2007)","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures\u2014an application of decompilation into logic. In: 2008 Formal Methods in Computer-Aided Design. pp. 1\u20138. IEEE (Nov 2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"6_CR42","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic\u2013improved. In: 2012 Formal Methods in Computer-Aided Design (FMCAD). pp. 78\u201381. IEEE (2012)"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 106\u2013119. ACM (1997)","DOI":"10.1145\/263699.263712"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer Science & Business Media (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: International Workshop on Computer Science Logic. pp. 1\u201319. Springer (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"6_CR46","unstructured":"Quynh, N.A.: Capstone: Next-gen disassembly framework (Aug 2014), http:\/\/www.capstone-engine.org\/, accessed June 27, 2019"},{"key":"6_CR47","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55\u201374. IEEE (2002)"},{"issue":"2","key":"6_CR48","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"HG Rice","year":"1953","unstructured":"Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society 74(2), 358\u2013366 (1953)","journal-title":"Transactions of the American Mathematical Society"},{"key":"6_CR49","doi-asserted-by":"crossref","unstructured":"Roessle, I., Verbeek, F., Ravindran, B.: Formally verified big step semantics out of x86-64 binaries. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 181\u2013195. CPP 2019, ACM, New York, NY, USA (2019)","DOI":"10.1145\/3293880.3294102"},{"key":"6_CR50","unstructured":"Rushby, J.: Noninterference, Transitivity, and Channel-Control Security Policies. SRI International, Computer Science Laboratory (1992)"},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 471\u2013482. PLDI \u201913, ACM, New York, NY, USA (2013)","DOI":"10.1145\/2491956.2462183"},{"key":"6_CR52","doi-asserted-by":"crossref","unstructured":"Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: Formal verified OSEK\/VDX real-time operating system. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems. pp. 293\u2013301 (Jul 2012)","DOI":"10.1109\/ICECCS20050.2012.6299224"},{"key":"6_CR53","doi-asserted-by":"crossref","unstructured":"Shi, J., Zhu, L., Fang, H., Guo, J., Zhu, H., Ye, X.: xBIL \u2013 a hardware resource oriented binary intermediate language. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems. pp. 211\u2013219 (Jul 2012)","DOI":"10.1109\/ICECCS20050.2012.6299216"},{"key":"6_CR54","doi-asserted-by":"crossref","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: International Conference on Theorem Proving in Higher Order Logics. pp. 28\u201332. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"6_CR55","doi-asserted-by":"crossref","unstructured":"Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., Saxena, P.: BitBlaze: A new approach to computer security via binary analysis. In: Proceedings of the 4th International Conference on Information Systems Security. Keynote invited paper. Hyderabad, India (Dec 2008)","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"6_CR56","doi-asserted-by":"crossref","unstructured":"Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P.: Auspice: Automatic safety property verification for unmodified executables. In: VSSTE. pp. 202\u2013222. Springer (2015)","DOI":"10.1007\/978-3-319-29613-5_12"},{"key":"6_CR57","unstructured":"Verbeek, F., Bockenek, J.A., Ravindran, B.: Artifact \u2013 Highly automated formal proofs over memory usage of assembly code (2020). 10.5281\/zenodo.3676687"},{"key":"6_CR58","doi-asserted-by":"crossref","unstructured":"Wang, F., Shoshitaishvili, Y.: Angr \u2013 the next generation of binary analysis. In: 2017 IEEE Cybersecurity Development (SecDev). pp. 8\u20139. IEEE (2017)","DOI":"10.1109\/SecDev.2017.14"},{"key":"6_CR59","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a generic framework for human-readable proof documents. From Insight to Proof\u2014Festschrift in Honour of Andrzej Trybulec 10(23), 277\u2013298 (2007)"},{"key":"6_CR60","unstructured":"Yu, Y.: Automated Proofs of Object Code for a Widely Used Microprocessor. Ph.D. thesis, University of Texas at Austin (1992)"},{"key":"6_CR61","unstructured":"Zhang, M., Sekar, R.: Control flow integrity for COTS binaries. In: Presented as part of the 22nd USENIX Security Symposium (USENIX Security 13). pp. 337\u2013352 (2013)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45237-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:05:51Z","timestamp":1616436351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45237-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452360","9783030452377"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45237-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}