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 post conditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for removable statements, and (ii) the construction of a slice graph, a program control flow graph extended with semantic labels. 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). The paper also reviews in detail, through examples, the ideas behind the use of preconditions and post conditions for slicing programs. © 2010 IEEE.

Abstract
This paper has two purposes: first, to describe an experiment made in an undergraduate course, using Internet services to improve the speed and ease of communication between students and teaching team. We claim that the very positive results we obtained may very easily be reproduced in any course, with undergraduate students from the first year on. The second purpose is to discuss some possible directions the authors are planning to follow, in what concerns the utilization of Internet in education. Virtual environments such as MUDs and the automatic marking-up of problems submitted through WWW forms are steps towards what might end up as a full-blown Distance Education Environment.

Abstract
We describe the MPINE tool, a multi-threaded evaluator for Interaction Nets. The evaluator is an implementation of the present author's Abstract Machine for Interaction Nets [5] and uses POSIX threads to achieve concurrent execution. When running on a multi-processor machine (say an SMP architecture), parallel execution is achieved effortlessly, allowing for desktop parallelism on commonly available machines. © Springer-Verlag Berlin Heidelberg 2001.

Abstract
In software development, it is often desirable to reuse existing software components. This has been recognized since 1968, when Douglas Mcllroy of Bell Laboratories proposed basing the software industry on reuse. Despite the failures in practice, many efforts have been made to make this idea successful. In this context, we address the problem of reusing annotated components as a rigorous way of assuring the quality of the application under construction. We introduce the concept of caller-based slicing as a way to certify that the integration of an annotated component with a contract into a legacy system will preserve the behavior of the former. To complement the efforts done and the benefits of the slicing techniques, there is also a need to find an efficient way to visualize the annotated components and their slices. To take full profit of visualization, it is crucial to combine the visualization of the control/ data flow with the textual representation of source code. To attain this objective, we extend the notion of System Dependence Graph and slicing criterion.

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
In this poster we describe a work in progress aimed at using a variant of specification-based slicing to improve the reuse of annotated software components, developed under the so called design-by-contract approach. We have named this variant as contract-based because we use the annotations, more precisely the pre and post-conditions, to slice programs intra and inter-procedures. The idea, expressed in the poster, is to take the pre-condition of the reused annotated component as slicing criterion, and slice backward the program where the component is called. In that way, we can isolate the statements that have influence on the variables involved on the pre-condition and check if it is preserved by that invocation, or not. © 2010 IEEE.