Search

In order to support efficient compilation to modern architectures, mainstream programming languages, such as C/C++ and Java, have adopted weak (or relaxed) memory models. According to these weak memory models, multithreaded programs are allowed to exhibit behaviours that would have been inconsistent under the traditional strong (i.e., sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, developed by Turon et al. (ACM OOPSLA, pp 691-707, 2014), has made a step forward towards tackling this challenge for the release-acquire fragment of the C11 memory model. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we introduced GPS+ to support a larger class of C11 programs, that is, programs with release-acquire atomics, relaxed atomics and release-acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of new verification rules. [ABSTRACT FROM AUTHOR]

Discovering program specifications automatically for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework that would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only infer memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs. [ABSTRACT FROM AUTHOR]

Abstract: Automatically verifying heap-manipulating programs is a challenging task, especially when dealing with complex data structures with strong invariants, such as sorted lists and AVL/red–black trees. The verification process can greatly benefit from human assistance through specification annotations, but this process requires intellectual effort from users and is error-prone. In this paper, we propose a new approach to program verification that allows users to provide only partial specification to methods. Our approach will then refine the given annotation into a more complete specification by discovering missing constraints. The discovered constraints may involve both numerical and multi-set properties that could be later confirmed or revised by users. We further augment our approach by requiring partial specification to be given only for primary methods. Specifications for loops and auxiliary methods can then be systematically discovered by our augmented mechanism, with the help of information propagated from the primary methods. Our work is aimed at verifying beyond shape properties, with the eventual goal of analysing full functional properties for pointer-based data structures. Initial experiments have confirmed that we can automatically refine partial specifications with non-trivial constraints, thus making it easier for users to handle specifications with richer properties. [Copyright &y& Elsevier]

Abstract: Automated verification of memory safety and functional correctness for heap-manipulating programs has been a challenging task, especially when dealing with complex data structures with strong invariants involving both shape and numerical properties. Existing verification systems usually rely on users to supply annotations to guide the verification, which can be cumbersome and error-prone by hand and can significantly restrict the usability of the verification system. In this paper, we reduce the need for some user annotations by automatically inferring loop invariants over an abstract domain with both shape and numerical information. Our loop invariant synthesis is conducted automatically by a fixed-point iteration process, equipped with newly designed abstraction mechanism, together with join and widening operators over the combined domain. We have also proven the soundness and termination of our approach. Initial experiments confirm that we can synthesise loop invariants with non-trivial constraints. [Copyright &y& Elsevier]

Binary type inference is a challenging problem due partly to the fact that during the compilation much type-related information has been lost. Most existing research work resorts to program analysis techniques, which can be either too heavyweight to be viable in practice or too conservative to be able to infer types with high accuracy. In this paper, we propose a new approach to learning types for binary code. Motivated by “duck typing,” our approach learn types for recovered variables from their features and properties (e.g., related representative instructions). We first use machine learning to train a classifier with basic types as its levels from binaries with debugging information. The classifier is then used to learn types for new and unseen binaries. While for composite types, such as ${pointer}$ and ${struct}$ , a points-to analysis is performed. Finally, several experiments are conducted to evaluate our approach. The results demonstrate that our approach is more precise, both in terms of correct types and compatible types, than the commercial tool Hex-Rays, the open source tool Snowman, and a recent tool EKLAVYA using machine learning. We also show that the type information our proposed system learns is capable of helping detect malware. [ABSTRACT FROM AUTHOR]

Hybrid Event-B, initially introduced for single machines to add continuously varying behaviour to discrete change of state in Event-B, is extended to cater for multiple cooperating machines. Multiple machine working is mediated by INTERFACE and PROJECT constructs. The former encapsulates a set of variables, their invariants and initialisations, in a form that several machines can exploit simultaneously. The latter organises the set of cooperating machines and interfaces into a coherent system. Machine instantiation and composition via interfaces are discussed. Machine decomposition is explored in this framework. Multi-machine refinement is described. A hypergraph project architecture is proposed. Two small case studies, on power switching and on the European Train Control System (the latter treated earlier within the single machine formalism), illustrate these mechanisms. The semantics of interacting multi-machine systems is described, and proof obligations that ensure correctness are covered. [ABSTRACT FROM AUTHOR]

Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specified by a combination of indirect specification via ordinary differential equations, or direct specification via assignment of variables to values that depend on time, or indirect specification by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Refinement is examined in detail, with reference to the notion of refinement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge — bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin) — is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B. [ABSTRACT FROM AUTHOR]

