Abstract
Among many theories supported by SMT solvers, the theory of finite-precision bit-vector arithmetic is one of the most useful, for both hardware and software systems verification. This theory is also particularly useful for some specific domains such as cryptography, in which algorithms are naturally expressed in terms of bit-vectors. Cryptol is an example of a domain-specific language (DSL) and toolset for cryptography developed by Galois, Inc.; providing an SMT backend that relies on bit-vector decision procedures to certify the correctness of cryptographic specifications [3]. Most of these decision procedures use bit-blasting to reduce a bit-vector problem into pure propositional SAT. Unfortunately bit-blasting does not scale very well, especially in the presence of operators like multiplication or division. © 2012 Springer-Verlag.

Abstract

Abstract
This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (a) a precise test for removable statements, and (b) the construction of a slice graph, a program control flow graph extended with semantic labels and additional edges that "short-circuit" removable commands. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions.

Abstract
A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this paper we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas. © 2012 ACM.

Abstract
This paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automatically extracts from an Ada program a SPIN model, together with a set of desirable properties. ATOS is also capable of extracting properties from a specification annotated by the user in the program, inspired by the SPARK Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada programs, based on model checking. © 2012 Springer-Verlag.

Abstract
Broadcast is a communication primitive building block widely used in mobile ad-hoc networks (MANETs) for the exchange of control packets and resource location for upper level services such as routing and management protocols. Flooding is the most simple broadcast algorithm, but it wastes a lot of energy and bandwidth, as flooding leads to many redundant radio transmissions. An optimization to flooding is to contain it, once the resource has been found. In this paper, we compare the impact on the latency and power consumption of four competing approaches for flooding containment. The results show that stopping ongoing broadcasts can achieve promising performance increases over other flooding base techniques, when applied in large scale MANETs with scarce power resources. In addition, results show that both network topology and the number of copies of the resource influence differently the performance of each searching approach. © 2012 ACM.