Publication

Mechanized Semantics for JavaScript Regular Expressions

2024

Abstract

We introduce a mechanization of the JavaScript regexes by transcribing the ECMAScript specification, to which JavaScript conforms, into Coq. We discuss the challenges which arose during this mechanization, and present our efforts to ensure that the result is faithful to the original paper specification. We also use our implementation to prove some properties of the specification, notably that the functions it defines terminate and that no operation ever fails. We extract the implemented engine to OCaml and execute it on test inputs to further increase confidence in its correctness.

Official source

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2024

Abstract

Official source

Related concepts (32)

JavaScript

JavaScript (ˈdʒɑːvəskrɪpt), often abbreviated as JS, is a programming language that is one of the core technologies of the World Wide Web, alongside HTML and CSS. As of 2023, 98.7% of websites use JavaScript on the client side for webpage behavior, often incorporating third-party libraries. All major web browsers have a dedicated JavaScript engine to execute the code on users' devices. JavaScript is a high-level, often just-in-time compiled language that conforms to the ECMAScript standard.

Regular expression

A regular expression (shortened as regex or regexp; sometimes referred to as rational expression) is a sequence of characters that specifies a match pattern in text. Usually such patterns are used by string-searching algorithms for "find" or "find and replace" operations on strings, or for input validation. Regular expression techniques are developed in theoretical computer science and formal language theory. The concept of regular expressions began in the 1950s, when the American mathematician Stephen Cole Kleene formalized the concept of a regular language.

ECMAScript

ECMAScript ('ɛkməskrɪpt; ES) is a standard for scripting languages, including JavaScript, JScript, and ActionScript. It is also best known as a JavaScript standard intended to ensure the interoperability of web pages across different web browsers. It is standardized by Ecma International in the document ECMA-262. ECMAScript is commonly used for client-side scripting on the World Wide Web, and it is increasingly being used to write server-side applications and services using Node.js and other runtime environments.

Related publications (5)

Mechanized Semantics for JavaScript Regular Expressions

Chat with Graph Search

Utility Metrics Specifications. OpenIoT Deliverable D422

Supporting Loop Proofs in KeY by using BLAST

Automating the Addition of Fail-Safe Fault-Tolerance: Beyond Fusion-Closed Specifications