Coursera Spring Sale
40% Off Coursera Plus Annual!
Grab it
Explore a 27-minute conference talk from VMCAI 2025 that presents a verified executable Scala backend for ASN1SCC, a compiler for ASN.1/ACN. Learn how researchers from EPFL and Ateleris GmbH developed a solution to generate Scala code from ASN.1, a language widely used for describing data structures in telecommunications. Discover how they enhanced the generator to emit not only executable code but also preconditions, postconditions, and lemmas for inductive proofs, enabling verification with Stainless, a program verifier for Scala. The presentation covers the verification of critical properties including runtime error prevention and invertibility of encoding/decoding functions, demonstrating a significant advancement in formally verifiable code generation for telecommunications protocols. This talk was presented at the VMCAI conference in January 2025, sponsored by ACM SIGPLAN.
