Abstract
A central issue in program verification is the generation of verification conditions (VCs): proof obligations which, if successfully discharged, guarantee the correctness of a program vis-a-vis a given specification. While the basic theory of program verification has been around since the 1960s, the late 1990s saw the advent of practical tools for the verification of realistic programs, and research in this area has been very active since then. Automated theorem provers have contributed decisively to these developments. This paper establishes a basis for the generation of verification conditions combining forward and backward reasoning, for programs consisting of mutually-recursive procedures annotated with contracts and loop invariants. We introduce also a visual technique to verify a program, in an interactive way, using Verification Graphs (VG), where a VG is a Control Flow Graph (CFG) whose edges are labeled with contracts (pre- and postconditions). This technique intends to help a software engineer to find statements that are not valid with respect to the program's specification.

Abstract
Searching for resources over unstructured networks is usually supported by broadcast communication primitives. Ideally, the broadcast process should be cancelled as soon as possible after a successful discovery, to avoid flooding the entire network. However, cancelling an ongoing broadcast is challenging and may increase the number of exchanged messages. In this paper, we compare the cancellation mechanisms used by BERS and BERS^* with new proposed cancellation approaches BCIR and BCIR^*. The formulation of a simplified analytical model and the simulation results show that: i) it is possible to reduce the number of retransmitted messages, without increasing the latency observed in BERS^*; and ii) BCIR is more energy efficient, which can contribute to extend the availability of mobile battery powered devices. Copyright 2013 ACM.

Abstract
Distributed Computing is becoming more and more led by technological and application advances. Many works consider new computing models compared to the classical closed model with a fixed number of participants and strong hypothesis on communication and structuration. Indeed, it is hard to imagine some application or computational activity and process that falls outside Distributed Computing. Internet and the web (e.g. social networks, clouds) are becoming the main application field for distributed computing. In addition to the classical challenges that developers have to face (asynchrony and failures) they have to deal with load balancing, malicious and selfish behaviors, mobility, heterogeneity and the dynamic nature of participating processes. © 2013 Springer-Verlag.

Abstract

Abstract
The aggregation and estimation of values over networks is fundamental for distributed applications, such as wireless sensor networks. Estimating the average, minimal and maximal values has already been extensively studied in the literature. In this paper, we focus on estimating empirical distributions of values in a network with anonymous agents. In particular, we compare two different estimation strategies in terms of their convergence speed, accuracy and communication costs. The first strategy is deterministic and based on the average consensus protocol, while the second strategy is probabilistic and based on the max consensus protocol.

Abstract
In order to further improve the performance of current genetic algorithms aiming at discovering communities, a local search based genetic algorithm (GALS) is here proposed. The core of GALS is a local search based mutation technique. In order to overcome the drawbacks of traditional mutation methods, the paper develops the concept of marginal gene and then the local monotonicity of modularity function Q is deduced from each node's local view. Based on these two elements, a new mutation method combined with a local search strategy is presented. GALS has been evaluated on both synthetic benchmarks and several real networks, and compared with some presently competing algorithms. Experimental results show that GALS is highly effective and efficient for discovering community structure.