Abstract
Lightweight formal methods ought to provide to the end user the rigorousness of mathematics, without compromising simplicity and intuitiveness. Alloy is a powerful tool, particularly successful on this mission. Limitations on the verification side, however, are known to prevent its wider use in the development of safety or mission critical applications. A number of researchers proposed ways to connect Alloy to other tools in order to meet such challenges. This paper's proposal, however, is not establishing a link from Alloy to another single tool, but rather to 'plunge' it into the Hets network of logics, logic translators and provers. This makes possible for Alloy specifications to 'borrow' the power of several, non dedicated proof systems. Semantical foundations for this integration are discussed in detail. © 2013 IEEE.

Abstract
This paper presents the encoding of the hybridisation method proposed in [MMDB11, DM13] into the Hets platform. © 2013 Springer-Verlag Berlin Heidelberg.

Abstract
As a complex artefact, software has to meet requirements formulated and verified at different levels of abstraction. A basic distinction is drawn between behavioural (dynamic) and data (static) aspects. From an educational point of view, although disguised under a number of different designations, both issues are usually present, but kept separated, in typical Computer Science undergraduate curricula. It is often argued that they tackle orthogonal problems through essentially different methods. This paper explores an alternative path in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.

Abstract
Lightweight formal methods, of which Alloy is a prime example, combine the rigour of mathematics without compromising simplicity of use and suitable tool support. In some cases, however, the verification of safety or mission critical software entails the need formore sophisticated technologies, typically based on theorem provers. This explains a number of attempts to connect Alloy to specific theorem provers documented in the literature. This chapter, however, takes a different perspective: instead of focusing on one more combination of Alloy with still another prover, it lays out the foundations to fully integrate this system in the Hets platform which supports a huge network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. The chapter extends the authors’ previous work on this subject by developing in full detail the semantical foundations for this integration, including a formalisation of Alloy as an institution, and introducing a new, more general translation of the latter to second-order logic.

Abstract
This paper extends the authors' previous work on a formal approach to the specification of reconfigurable systems, introduced in [7], in which configurations are taken as local states in a suitable transition structure. The novelty is the explicit consideration that not only the realisation of a service may change from a configuration to another, but also the set of services provided and even their functionality, may themselves vary. In other words, interfaces may evolve, as well.

Abstract
The original purpose of component-based development was to provide techniques to master complex software, through composition, reuse and parametrisation. However, such systems are rapidly moving towards a level in which software becomes prevalently intertwined with (continuous) physical processes. A possible way to accommodate the latter in component calculi relies on a suitable encoding of continuous behaviour as (yet another) computational effect. This paper introduces such an encoding through a monad which, in the compositional development of hybrid systems, may play a role similar to the one played by 1+, powerset, and distribution monads in the characterisation of partial, nondeterministic and probabilistic components, respectively. This monad and its Kleisli category provide a universe in which the effects of continuity over (different forms of) composition can be suitably studied.