As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It also has real-time and shared-variable features. Previously we have studied an operational semantics for SystemC Peng et al. (An operational semantics of an event-driven system-level simulator, pp 190-200, ) and bisimulation has been introduced based on some aspects of reasonable abstractions. The denotational method is another approach to studying the semantics of a programming language. It provides the mathematical meaning to programs and can predict the behaviour of programs. Due to the novel features of SystemC, it is challenging to study the denotational semantics for SystemC. In this paper, we apply Unifying Theories of Programming (abbreviated as UTP) Hoare and He (Unifying theories of programming, ) in exploring the denotational semantics. Two trace variables are introduced, one to record the state behaviours and another to record the event behaviours. The timed model is formalized in a threedimensional structure. A set of algebraic laws is explored, which can be proved via the presented denotational semantics. In this paper, we also consider the linking between denotational semantics and algebraic semantics. The linking is obtained by deriving the denotational semantics from algebraic semantics for SystemC. A complete set of parallel expansion laws is explored, where the location status of an instantaneous action is studied. The location status indicates an instantaneous action is due to which exact parallel component. We introduce the concept of head normal form for each program and every program is expressed in the form of guarded choice with location status. Based on this, the derivation strategy for deriving denotational semantics from algebraic semantics is provided. [ABSTRACT FROM AUTHOR]

Conventional specifications typically have a flat structure that is based primarily on the underlying logic. Such specifications lack structures that could provide better guidance to the verification process. In this work, we propose to add three new structures to a specification framework for separation logic to achieve a more precise and better guided verification for pointer-based programs. The newly introduced structures empower users with more control over the verification process in the following ways: (1) case analysis can be invoked to take advantage of disjointedness conditions in the logic, (2) early, as opposed to late, instantiation can minimise the use of existential quantification and (3) novel formulae structuring can provide better reuse of the verification process. Initial experiments have shown that structured specifications can lead to more precise verification without incurring any performance overhead. To support our proposal, we shall illustrate the usage of structured specifications in the context of proving termination and we will briefly outline the impact of our proposal on a recent development focussed on verifying the FreeRTOS scheduler Ferreira et al. (Int. J. Softw. Tools Technol. Trans. ). [ABSTRACT FROM AUTHOR]

Abstract: We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specification in separation logic, where the program contains calls to some unknown procedure , we infer a specification for the unknown procedure from the calling contexts. We show that the problem of verifying the program against the specification can be safely reduced to the problem of proving that the procedure (once its code is available) meets the derived specification . The expected specification for the unknown procedure is automatically calculated using an abduction-based shape analysis. We have also implemented a prototype system to validate the viability of our approach. Preliminary results show that the specifications derived by our tool fully capture the behaviors of the unknown code in many cases. [Copyright &y& Elsevier]

Influence maximization is a fundamental research problem in social networks. Viral marketing, one of its applications, aims to select a small set of users to adopt a product, so that the word-of-mouth effect can subsequently trigger a large cascade of further adoption in social networks. The problem of influence maximization is to select a set of K nodes from a social network so that the spread of influence is maximized over the network. Previous research on mining top- K influential nodes assumes that all of the selected K nodes can propagate the influence as expected. However, some of the selected nodes may not function well in practice, which leads to influence loss of top- K nodes. In this paper, we study an alternative influence maximization problem which is naturally motivated by the reliability constraint of nodes in social networks. We aim to find top- K influential nodes given a threshold of influence loss due to the failure of a subset of R (< K ) nodes. To solve the new type of influence maximization problem, we propose an approach based on constrained simulated annealing and further improve its performance through efficiently estimating the influence loss. We provide experimental results over multiple real-world social networks in support. This research will further support practical applications of social networks in various domains particularly where reliability would be a main concern in a system deployment. [ABSTRACT FROM AUTHOR]

