| 1. |
- Smirnova, Oxana, et al.
(författare)
-
The NorduGrid Architecture And Middleware for Scientific Applications
- 2003
-
Ingår i: Lecture Notes in Computer Science. - Berlin, Heidelberg : Springer Berlin Heidelberg. ; 2657, s. 264-273
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- The NorduGrid project operates a production Grid infrastructure in Scandinavia and Finland using own innovative middleware solutions. The resources range from small test clusters at academic institutions to large farms at several supercomputer centers, a
|
|
| 2. |
- Abel, Andreas, 1974, et al.
(författare)
-
Fixed Points of Type Constructors and Primitive Recursion
- 2004
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3210, s. 190-204
-
Tidskriftsartikel (refereegranskat)abstract
- For nested or heterogeneous datatypes, terminating recursion schemes considered so far have been instances of iteration, excluding efficient definitions of fixed-point unfolding. Two solutions of this problem are proposed: The first one is a system with equi-recursive non-strictly positive type constructors of arbitrary finite kinds, where fixed-point unfolding is computationally invisible due to its treatment on the level of type equality. Positivity is ensured by a polarized kinding system, and strong normalization is proven by a model construction based on saturated sets. The second solution is a formulation of primitive recursion for arbitrary type constructors of any rank. Although without positivity restriction, the second system embeds—even operationally—into the first one.
|
|
| 3. |
- Adams, Robin, 1978
(författare)
-
A Modular Hierarchy of Logical Frameworks
- 2004
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3085, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.
|
|
| 4. |
- Agnarsson, G., et al.
(författare)
-
Powers of geometric intersection graphs and dispersion algorithms
- 2002
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540438663 ; 2368, s. 140-149
-
Konferensbidrag (refereegranskat)abstract
- We study powers of certain geometric intersection graphs: interval graphs, m-trapezoid graphs and circular-arc graphs. We define the pseudo product, (G,G′) → G * G′, of two graphs G and G′ on the same set of vertices, and show that G*G′ is contained in one of the three classes of graphs mentioned here above, if both G and G′ are also in that class and fulfill certain conditions. This gives a new proof of the fact that these classes are closed under taking power; more importantly, we get efficient methods for computing the representation for G k if k ≥ 1 is an integer and G belongs to one of these classes, with a given representation sorted by endpoints. We then use these results to give efficient algorithms for the k-independent set, dispersion and weighted dispersion problem on these classes of graphs, provided that their geometric representations are given.
|
|
| 5. |
- Ahrendt, Wolfgang, 1967
(författare)
-
Deductive Search for Errors in Free Data Type Specifications using Model Generation
- 2002
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540439318 ; 2392, s. 211-225
-
Konferensbidrag (refereegranskat)abstract
- The presented approach aims at identifying false conjectures about free data types. Given a specification and a conjecture, the method performs a search for a model of an according counter specification. The model search is tailor-made for the semantical setting of free data types, where the fixed domain allows to describe models just in terms of interpretations. For sake of interpretation construction, a theory specific calculus is provided. The concrete rules are ‘executed’ by a procedure known as model generation. As most free data types have infinite domains, the ability of automatically solving the non-consequence problem is necessarily limited. That problem is addressed by limiting the instantiation of the axioms. This approximation leads to a restricted notion of model correctness, which is discussed. At the same time, it enables model completeness for free data types, unlike approaches based on limiting the domain size.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
The KeY System: Integrating Object-Oriented Design and Formal Methods
- 2002
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540433538 ; 2306, s. 327-330
-
Konferensbidrag (refereegranskat)abstract
- This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project1, which is aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.
|
|
| 7. |
- Altafini, Claudio, et al.
(författare)
-
Hybrid control of a truck and trailer vehicle
- 2002
-
Ingår i: Lecture Notes in Computer Science. - : Springer Berlin/Heidelberg. - 0302-9743 .- 1611-3349. - 354043321X ; 2289, s. 21-34
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- A hybrid control scheme is proposed for the stabilization of backward driving along simple paths for a miniature vehicle composed of a truck and a two-axle trailer. When reversing, the truck and trailer can be modelled as an unstable nonlinear system with state and input saturations. Due to these constraints the system is impossible to globally stabilize with standard smooth control techniques, since some initial states necessarily lead to that the so called jack-knife locks between the truck and the trailer. The proposed hybrid control method, which combines backward and forward motions, provide a global attractor to the desired reference trajectory. The scheme has been implemented and successfully evaluated on a radio-controlled vehicle. Results from experimental trials are reported.
|
|
| 8. |
- Ambroladze, Amiran, et al.
(författare)
-
When is small beautiful?
- 2003
-
Ingår i: Lecture Notes in Computer Science (Learning Theory and Kernel Machines). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540407201 ; 2777, s. 729-730
-
Konferensbidrag (refereegranskat)abstract
- The basic bound on the generalisation error of a PAC learner makes the assumption that a consistent hypothesis exists. This makes it appropriate to apply the method only in the case where we have a guarantee that a consistent hypothesis can be found, something that is rarely possible in real applications. The same problem arises if we decide not to use a hypothesis unless its error is below a prespecified number.
|
|
| 9. |
- Andersson, Christian
(författare)
-
Register allocation by optimal graph coloring
- 2003
-
Ingår i: Lecture Notes in Computer Science (Compiler Construction). - 1611-3349 .- 0302-9743. ; 2622, s. 33-45
-
Konferensbidrag (refereegranskat)abstract
- We here present new insights of properties of real-life interference graphs emerging in register allocation. These new insights imply good hopes for a possibility of improving the coloring approach towards optimal solutions. The conclusions axe based on measurements of nearly 28,000 real instances of such interference graphs. All the instances explored are determined to possess the so-called 1-perfectness property, a fact that seems to make them easy to color optimally. The exact algorithms presented not only produce better solutions than the traditional heuristic methods, but also, indeed, seem to perform surprisingly fast, according to the measurements on our implementations.
|
|
| 10. |
- Andersson, Jens K, et al.
(författare)
-
Performance analysis and modelling of an OSA gateway
- 2003
-
Ingår i: Personal Wireless Communications / Lecture Notes in Computer Science. - 0302-9743 .- 1611-3349. - 9783540201236 ; 2775, s. 511-517
-
Konferensbidrag (refereegranskat)abstract
- It is foreseen that you in the future should be able to use the same services independent of where you are positioned or which terminal that is used. The open service architectures provide these opportunities. Open Service Access (OSA) is an example of such an architecture and it is part of the specification delivered by 3GPP. This paper explains the OSA architecture and presents a model of an OSA gateway. Further, it discusses and proposes some feasible overload control mechanisms for the gateway. The behaviour of the mechanisms is investigated through simulation.
|
|
