Abstract
Invariants, bisimulations and assertions are the main ingredients of coalgebra theory applied to software systems. In this paper we reduce the first to a particular case of the second and show how both together pave the way to a theory of coalgebras which regards invariant predicates as types. An outcome of such a theory is a calculus of invariants' proof obligation discharge, a fragment of which is presented in the paper. The approach has two main ingredients: one is that of adopting relations as "first class citizens" in a pointfree reasoning style; the other lies on a synergy found between a relational construct, Reynolds' relation on functions involved in the abstraction theorem on parametric polymorphism and the coalgebraic account of bisimulations and invariants. This leads to an elegant proof of the equivalence between two different definitions of bisimulation found in coalgebra literature (due to B. Jacobs and Aczel & Mendler, respectively) and to their instantiation to the classical Park-Milner definition popular in process algebra.

Abstract
This paper presents a transient stability preventive control technique based on a hybrid method. In order to maintain the power system security it is evaluated the generators output power that should be shift from the most unstable synchronous machines to the undisturbed units. The reallocation of the generators output power is carried out using an optimal power flow program. The hybrid method is a very important tool for the transient stability analysis, since it allows a fast evaluation of the stability limits and margins. This approach can also easily accommodate detailed models of the network devices and protective schemes. In order to validate the established mathematical models it was studied the transient stability of the New England test power network. The results obtained with the proposed methodology were compared with the solutions produced by another numerical formulation, showing a very close agreement.

Abstract
A test technique for capacitive MEMS accelerometers and electrostatic microactuators, based on the measurement of pull-in voltages and resonance frequency, is described. Using this combination of measurements, one can estimate process-induced variations in the device layout dimensions as well as deviations from nominal value in material properties, which can be used either for testing or device diagnostics purposes. Measurements performed on fabricated devices confirm that the 250nm overetch observed on SEM images can be correctly estimated using the proposed technique.

Abstract
This work studies dual-band EBG structures used as an Artificial Magnetic Conductor (AMC) ground plane for WLAN co-planar antenna to achieve a low profile structure. From the simulation results, the EBG surface geometry with Jerusalem Cross (JCSS) slot has been chosen in this study. A dual band prototype operating at 2.4 and 5.2 GHz has been implemented and tested. The results show that the EBG antenna can work properly at desired frequency bands with improved gain and reduced back lobe. ©2008 IEEE.

Abstract
This paper evaluates and compares different network generators to generate project scheduling problem instances based on indicators measuring the topological network structure. We review six topological network indicators in order to describe the detailed structure of a project network. These indicators were originally developed by [L.V. Tavares, J.A. Ferreira and J.S. Coelho, The risk of delay of a project in terms of the morphology of its network, European Journal of Operational Research 119 (1999), 510-537] and have been modified, or sometimes completely replaced, by alternative indicators to describe the network topology. The contribution of this paper is twofold. Firstly, we generate a large amount of different networks with four project network generators. Our general conclusions are that none of the network generators are able to capture the complete feasible domain of all networks. Additionally, each network generator covers its own network-specific domain and, consequently, contributes to the generation of data sets. Secondly, we perform computational results on the well-known resource-constrained project scheduling problem to prove that our indicators are reliable and have significant, predictive power to serve as complexity indicators.

Abstract
Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Calculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed. Copyright © 2008 ACM.