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.

Abstract