{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T06:26:47Z","timestamp":1763706407521,"version":"3.45.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031827020"},{"type":"electronic","value":"9783031827037"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-82703-7_9","type":"book-chapter","created":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T02:16:47Z","timestamp":1737512207000},"page":"185-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally Verifiable Generated ASN.1\/ACN Encoders and\u00a0Decoders: A Case Study"],"prefix":"10.1007","author":[{"given":"Mario","family":"Bucev","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9751-9252","authenticated-orcid":false,"given":"Samuel","family":"Chassot","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3979-128X","authenticated-orcid":false,"given":"Simon","family":"Felix","sequence":"additional","affiliation":[]},{"given":"Filip","family":"Schramka","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,23]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrialstrength SMT solver. In: TACAS (1). Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Scala Workshop (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Blanc, R.W.: Verification by Reduction to Functional Programs. Ph.D. thesis, EPFL, Lausanne (2017). https:\/\/doi.org\/10.5075\/epfl-thesis-7636, http:\/\/infoscience.epfl.ch\/record\/230242","DOI":"10.5075\/epfl-thesis-7636"},{"key":"9_CR5","unstructured":"Bucev, M., Kun\u010dak, V.: Formally verified quite OK image format. In: Formal Methods in Computer-Aided Design (FMCAD) (2022)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Chassot, S., Kun\u010dak, V.: Verifying a realistic mutable hash table - case study (short paper). In: International Joint Conference on Automated Reasoning (IJCAR) (2024)","DOI":"10.1007\/978-3-031-63498-7_18"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, 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 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Delaware, B., Suriyakarn, S., Pit-Claudel, C., Ye, Q., Chlipala, A.: Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3(ICFP) (2019). https:\/\/doi.org\/10.1145\/3341686","DOI":"10.1145\/3341686"},{"key":"9_CR9","unstructured":"Enumeration, M.C.W.: CWE top 25 most dangerous software weaknesses. https:\/\/cwe.mitre.org\/top25\/ (2023). Accessed 4 Sep 2024"},{"key":"9_CR10","unstructured":"ESA-ESTEC, E.S.: Telemetry and telecommand packet utilization. Standard, European Cooperation for Space Standardization (April 2016)"},{"key":"9_CR11","unstructured":"Google: Protocol buffers. https:\/\/protobuf.dev\/"},{"key":"9_CR12","unstructured":"Group, N.W.: Internet x.509 public key infrastructure certificate and certificate revocation list (crl) profile. https:\/\/www.rfc-editor.org\/rfc\/rfc5280"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Guilloud, S., Bucev, M., Milovan\u010devi\u0107, D., Kun\u010dak, V.: Formula normalizations in verification. In: Computer-Aided Verification (CAV) (2023)","DOI":"10.1007\/978-3-031-37709-9_19"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Hamza, J., Felix, S., Kun\u010dak, V., Nussbaumer, I., Schramka, F.: From verified Scala to STIX file system embedded code using Stainless. In: NASA Formal Methods (NFM), pp.\u00a018 (2022). http:\/\/infoscience.epfl.ch\/record\/292424","DOI":"10.1007\/978-3-031-06773-0_21"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: formalized foundations for the Stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA) (Oct 2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Isychev, A., Darulova, E.: Scaling up roundoff analysis of functional data structure programs. In: SAS. Lecture Notes in Computer Science, vol. 14284, pp. 371\u2013402. Springer (2023)","DOI":"10.1007\/978-3-031-44245-2_17"},{"key":"9_CR17","unstructured":"ITU-T Study Group 17: Abstract syntax notation one (ASN.1) recommendations. Standard ITU-T X.680, International Telecommunication Union (ITU), Geneva, CH (2008). https:\/\/www.itu.int\/ITU-T\/studygroups\/com17\/languages\/"},{"key":"9_CR18","unstructured":"Laboratory, N.I.T.: National vulnerability database CVE-2024-37305 detail. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2024-37305"},{"key":"9_CR19","unstructured":"Mamais, G., Tsiodras, T., Lesens, D., Perrotin, M.: An ASN.1 compiler for embedded\/space systems. In: Embedded Real Time Software and Systems (ERTS2012). Toulouse, France (Feb 2012), https:\/\/hal.science\/hal-02263447"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Mondet, S., Alberdi, I., Plagemann, T.: Generating optimised and formally checked packet parsing code. In: IFIP International Information Security Conference, pp. 173\u2013184. Springer (2011)","DOI":"10.1007\/978-3-642-21424-0_14"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"9_CR22","unstructured":"N7 Space: ASN.1 PUS-C types library. https:\/\/n7space.github.io\/asn1-pusc-lib\/. Accessed 13 Sep 2024"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Ni, H., Delignat-Lavaud, A., Fournet, C., Ramananandro, T., Swamy, N.: ASN1*: provably correct, non-malleable parsing for ASN.1 DER. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 275\u2013289. ACM, Boston MA USA (Jan 2023). https:\/\/doi.org\/10.1145\/3573105.3575684","DOI":"10.1145\/3573105.3575684"},{"key":"9_CR24","unstructured":"Office, E.S.: ESA cyber security resilience achievement. Tech. rep., European Space Agency (10 2023)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"issue":"8","key":"9_CR26","first-page":"127","volume":"5","author":"M Slee","year":"2007","unstructured":"Slee, M., Agarwal, A., Kwiatkowski, M.: Thrift: scalable cross-language services implementation. Facebook white pap. 5(8), 127 (2007)","journal-title":"Facebook white pap."},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Static Analysis Symposium (SAS) (2011)","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Swamy, N., et al.: Hardening attack surfaces with formally proven binary format parsers. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 31\u201345. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523708","DOI":"10.1145\/3519939.3523708"},{"key":"9_CR29","unstructured":"Tsiodras, T.: TASTE - an ESA-led toolchain that uses model-driven code generation to create correct-by-construction sw for safety-critical targets. In: MeTRiD 2018: First International Workshop on Methods and Tools for Rigorous System Design (2018)"},{"key":"9_CR30","unstructured":"Voirol, N.: Verified Functional Programming. Ph.D. thesis, EPFL, Switzerland (2019)"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Scala Symposium (2015)","DOI":"10.1145\/2774975.2774978"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-82703-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T06:13:57Z","timestamp":1763705637000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-82703-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031827020","9783031827037"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-82703-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denver, CO","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2025","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":"vmcai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}