ABSTRACT. Ciao is a logic programming language which was designed from the root to be extensible, support multiparadigm features, and provide the flexibility of a dynamic language, but with guaranteed safety, reliability, and efficiency. A key component of Ciao is its preprocessor (CiaoPP), a context-sensitive, abstract interpretation-based analyzer based on inferring via fixpoint computation the abstract program semantics, over a set of user-definable abstract domains.

In this talk I will introduce the Ciao/CiaoPP approach, and recent results on the use of assertions to guide such fixpoint computations, incremental and modular analysis, optimization of run-time checks and static analysis of their cost, combination with automated testing, as well as other applications like semantic code search, multilanguage analysis based on transforming both high- and low-level program representations into Horn clauses, or energy consumption verification.

Short bio: Jose F. Morales holds a PhD in Cs from the Technical University of Madrid (UPM). He is a member of the CLIP group at UPM and researcher at the IMDEA Software Institute. His main research interests are logic programming, compilers, and program analysis and verification.

ABSTRACT. Performing formal verification of concurrent systems involves partial order logics (here MSO with partial orders) for the specification of properties or of the concurrent system itself. A common structure for the verification of concurrent systems is the structure so-called pomset. A pomset is a multiset of partially ordered events. The partial order relation describes causal dependencies of events. We propose a new word based model, so-called Pre-Post-Pomset, making the exploration of pomsets space possible. In this paper, our new model stands to be a general model in the sense that some classical models used in the specification of concurrent systems (Synchronized product of systems, Mazurkiewicz traces or parallel series) can be specified within. Not only is our model general but also offers decidability results on the verification problem according to an MSO formula on pomsets.

ABSTRACT. HTML5-based mobile apps are developed using the standard web technologies such as HTML5, CSS, JavaScript, so they may also face with event-based races like web apps. However, HTML5-based mobile apps have a variety of asynchronous events compared with web apps, and such events are supported by a middleware framework for building hybrid mobile apps. For example, PhoneGap framework supports the lifecycle events for signaling states of an app like Android’s lifecycle and the asynchronous events for interacting with the platform resources such as contact, SMS, etc. When those events fire, it can generate nondeterministic execution orders of the corresponding event handlers. Those nondeterminisms may cause data races among the fired events. In this paper, we present event-based races in HTML5-based mobile apps that are caused by the asynchronous events of a middleware framework. Moreover, we propose a semi-automated approach combining data flow analysis with manual code inspection for race detection. To evaluate its effectiveness, we conducted the experiments for detecting how many detected races on a dataset of 1,926 HTML5-based mobile apps. Eventually, it flagged 18 vulnerable apps. We manually inspected such vulnerable apps and identified 21 true races.

ABSTRACT. Geometric-Zeno behaviour is one of the most challenging problems in the analysis and simulation of hybrid systems. Geometric-Zeno solutions involve an accumulation of an infinite number of discrete events occurring in a finite amount of time. In models that exhibit geometric-Zeno, discrete events occur at an increasingly smaller distance in time, converging to a limit point according to a geometric series. In practice, simulating a geometric-Zeno hybrid system is highly challenging, in that the simulation either halts or produces faulty results, as the time interval lengths are decreasing to arbitrary small positive numbers. Although many simulation tools for hybrid systems have been developed in the past years, none of them have a Zeno-free semantic model. All of them produce faulty results when simulating geometric-Zeno models. In this paper, we propose a new non-standard Zeno-free mathematical formalism for detecting and eliminating geometric-Zeno. We derive sufficient conditions for the existence of geometric-Zeno behaviour based on the existence of a non-standard contraction map in a complete metric space. We also provide methods for carrying solutions from pre-Zeno to post-Zeno. We illustrate the concepts with examples throughout the paper.

ABSTRACT. Whereas correctness preservation is considered as the gold standard of software engineering processes, in this talk we argue that in fact the vast majority of software engineering processes do not involve correctness preservation but rather correctness enhancement. We explore some mathematics of correctness enhancement, discuss in what way and to what extent correctness correctness enhancement pervades software engineering, and tentatively speculate about prospects for using these insights to enhance software engineering practice

ABSTRACT. In this paper, we present a methodology for analysing security protocols using scenario based simulation. A scenario of a potential attack specifies the flow but not the content of messages. Using scenarios can reduce the number of protocol runs to be explored during attack searching via simulation. The number of runs can be further reduced by minimizing the number of intruder's generated messages. The intruder's ability to generate messages is limited by considering: the expected message content and type matching. Our approach uses two tools that support the Abstract State Machines method: the AsmetaL for modelling purposes and the AsmetaS for performing the simulation. We propose a simple model for the specification of commutative encryption. Several protocols are examined to show the effectiveness of our method.

ABSTRACT. Gas is a measurement unit of the computational effort that it will take to execute every single replicated operation that takes part in the Ethereum blockchain platform. Each transactions involving such operations, executed by involved distributed parties via the Ethereum Virtual Machine (EVM), has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised, interrupting the current execution. While designed to solve potential denial-of-service attacks, this cost-instrumented computational model of Ethereum has also brought new wide family of contract-specific vulnerabilities due to out-of-gas behaviours, leading to potential exploits and monetary losses.

This paper presents, to the best of our knowledge, the first static analysis that is able to infer parametric gas bounds for smart contracts. The inferred bounds are typically parametric on the sizes of the input parameters for the functions, but also they are often parametric on the contract state, and even sometimes they will be parametric on blockchain data. The analysis is implemented in a tool named GASTAP, Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers sound gas upper bounds for all its public functions, or for the selected functions. Our soundly inferred bounds can be used to prevent out-of-gas vulnerabilities: the bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas exceptions.

ABSTRACT. This paper presents an approach to support multiple permanent node failures in multicore real time systems. The used scheduling algorithm in the absence of failures is the PFair algorithm PD2 which create an optimal schedule in polynomial time. A core defection leads to the reduction of the processing capacity and possibly to an overload on the remaining cores. This can causes temporal faults and thus desastrous consequences for safety critical systems. To overcome this issue, a single spare core is provided and two protocols are defined: The Recovery Time Distribution Protocol (RTDP) and the Graceful Degradation Protocol (GDP). When a single core fails, RTDP set the system parameters such that all the tasks still meet their deadlines, although after a bounded delay. When multiple cores fail, GDP defines several modes corresponding to degraded execution. The modes differ depending on task importance. Different heuristics are defined to decide on which tasks are dropped in degraded modes. The experimentation of the two protocols shows conclusive results. Tasks recover from the failure in a bounded delay with RTDP whereas there are some missed deadlines with GDP. However, we exploit the experimental results to guide the designer on which task elimination strategy to use depending on the system characteristics.

ABSTRACT. Synchronous Dataflow Graph (SDFG) is a formal tool widely used to model and analyze the behaviour of systems constrained by tim- ing requirements. It has been successfully used in digital signal process- ing and manufacturing fields to specify and analyze the performance of embedded and distributed applications. Various performance indicators such as throughput, latency or memory consumption can be evaluated using SDFGs. This paper tackles the latency analysis for SDFG using the periodic schedules.