Abstract
In the early days of the world wide web, browsers were developed to navigate through (static) HTML web page documents. This has changed dramatically, and nowadays web pages are dynamic, expressed by programs written in regular programming languages. As a result, browsers are almost operating systems, having to interpret/compile such programs and execute them within the browser itself. Currently, while JavaScript is the main de facto language to express web pages, it does have various short comings and performance inefficiencies. WebAssembly, a new portable and size/load efficient alternative developed by major IT powerhouses, is seen as the future substitute. As WebAssembly aims to be more performance efficient than JavaScript, we aim to look at this current status and present a preliminary study on the performance of these two, based on their runtime and energy efficiency. Preliminary results show that WebAssembly, while still in its infancy, is starting to already challenge JavaScript, with much more room to grow. Additionally, our benchmarking framework is also made available to allow further research and replication.

Abstract
Recent studies show that many real-world software faults are due to slight modifications (mutations) to the program. Thus, analyzing transformations made by a developer and associating them with well-known mutation operators can help pinpoint and repair the root cause of failures. This paper proposes a mutation operator inference technique: given the original program and one of its subsequent forms, it infers which mutation operators would transform the original and produce such a version. Moreover, we implemented this technique as a tool called Morpheus, which analyzes faulty Java programs. We have also validated both the technique and tool by analyzing a repository with 1753 modifications for 20 different programs, successfully inferring mutation operators 78% of times. Furthermore, we also show that several program versions result from not just a single mutation operator but multiple ones. In the end, we resort to real-world case studies to demonstrate the advantages of this approach regarding program repair.

Abstract
Software patterns are well known to both researchers and practitioners. They emerge from the need to tackle problems that become ever more common in development activities. Thus, it is not surprising that patterns have also been explored as a means to address issues related to energy consumption. In this chapter, we discuss patterns at code and design level and address energy efficiency not only as the main concern of patterns but also as a side effect of patterns that were not originally intended to deal with this problem. We first elaborate on state-of-the-art energy-oriented and general-purpose patterns. Next, we present cases of how patterns appear naturally as part of decisions made in industrial projects. By looking at the two levels of abstraction, we identify recurrent issues and solutions. In addition, we illustrate how patterns take part in a network of interconnected components and address energetic concerns. The reporting and cases discussed in this chapter emphasize the importance of being aware of energy-efficient strategies to make informed decisions, especially when developing sustainable software systems.

Abstract

Abstract

Abstract
MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.