In the design of symbolic mathematical computation systems, it is a popular choice to use the same syntax for both mathematical indeterminates and programming variables. While mathematical indeterminates are to be use...
详细信息
ISBN:
(纸本)9781665465458
In the design of symbolic mathematical computation systems, it is a popular choice to use the same syntax for both mathematical indeterminates and programming variables. While mathematical indeterminates are to be used without specific values, programming variables must be initialized before being used in expressions. A problem occurs when mistakenly uninitialized programming variables are silently taken to be mathematical indeterminates. this article explores how this problem can arise and its consequences. An algorithm to analyze programs for this defect is shown along with a Maple implementation.
Service oriented architectures become more and more popular withthe emergence and consolidation of new paradigms such as Clouds and Grids. In this context scheduling becomes an important and difficult problem as serv...
详细信息
ISBN:
(纸本)9780769539645
Service oriented architectures become more and more popular withthe emergence and consolidation of new paradigms such as Clouds and Grids. In this context scheduling becomes an important and difficult problem as services hide their actual implementation, requirements or efficiency and are spread across multiple institutions and geographical locations. this paper proposes a distributed scheduling approach based on agents where each agent handles a certain domain and manages independently the policies inside it. In its frame several scheduling algorithms are also studied, compared and some results are given.
As an extension of our previous work on imperative program verification, we present a formalism for handling the total correctness of While loops in imperative programs, consisting in functional based definitions of t...
详细信息
ISBN:
(纸本)9780769539645
As an extension of our previous work on imperative program verification, we present a formalism for handling the total correctness of While loops in imperative programs, consisting in functional based definitions of the verification conditions for both partial correctness and for termination. A specific feature of our approach is the generation of verification conditions as first order formulae, including the termination condition which is expressed as an induction principle.
Satisfiability Checking is a relatively young research area, aiming at the development of efficient software technologies for checking the satisfiability of existentially quantified logical formulas. Besides the succe...
详细信息
ISBN:
(纸本)9781509057078
Satisfiability Checking is a relatively young research area, aiming at the development of efficient software technologies for checking the satisfiability of existentially quantified logical formulas. Besides the success story of SAT solving for propositional logic, SAT-modulo-theories (SMT) solvers offer sophisticated solutions for different theories. When targeting arithmetic theories, SMT solvers also make use of decision procedures rooted in symbolic Computation. In this paper we give a brief introduction to SMT solving, discuss differences to symbolic Computation, and illustrate the potentials and obstacles for embedding symbolic Computation techniques in SMT solving on the example of the Cylindrical Algebraic Decomposition.
the investigation of biological dynamics involves many interesting aspects such as abstraction, modelling and simulation, but a very important aspect to consider is the representation of such dynamics. A correct, flex...
详细信息
ISBN:
(纸本)0769524532
the investigation of biological dynamics involves many interesting aspects such as abstraction, modelling and simulation, but a very important aspect to consider is the representation of such dynamics. A correct, flexible and formal representation mechanism of interesting behaviours is the right starting point for all successive modelling steps and it can be helpful in capturing the essence of the system under investigation. In particular, provided a formal representation of the relevant traits of biological systems behaviours, the application of P systems, to their modelling can become more and more fruitful. For this reason, here we present a formalism allowing us to represent biological oscillations by means of strings composed by parametric words that we call beats.
Resource identification in massive deployed distributed systems, like the cloud environments, is a common problem when multiple types of resources need to be managed. this is the case of platform as a service (PaaS) w...
详细信息
ISBN:
(纸本)9781479930357
Resource identification in massive deployed distributed systems, like the cloud environments, is a common problem when multiple types of resources need to be managed. this is the case of platform as a service (PaaS) where the platform offers different types resources that are deployed in heterogeneous systems. While most of the solutions on the market follow a predefined architecture using common naming services in a centralized manner this paper proposes a new approach based on a distributed naming and resource identification service. the proposed solution allows a client to consume or communicate with a resource without having to deal with resource location or discovery protocols.
Modern program analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using logic for describing states and transformations between...
详细信息
ISBN:
(纸本)9780769539645
Modern program analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using logic for describing states and transformations between system states. the system Z3, developed at Microsoft Research, is a Satisfiability Modulo theories (SMT) solver. It provides logic inference capabilities that are critical for the functionality of these systems. the tutorial exemplifies a number of applications of Z3 at Microsoft.
We define a new bio-inspired computational model for deciding 2-dimensional languages that is directly derived from the one in [13]. the described model has a slightly different accepting protocol as the previous one ...
详细信息
ISBN:
(纸本)9781538626269
We define a new bio-inspired computational model for deciding 2-dimensional languages that is directly derived from the one in [13]. the described model has a slightly different accepting protocol as the previous one and, besides the deletion and substitution operations, we now consider a new type of operation, namely circular permutation. We show that by using circular permutations, such networks can recognize any input that contains a given sub-picture as where our previous model limited one of the pattern dimensions to a size of at most 3.
the strong convergence properties of the projection method for convex feasibility problem are investigated in the frame of a real Hilbert space. the significant role of the regularity properties for strong convergence...
详细信息
ISBN:
(纸本)9780769530789
the strong convergence properties of the projection method for convex feasibility problem are investigated in the frame of a real Hilbert space. the significant role of the regularity properties for strong convergence of these methods is pointed out.
Computational simulation is an important research tool for modern scientists. there are a range of different scales of high performance computing (HPC) resources available to scientists, from laptop and desktop machin...
详细信息
ISBN:
(纸本)9781479930357
Computational simulation is an important research tool for modern scientists. there are a range of different scales of high performance computing (HPC) resources available to scientists, from laptop and desktop machines, to small institutional clusters, to national HPC resources, and the largest parallel computers in the world. this paper outlines the challenges that developers and users face moving from small scale computational resources to larger scale parallel machines. We present an overview of various research efforts to improve performance on large scale systems to enable users and developers to gain an understanding of the performance issues often encountered by simulation codes.
暂无评论