Abstract
Energy consumption is an issue that involves all of us, both as individuals and as members of a society, and covers all our areas of activity. It is something so broad that its impact has important reflections on our social, cultural and financial structures. The domain of software, and in particular database systems, is not an exception. Although it seems to be a little bit strange to study the energy consumption of just one query, when we consider the execution of a a few thousand queries per second, quickly we see the importance of the querying consumption in the monthly account of any company that has a conventional data center. To demonstrate the energy consumption of queries in data centers, we idealized a small dashboard for monitoring and analyzing the sales of a company, and implemented all the queries needed for populating it and ensuring its operation. The queries were organized into two groups, oriented especially to two distinct database management systems: one relational (MySQL) and one non relational (Neo4J). The goal is to evaluate the energy consumption of different types of queries, and at the same time compare it in terms of relational and non-relational database approaches. This paper relates the process we implemented to set up the energy consumption application scenario, measure the energy consumption of each query, and present our first preliminary results.

Abstract
Spreadsheets are used in professional business contexts to make decisions based on collected data. Usually, these spreadsheets are developed by end users (e. g. accountants) in an ad-hoc way. The effect of this practice is that the business logic of a concrete spreadsheet is not explicit to them. Thus, its correctness is hard to assess and users have to trust. We present an approach where structure and computational behavior of a spreadsheet are specified by a model with a process-like notation based on combining pre-defined functional spreadsheet services with typed interfaces. This allows for a consistent construction of a spreadsheet by defining its structure and computational behavior as well as filling it with data and executing the defined computational behavior. Thus, concrete spreadsheets are equipped with a specification of their construction process. This supports their understanding and correct usage, even in case of legacy spreadsheets. The approach has been developed in cooperation with an industrial partner from the automotive industry.

Abstract

Abstract
Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the SUPER COP framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines.

Abstract
We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i.a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

Abstract
Critical human-machine interfaces are present in many systems including avionics systems and medical devices. Use error is a concern in these systems both in terms of hardware panels and input devices, and the software that drives the interfaces. Guaranteeing safe usability, in terms of buttons, knobs and displays is now a key element in the overall safety of the system. New integrated development environments (IDEs) based on formal methods technologies have been developed by the research community to support the design and analysis of high-confidence human-machine interfaces. To date, little work has focused on the comparison of these particular types of formal IDEs. This paper compares and evaluates two state-of-the-art toolkits: CIRCUS, a model-based development and analysis tool based on Petri net extensions, and PVSio-web, a prototyping toolkit based on the PVS theorem proving system.