Titlebook: Software Engineering and Formal Methods; 10th International C George Eleftherakis,Mike Hinchey,Mike Holcombe Conference proceedings 2012 Sp

北极熊

Judicious

Checking Sanity of Software Requirements on the fact that functional requirements can be expressed in temporal logic and we propose new techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate new approaches to consistency and vacuity checking that ide

Aesthete

TVAL+ : TVLA and Value Analyses Togetherined great achievements in the field of heap abstraction. Similarly, numerical and other value abstractions have made tremendous progress, and they are effectively applied to the analysis of industrial software. In addition, several generic static analyzers have been introduced. These compositional

Apraxia

荧光

Compositional Reasoning about Shared Futurestion mechanisms. The . extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed enviro

hereditary

Verification of Aspectual Composition in Feature-Modelingning families of these systems to address issues with the crosscutting concerns, such as security concerns, is recognised to be tedious and costly. To tackle the above problem, we adapt the aspect-oriented paradigm to feature-modeling..One of the most serious problems in aspect-oriented modeling is

Psychogenic

A Denotational Model for Instantaneous Signal Calculuss reactions of signal calculus for event-based synchronous languages. The healthiness conditions are studied for especially dealing with the emission of signals. Every instantaneous reaction can be identified as denoting a healthiness function over the set of events which describe the state of the s

CHIDE

鞭打

Towards a Formal Component Model for the Clouddeployed on clusters of heterogeneous (virtual) machines that can be created and connected on-the-fly. We introduce the Aeolus component model to capture similar scenarii from realistic cloud deployments, and instrument automated planning of day-to-day activities such as software upgrade planning, s

改良

The Rely/Guarantee Approach to Verifying Concurrent BPEL Programson. It contains several distinct features, including scope-based compensation and fault handling mechanism. This paper focuses on the verification of BPEL programs, especially the verification of concurrent BPEL programs. The rely/guarantee approach is applied. Firstly, we present the operational se