Automated verification of operating system kernels is a challenging problem, partly due to the use of shared mutable data structures. In this paper, we show how we can automatically verify memory safety and functional correctness properties of the task scheduler component of the FreeRTOS kernel using the verification system Hip/Sleek. We show how some of Hip/Sleek features such as user-defined predicates and lemmas make the specifications highly expressive and the verification process viable. To the best of our knowledge, this is the first code-level verification of memory safety and functional correctness properties of the FreeRTOS scheduler. The outcome of our experiment confirms that Hip/Sleek can indeed be used to verify code that is used in production. Moreover, since the properties that we verify are quite general, we envisage that the same approach can be adopted to verify components of other operating systems. [ABSTRACT FROM AUTHOR]

Abstract: Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In this paper, we propose an automated verification system for ensuring the safety of pointer-based programs, where specifications handled are concise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded predicates (that may be recursively defined) using unfold/fold reasoning. We have proven the soundness and termination of our verification system and built a prototype system to demonstrate the viability of our approach. [Copyright &y& Elsevier]

Abstract: Complex software systems typically involve features like time, concurrency and probability, with probabilistic computations playing an increasing role. However, it is currently challenging to formalize languages incorporating all those features. Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. (2006, 2009) ), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC, highlighting both its theoretical and practical aspects. The link is obtained by deriving the operational semantics from the algebraic semantics, an approach that may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws are provided that suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from the algebraic semantics, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operational semantics with respect to the algebraic semantics. That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, the generation of head normal form is explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy that exploits head normal form. The operational semantics is also animated. These animations, which again supports to claim soundness and completeness of the operational semantics with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results. [Copyright &y& Elsevier]

This paper proposes a multimodal deep learning method for forecasting the daily power generation of small hydropower stations that considers the temporal and spatial distribution of precipitation, which compensates for the shortcomings of traditional forecasting methods that do not consider differences in the spatial distribution of precipitation. First, the actual precipitation values measured by ground weather stations and the spatial distribution of precipitation observed by meteorological satellite remote sensing are used to complete the missing precipitation data through linear interpolation, and the gridded precipitation data covering a group of small hydropower stations are constructed. Then, considering the time lag between changes in the daily power generation of the group of small hydropower stations and precipitation, the partial mutual information method is used to estimate the "time difference" between the two, and combined with the precipitation grid data, a data set of the temporal and spatial distribution of precipitation is generated. Finally, using only the temporal and spatial distribution of precipitation and historical power generation data, a multimodal deep learning network based on a convolutional neural network (CNN) and multilayer perceptron (MLP) is constructed, and a highly accurate prediction model for the daily power generation of small hydropower stations is obtained. Taking the real power generation data of a group of small hydropower stations in southern China as an example, after considering the temporal and spatial distribution of precipitation, the prediction accuracy of the proposed method is as high as 93%, which is approximately 5.8% higher than before considering the temporal and spatial distribution of precipitation. In addition, compared with mainstream methods such as support vector regression (SVR) and the long–short-term memory network (LSTM) (the average accuracy is about 87%), and the average accuracy improvement of the proposed method is approximately 6%. [ABSTRACT FROM AUTHOR]

Abstract: The POSIX threads (Pthreads) library is a thread API for C/C++ to control parallel threads and spawn concurrent process flows. Programming in Pthreads usually suffers from undesirable deadlock, data race, and race condition problems due to the potential nondeterministic execution behaviors between parallel threads. Dthreads, as another multithreading model that re‐implements Pthreads, was proposed by Liu et al for efficient deterministic multithreading. They found out that, under specific test cases, Dthreads can effectively prevent data races. However, no comparison test has been made with Pthreads. To perform a formal comparison between Pthreads and Dthreads over deadlocks, data races, and race conditions, in this paper, we adopt CSP (communicating sequential processes) as a formal model for specifying part of API functions in Pthreads and Dthreads and illustrate the model construction using 4 classical example programs. By feeding the models into the model checker PAT (process analysis toolkit), we have verified that deadlocks and data races exist in Pthreads, but do not exist in Dthreads, for the considered programs. We have also found that neither of them can prevent race conditions. Our comparative modelling and verification of Pthreads and Dthreads show that though Dthreads cannot prevent all the deadlock situations, shown by verification results of another 2 example programs, Dthreads is better than Pthreads on eliminating data races and preventing deadlocks. Considering limited scalability of Dthreads, we have introduced a new programming model to support coarse granularity in bank transfer. Our modelling is also extended by covering the synchronization operations in Liu et al work. [ABSTRACT FROM AUTHOR]