| 1. |
- Alvén, Jennifer, 1989, et al.
(författare)
-
A Deep Learning Approach to MR-less Spatial Normalization for Tau PET Images
- 2019
-
Ingår i: Medical Image Computing and Computer Assisted Intervention : MICCAI 2019 - 22nd International Conference, Proceedings - MICCAI 2019 - 22nd International Conference, Proceedings. - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783030322441 - 9783030322458 ; 11765 LNCS, s. 355-363
-
Konferensbidrag (refereegranskat)abstract
- The procedure of aligning a positron emission tomography (PET) image with a common coordinate system, spatial normalization, typically demands a corresponding structural magnetic resonance (MR) image. However, MR imaging is not always available or feasible for the subject, which calls for enabling spatial normalization without MR, MR-less spatial normalization. In this work, we propose a template-free approach to MR-less spatial normalization for [18F]flortaucipir tau PET images. We use a deep neural network that estimates an aligning transformation from the PET input image, and outputs the spatially normalized image as well as the parameterized transformation. In order to do so, the proposed network iteratively estimates a set of rigid and affine transformations by means of convolutional neural network regressors as well as spatial transformer layers. The network is trained and validated on 199 tau PET volumes with corresponding ground truth transformations, and tested on two different datasets. The proposed method shows competitive performance in terms of registration accuracy as well as speed, and compares favourably to previously published results.
|
|
| 2. |
- Cheraghchi, M., et al.
(författare)
-
Approximating Linear Threshold Predicates
- 2010
-
Ingår i: Lecture Notes in Computer Science. 13th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems, APPROX 2010 and 14th International Workshop on Randomization and Computation, RANDOM 2010, Barcelona, 1-3 September 2010. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743 .- 1611-3349. - 9783642153686 ; 6302, s. 110-123
-
Konferensbidrag (refereegranskat)abstract
- We study constraint satisfaction problems on the domain {-1,1}, where the given constraints are homogeneous linear threshold predicates. That is, predicates of the form sgn(w1 x1+⋯+wn x n ) for some positive integer weights w 1, ..., w n . Despite their simplicity, current techniques fall short of providing a classification of these predicates in terms of approximability. In fact, it is not easy to guess whether there exists a homogeneous linear threshold predicate that is approximation resistant or not. The focus of this paper is to identify and study the approximation curve of a class of threshold predicates that allow for non-trivial approximation. Arguably the simplest such predicate is the majority predicate sgn(x 1+⋯+xn ), for which we obtain an almost complete understanding of the asymptotic approximation curve, assuming the Unique Games Conjecture. Our techniques extend to a more general class of "majority-like" predicates and we obtain parallel results for them. In order to classify these predicates, we introduce the notion of Chow-robustness that might be of independent interest.
|
|
| 3. |
- Hedin, Daniel, 1978, et al.
(författare)
-
A Principled Approach to Tracking Information Flow in the Presence of Libraries
- 2017
-
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. - 9783662544549 ; 10204, s. 49-70
-
Konferensbidrag (refereegranskat)abstract
- There has been encouraging progress on information flow control for programs in increasingly complex programming languages, tracking the propagation of information from input sources to output sinks. Yet, programs are typically deployed in an environment with rich APIs and powerful libraries, posing challenges for information flow control when the code for these APIs and libraries is either unavailable or written in a different language.This paper presents a principled approach to tracking information flow in the presence of libraries. With the goal to strike the balance between security and precision, we present a framework that explores the middle ground between the “shallow”, signature-based modeling of libraries and the “deep”, stateful approach, where library models need to be supplied manually. We formalize our approach for a core language, extend it with lists and higher-order functions, and establish soundness results with respect to the security condition of noninterference.
|
|
| 4. |
- Isaksson, Martin, et al.
(författare)
-
Adaptive Expert Models for Federated Learning
- 2023
-
Ingår i: <em>Lecture Notes in Computer Science </em>Volume 13448 Pages 1 - 16 2023. - Cham : Springer Science and Business Media Deutschland GmbH. - 9783031289958 ; 13448 LNAI, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- Federated Learning (FL) is a promising framework for distributed learning when data is private and sensitive. However, the state-of-the-art solutions in this framework are not optimal when data is heterogeneous and non-IID. We propose a practical and robust approach to personalization in FL that adjusts to heterogeneous and non-IID data by balancing exploration and exploitation of several global models. To achieve our aim of personalization, we use a Mixture of Experts (MoE) that learns to group clients that are similar to each other, while using the global models more efficiently. We show that our approach achieves an accuracy up to 29.78% better than the state-of-the-art and up to 4.38% better compared to a local model in a pathological non-IID setting, even though we tune our approach in the IID setting. © 2023, The Author(s)
|
|
| 5. |
- 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
|
|
| 6. |
- Aanæs, Henrik, et al.
(författare)
-
Camera Resectioning from a Box
- 2009
-
Ingår i: Lecture Notes in Computer Science. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- In this paper we describe how we can do camera resectioning from a box with unknown dimensions, i.e. determine the camera model, assuming that image pixels are square. This assumption is equivalent to assuming that the camera as an aspect ratio of one and zero skew, and holds for most - if not all - digital cameras. Our proposed method works by first deriving 9 linear constraints on the projective camera matrix from the box, leaving a 3 dimensional subspace in which the projective camera matrix can lye. A single solution in this 3D subspace is then found via a method by Triggs in 1999, which uses the squared pixel assumption to set up a 4th degree polynomial to which the solution is the desired model. This approach is, however, numerically challenging, and we use several means to combat this issue. Lastly the solution is refined in an iterative manner, i.e. using bundle adjustment.
|
|
| 7. |
- Abbasi, Rosa, et al.
(författare)
-
Deductive Verification of Floating-Point Java Programs in KeY
- 2021
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 12652 LNCS, s. 242-261
-
Konferensbidrag (refereegranskat)abstract
- Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Num-ber’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for further reasoning about numerical computations—as well as certain functional properties for realistic benchmarks.
|
|
| 8. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
A PO Characterisation ofReconfiguration
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, events in which the entity does not participate. We show that partial order computations need to capture additional restrictions about event ordering, i.e., restrictions that arise from such reconfigurations. This introduces ambiguity where different partial orders represent exactly the same events with the same participants happening in different orders, thus defeating the purpose of using partial order semantics. To remove this ambiguity, we suggest an extension of partial orders called glued partial orders. We show that glued partial orders capture all possible forced reordering arising from said reconfigurations. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism. We consider channeled transition systems and Petri-nets with inhibiting arcs as examples.
|
|
| 9. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Model Checking Reconfigurable Interacting Systems
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13703). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031197581
-
Konferensbidrag (refereegranskat)abstract
- Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK (Find the associated toolkit repository here: https://github.com/dsynma/recipe.), to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, and self-organisation.
|
|
| 10. |
- Abd Alrahman, Yehia, 1986, et al.
(författare)
-
Testing for coordination fidelity : Testing for coordination fidelity
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. ; , s. 152-169
-
Bokkapitel (refereegranskat)abstract
- © Springer Nature Switzerland AG 2019. Operation control in modern distributed systems must rely on decentralised coordination among system participants. In particular when the operation control involves critical infrastructures such as power grids, it is vital to ensure correctness properties of such coordination mechanisms. In this paper, we present a verification technique that addresses coordination protocols for power grid operation control. Given a global protocol specification, we show how we can rely on testing semantics for the purpose of ensuring protocol fidelity, i.e., to certify that the interaction among the grid nodes follows the protocol specification.
|
|
