Related papers: The Essence of JavaScript
There is a plethora of research articles describing the deep semantics of JavaScript. Nevertheless, such articles are often difficult to grasp for readers not familiar with formal semantics. In this report, we propose a digest of the…
Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that…
We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational…
Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic…
Dependency analysis is a program analysis that determines potential data flow between program points. While it is not a security analysis per se, it is a viable basis for investigating data integrity, for ensuring confidentiality, and for…
The JSC language is a superset of JavaScript designed to ease the development of large web applications. This language extends JavaScripts own object system by isolating code in a class declaration, simplifying multiple inheritance and…
The idea of using unfolding as a way of computing a program semantics has been applied successfully to logic programs and has shown itself a powerful tool that provides concrete, implementable results, as its outcome is actually source…
JavaScript is one of the most popular programming languages on the web. Despite the language popularity and the increasing size of JavaScript systems, there is a limited number of visualization tools that can be used by developers to…
JavaScript has been consistently among the most popular programming languages in the past decade. However, its dynamic, weakly-typed, and asynchronous nature can make it challenging to write maintainable code for developers without in-depth…
We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its faithfulness by proving it equivalent to a preexisting…
This article presents a formalisation of a simple imperative programming language. The objective is to study and develop "hands-on" a formal specifcation of a programming language, namely its syntax, operational semantics and type system.…
Modern regex languages have strayed far from well-understood traditional regular expressions: they include features that fundamentally transform the matching problem. In exchange for these features, modern regex engines at times suffer from…
SEMAT/OMG Essence provides a powerful Language and a Kernel for describing software development processes. How can it be tweaked to apply it to systems engineering methods description? We must harmonize Essence and various systems…
Verifying properties of object-oriented software requires a method for handling references in a simple and intuitive way, closely related to how O-O programmers reason about their programs. The method presented here, a Calculus of Object…
JavaScript is a popular attack vector for releasing malicious payloads on unsuspecting Internet users. Authors of this malicious JavaScript often employ numerous obfuscation techniques in order to prevent the automatic detection by…
Web sites routinely incorporate JavaScript programs from several sources into a single page. These sources must be protected from one another, which requires robust sandboxing. The many entry-points of sandboxes and the subtleties of…
JavaScript's widespread adoption has made it an attractive target for malicious attackers who employ sophisticated obfuscation techniques to conceal harmful code. Current deobfuscation tools suffer from critical limitations that severely…
Semantic parsing aims at mapping natural language utterances into structured meaning representations. In this work, we propose a structure-aware neural architecture which decomposes the semantic parsing process into two stages. Given an…
The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like…
We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the…