SwePub - search: L773:1611 3349 OR L773:0302 97...

Enumeration	Reference	Cover	Find
1.	Kamnitsas, Konstantinos, et al. (author) Transductive Image Segmentation : Self-training and Effect of Uncertainty Estimation 2021 In: Domain Adaptation and Representation Transfer, and Affordable Healthcare and AI for Resource Diverse Global Health - 3rd MICCAI Workshop, DART 2021, and 1st MICCAI Workshop, FAIR 2021, Held in Conjunction with MICCAI 2021, Proceedings. - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783030877217 ; 12968 LNCS, s. 79-89 Conference paper (peer-reviewed)abstract Semi-supervised learning (SSL) uses unlabeled data during training to learn better models. Previous studies on SSL for medical image segmentation focused mostly on improving model generalization to unseen data. In some applications, however, our primary interest is not generalization but to obtain optimal predictions on a specific unlabeled database that is fully available during model development. Examples include population studies for extracting imaging phenotypes. This work investigates an often overlooked aspect of SSL, transduction. It focuses on the quality of predictions made on the unlabeled data of interest when they are included for optimization during training, rather than improving generalization. We focus on the self-training framework and explore its potential for transduction. We analyze it through the lens of Information Gain and reveal that learning benefits from the use of calibrated or under-confident models. Our extensive experiments on a large MRI database for multi-class segmentation of traumatic brain lesions shows promising results when comparing transductive with inductive predictions. We believe this study will inspire further research on transductive learning, a well-suited paradigm for medical image analysis.
2.	Cheraghchi, M., et al. (author) Approximating Linear Threshold Predicates 2010 In: 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 Conference paper (peer-reviewed)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. (author) A Principled Approach to Tracking Information Flow in the Presence of Libraries 2017 In: 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 Conference paper (peer-reviewed)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. (author) Adaptive Expert Models for Federated Learning 2023 In: <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 Conference paper (peer-reviewed)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. (author) The NorduGrid Architecture And Middleware for Scientific Applications 2003 In: Lecture Notes in Computer Science. - Berlin, Heidelberg : Springer Berlin Heidelberg. ; 2657, s. 264-273 Conference paper (other academic/artistic)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. (author) Camera Resectioning from a Box 2009 In: Lecture Notes in Computer Science. - 0302-9743 .- 1611-3349. Conference paper (peer-reviewed)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. (author) Deductive Verification of Floating-Point Java Programs in KeY 2021 In: 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 Conference paper (peer-reviewed)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. (author) A PO Characterisation ofReconfiguration 2022 In: 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. Conference paper (peer-reviewed)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. (author) Model Checking Reconfigurable Interacting Systems 2022 In: Lecture Notes in Computer Science book series (LNCS,volume 13703). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031197581 Conference paper (peer-reviewed)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. (author) Testing for coordination fidelity : Testing for coordination fidelity 2019 In: 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 Book chapter (peer-reviewed)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.
11.	Abdelraheem, Mohamed Ahmed, et al. (author) On The Distribution of Linear Biases: Three Instructive Examples 2012 In: Lecture Notes in Computer Science : Advances in Cryptology – CRYPTO 2012 32nd Annual Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2012. Proceedings - Advances in Cryptology – CRYPTO 2012 32nd Annual Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2012. Proceedings. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743 .- 1611-3349. - 9783642320088 - 9783642320095 ; 7417, s. 50-67 Conference paper (peer-reviewed)abstract Despite the fact that we evidently have very good block ciphers at hand today, some fundamental questions on their security are still unsolved. One such fundamental problem is to precisely assess the security of a given block cipher with respect to linear cryptanalysis. In by far most of the cases we have to make (clearly wrong) assumptions, e.g., assume independent round-keys. Besides being unsatisfactory from a scientific perspective, the lack of fundamental understanding might have an impact on the performance of the ciphers we use. As we do not understand the security sufficiently enough, we often tend to embed a security margin -- from an efficiency perspective nothing else than wasted performance. The aim of this paper is to stimulate research on these foundations of block ciphers. We do this by presenting three examples of ciphers that behave differently to what is normally assumed. Thus, on the one hand these examples serve as counter examples to common beliefs and on the other hand serve as a guideline for future work.
12.	Abdelraheem, Mohamed, et al. (author) Practical Attacks on Relational Databases Protected via Searchable Encryption 2018 In: Lecture Notes in Computer Science. - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319991351 ; , s. 171-191 Conference paper (peer-reviewed)abstract Searchable symmetric encryption (SSE) schemes are commonly proposed to enable search in a protected unstructured documents such as email archives or any set of sensitive text files. However, some SSE schemes have been recently proposed in order to protect relational databases. Most of the previous attacks on SSE schemes have only targeted its common use case, protecting unstructured data. In this work, we propose a new inference attack on relational databases protected via SSE schemes. Our inference attack enables a passive adversary with only basic knowledge about the meta-data information of the target relational database to recover the attribute names of some observed queries. This violates query privacy since the attribute name of a query is secret.
13.	Abed, F., et al. (author) Optimal coordination mechanisms for multi-job scheduling games 2014 In: 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. - 9783662447765 ; 8737, s. 13-24 Conference paper (peer-reviewed)abstract We consider the unrelated machine scheduling game in which players control subsets of jobs. Each player's objective is to minimize the weighted sum of completion time of her jobs, while the social cost is the sum of players' costs. The goal is to design simple processing policies in the machines with small coordination ratio, i.e., the implied equilibria are within a small factor of the optimal schedule. We work with a weaker equilibrium concept that includes that of Nash. We first prove that if machines order jobs according to their processing time to weight ratio, a.k.a. Smith-rule, then the coordination ratio is at most 4, moreover this is best possible among nonpreemptive policies. Then we establish our main result. We design a preemptive policy, externality, that extends Smith-rule by adding extra delays on the jobs accounting for the negative externality they impose on other players. For this policy we prove that the coordination ratio is 1+φ≈2.618, and complement this result by proving that this ratio is best possible even if we allow for randomization or full information. Finally, we establish that this externality policy induces a potential game and that an ε-equilibrium can be found in polynomial time. An interesting consequence of our results is that an ε-local optima of R\| \|∑w j C j for the jump (a.k.a. move) neighborhood can be found in polynomial time and are within a factor of 2.618 of the optimal solution. The latter constitutes the first direct application of purely game-theoretic ideas to the analysis of a well studied local search heuristic.
14.	Abel, Andreas, 1974, et al. (author) A formalized proof of strong normalization for guarded recursive types 2014 In: Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319127354 ; 8858, s. 140-158 Conference paper (peer-reviewed)abstract We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep reduction is parametrized by a natural number “depth” that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.
15.	Abel, Andreas, 1974 (author) Compositional coinduction with sized types 2016 In: 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. Conference paper (peer-reviewed)
16.	Abel, Andreas, 1974, et al. (author) Fixed Points of Type Constructors and Primitive Recursion 2004 In: 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 Journal article (peer-reviewed)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.
17.	Abel, Andreas, 1974, et al. (author) Verifying a semantic βη-conversion test for martin-löf type theory 2008 In: 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. - 9783540705932 ; 5133 LNCS, s. 29-56 Conference paper (peer-reviewed)abstract Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of Coquand's algorithm for checking the βη-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of contextual reification and strong semantic equality. The algorithm is part of a bi-directional type checking algorithm which checks whether a normal term has a certain semantic type, a technique used in the proof assistants Agda and Epigram. We work with an abstract notion of semantic domain in order to accommodate a variety of possible implementation techniques, such as normal forms, weak head normal forms, closures, and compiled code. Our aim is to get closer than previous work to verifying the type-checking algorithms which are actually used in practice.
18.	Abidin, Aysajan, 1983, et al. (author) Attacks on Privacy-Preserving Biometric Authentication 2014 In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 8788:2014, s. 293-294 Conference paper (peer-reviewed)
19.	Abidin, Aysajan, 1983, et al. (author) Efficient Verifiable Computation of XOR for Biometric Authentication 2016 In: 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. ; 10052, s. 284-298 Conference paper (peer-reviewed)abstract This work addresses the security and privacy issues in remote biometric authentication by proposing an efficient mechanism to verify the correctness of the outsourced computation in such protocols. In particular, we propose an efficient verifiable computation of XORing encrypted messages using an XOR linear message authentication code (MAC) and we employ the proposed scheme to build a biometric authentication protocol. The proposed authentication protocol is both secure and privacy-preserving against malicious (as opposed to honest-but-curious) adversaries. Specifically, the use of the verifiable computation scheme together with an homomorphic encryption protects the privacy of biometric templates against malicious adversaries. Furthermore, in order to achieve unlinkability of authentication attempts, while keeping a low communication overhead, we show how to apply Oblivious RAM and biohashing to our protocol. We also provide a proof of security for the proposed solution. Our simulation results show that the proposed authentication protocol is efficient.
20.	Abidin, Aysajan, 1983, et al. (author) Security of a Privacy-Preserving Biometric Authentication Protocol Revisited 2014 In: 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. - 9783319122809 ; 8813, s. 290-304 Conference paper (peer-reviewed)abstract Biometric authentication establishes the identity of an individual based on biometric templates (e.g. fingerprints, retina scans etc.). Although biometric authentication has important advantages and many applications, it also raises serious security and privacy concerns. Here, we investigate a biometric authentication protocol that has been proposed by Bringer et al. and adopts a distributed architecture (i.e. multiple entities are involved in the authentication process). This protocol was proven to be secure and privacy-preserving in the honest-but-curious (or passive) attack model. We present an attack algorithm that can be employed to mount a number of attacks on the protocol under investigation. We then propose an improved version of the Bringer et al. protocol that is secure in the malicious (or active) insider attack model and has forward security.
21.	Abrahamsson, Oskar, 1986, et al. (author) Automatically introducing tail recursion in CakeML 2018 In: 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. ; 10788, s. 118-134 Conference paper (peer-reviewed)abstract We describe and implement an optimizing compiler transformation which turns non–tail-recursive functions into equivalent tail-recursive functions in an intermediate language of the CakeML compiler. CakeML is a strongly typed functional language based on Standard ML with call-by-value semantics and a fully verified compiler. We integrate our implementation into CakeML compiler, and provide a machine-checked proof verifying that the observational semantics of programs is preserved under the transformation. To the best of our knowledge, this is the first fully verified implementation of this transformation in any modern compiler. Moreover, our verification efforts uncover surprising drawbacks in some of the verification techniques employed in several parts of the CakeML compiler. We provide a work-around for these drawbacks, and compare it to potential alternatives.
22.	Aceto, L., et al. (author) Decompositional Reasoning about the History of Parallel Processes 2011 In: Fundamentals of software engineering. - Heidelberg : Springer Berlin/Heidelberg. - 1611-3349 .- 0302-9743. - 9783642293191 - 9783642293207 ; , s. 32-47 Conference paper (peer-reviewed)abstract This paper presents a decomposition technique for Hennessy-Milner logic with past and its extension with recursively defined formulae. In order to highlight the main ideas and technical tools, processes are described using a subset of CCS with parallel composition, nondeterministic choice, action prefixing and the inaction constant. The study focuses on developing decompositional reasoning techniques for parallel contexts in that language. © 2012 Springer-Verlag.
23.	Adamaszek, Anna, et al. (author) PTAS for k-tour cover poblem on the plane for moderately large values of k 2009 In: Algorithms and computation / Lecture notes in computer science. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642106309 ; 5878, s. 994-1003 Conference paper (peer-reviewed)
24.	Adams, Robin, 1978 (author) A Modular Hierarchy of Logical Frameworks 2004 In: 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 Conference paper (peer-reviewed)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.
25.	Adams, Robin, 1978, et al. (author) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components 2018 In: 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. ; 11294, s. 196-214 Conference paper (peer-reviewed)abstract Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.
26.	Adams, Robin, 1978 (author) Formalized metatheory with terms represented by an indexed family of types 2006 In: 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. ; 3839, s. 1-16 Conference paper (peer-reviewed)abstract It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step’ form; but, once the correct form has been found, the proofs are very elegant and direct.
27.	Adams, Robin, 1978, et al. (author) Weyl's predicative classical mathematics as a logic-enriched type theory 2007 In: 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. ; 4502, s. 1-17 Conference paper (peer-reviewed)abstract In Das Kontinuum, Weyl showed how a large body of classical mathematics could be developed on a purely predicative foundation. We present a logic-enriched type theory that corresponds to Weyl’s foundational system. A large part of the mathematics in Weyl’s book — including Weyl’s definition of the cardinality of a set and several results from real analysis — has been formalised, using the proof assistant Plastic that implements a logical framework. This case study shows how type theory can be used to represent a non-constructive foundation for mathematics.
28.	Adenskog, Magnus, 1985-, et al. (author) Balancing Potential and Risk : The Living Lab Approach in Mobile Participation Research 2017 In: Lecture Notes in Computer Science. - Cham : Springer Berlin/Heidelberg. - 0302-9743 .- 1611-3349. ; :10429, s. 12-23 Journal article (peer-reviewed)abstract Living labs as a research approach have been said to hold many promises regarding the evaluation of state-of-the art technologies in real-world contexts, for instance by allowing close cooperation with various stakeholders. At the same time, a living lab approach is connected with substantial complexity and increased risk. This paper elaborates on a conducted living lab with the objective to explore challenges and opportunities of mobile participation. For this purpose, a novel mobile application enabling interaction between citizens and city authorities was tested over a period of five months in Turku, Finland. In this paper, we describe identified risks associated with a living lab approach to mobile participation research. We conclude with an overall evaluation regarding the appropriateness of the living lab approach within the e-participation research field and provide recommendations on how to balance potential and risk in future projects.
29.	Afanassiev, Valentine, et al. (author) Fast message authentication using efficient polynomial evaluation 1997 In: Fast Software Encryption : 4th International Workshop, FSE 1997, Proceedings - 4th International Workshop, FSE 1997, Proceedings. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 3540632476 - 9783540632474 ; 1267, s. 190-204 Conference paper (peer-reviewed)abstract Message authentication codes (MACs) using polynomial evaluation have the advantage of requiring a very short key even for very large messages. We describe a low complexity software polynomial evaluation procedure, that for large message sizes gives a MAC that has about the same low software complexity as for bucket hashing but requires only small keys and has better security characteristics.
30.	Afshari, Bahareh, 1981, et al. (author) Abstract Cyclic Proofs (Extended abstract) 2022 In: Lecture Notes in Computer Science, 28th International Workshop on Logic, Language, Information and Computation, Iași, Romania, September 20–23, 2022, Proceedings. - Cham : Springer. - 0302-9743 .- 1611-3349. - 9783031152979 Conference paper (peer-reviewed)abstract Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by a condition on the paths through the derivation graph, known as the global trace condition. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: First, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing the Ramsey trace condition.
31.	Afshari, Bahareh, 1981, et al. (author) Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic 2023 In: Automated Reasoning with Analytic Tableaux and Related Methods, 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings / Editors: Revantha Ramanayake, Josef Urban. - Cham : Springer. - 0302-9743 .- 1611-3349. - 9783031435126 Conference paper (peer-reviewed)
32.	Afshari, Bahareh, 1981, et al. (author) Lyndon Interpolation forModal μ-Calculus 2022 In: Language, Logic, and Computation, 13th International Tbilisi Symposium, TbiLLC 2019, Batumi, Georgia, September 16–20, 2019, Revised Selected Papers / editors: Aybüke Özgün, Yulia Zinova. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783030984793 Conference paper (peer-reviewed)
33.	Afshari, Bahareh, 1981, et al. (author) Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus 2021 In: Automated Reasoning with Analytic Tableaux and Related Methods, 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings / Anupam Das, Sara Negri (eds.). - Cham : Springer. - 0302-9743 .- 1611-3349. - 9783030860585 Conference paper (peer-reviewed)abstract We show how to construct uniform interpolants in the context of the modal mu-calculus. D’Agostino and Hollenberg (2000) were the first to prove that this logic has the uniform interpolation property, employing a combination of semantic and syntactic methods. This article outlines a purely proof-theoretic approach to the problem based on insights from the cyclic proof theory of mu-calculus. We argue the approach has the potential to lend itself to other temporal and fixed point logics.
34.	Afsharmazayejani, R., et al. (author) HoneyWiN : Novel honeycomb-based wireless NoC architecture in many-core era 2018 In: Lecture Notes in Computer Science. - Cham : Springer Verlag. - 0302-9743 .- 1611-3349. ; 10824 LNCS, s. 304-316 Journal article (peer-reviewed)abstract Although NoC-based systems with many cores are commercially available, their multi-hop nature has become a bottleneck on scaling performance and energy consumption parameters. Alternatively, hybrid wireless NoC provides a postern by exploiting single-hop express links for long-distance communications. Also, there is a common wisdom that grid-like mesh is the most stable topology in conventional designs. That is why almost all of the emerging architectures had been relying on this topology as well. In this paper, first we challenge the efficiency of the grid-like mesh in emerging systems. Then, we propose HoneyWiN, a hybrid reconfigurable wireless NoC architecture that relies on the honeycomb topology. The simulation results show that on average HoneyWiN saves 17% of energy consumption while increases the network throughput by 10% compared to its wireless mesh counterpart.
35.	Agnarsson, G., et al. (author) Powers of geometric intersection graphs and dispersion algorithms 2002 In: 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 Conference paper (peer-reviewed)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.
36.	Ahmadpanah, Seyed Mohammad Mehdi, 1996, et al. (author) Securing Node-RED Applications 2021 In: Protocols, Strands, and LogicEssays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday. - Cham : Springer Science and Business Media Deutschland GmbH. ; , s. 1-21, s. 1-21, s. 1-21 Conference paper (peer-reviewed)abstract Trigger-Action Platforms (TAPs) play a vital role in fulfilling the promise of the Internet of Things (IoT) by seamlessly connecting otherwise unconnected devices and services. While enabling novel and exciting applications across a variety of services, security and privacy issues must be taken into consideration because TAPs essentially act as persons-in-the-middle between trigger and action services. The issue is further aggravated since the triggers and actions on TAPs are mostly provided by third parties extending the trust beyond the platform providers. Node-RED, an open-source JavaScript-driven TAP, provides the opportunity for users to effortlessly employ and link nodes via a graphical user interface. Being built upon Node.js, third-party developers can extend the platform’s functionality through publishing nodes and their wirings, known as flows. This paper proposes an essential model for Node-RED, suitable to reason about nodes and flows, be they benign, vulnerable, or malicious. We expand on attacks discovered in recent work, ranging from exfiltrating data from unsuspecting users to taking over the entire platform by misusing sensitive APIs within nodes. We present a formalization of a runtime monitoring framework for a core language that soundly and transparently enforces fine-grained allowlist policies at module-, API-, value-, and context-level. We introduce the monitoring framework for Node-RED that isolates nodes while permitting them to communicate via well-defined API calls complying with the policy specified for each node.
37.	Ahn, Ki Yung, et al. (author) Executable relational specifications of polymorphic type systems using prolog 2016 In: 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. - 9783319296036 ; 9613, s. 109-125 Conference paper (peer-reviewed)abstract A concise, declarative, and machine executable specification of the Hindley–Milner type system (HM) can be formulated using logic programming languages such as Prolog. Modern functional language implementations such as the Glasgow Haskell Compiler support more extensive flavors of polymorphism beyond Milner’s theory of type polymorphism in the late 70's. We progressively extend the HM specification to include more advanced type system features. An interesting development is that extending dimensions of polymorphism beyond HM resulted in a multi-staged solution: resolve the typing relations first, while delaying to resolve kinding relations, and then resolve the delayed kinding relations. Our work demonstrates that logic programing is effective for prototyping polymorphic type systems with rich features of polymorphism, and that logic programming could have been even more effective for specifying type inference if it were equipped with better theories and tools for staged resolution of different relations at different levels.
38.	Ahrendt, Wolfgang, 1967, et al. (author) A broader view on verification: From static to runtime and back (track summary) 2018 In: 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. ; 11245 LNCS, s. 3-7 Conference paper (peer-reviewed)abstract © Springer Nature Switzerland AG 2018. When seeking to verify a computational system one can either view the system as a static description of possible behaviours or a dynamic collection of observed or actual behaviours. Historically, there have been clear differences between the two approaches in terms of their level of completeness, the associated costs, the kinds of specifications considered, how and when they are applied, and so on. Recently there has been a concentrated interest in the combination of static and runtime (dynamic) techniques and this track (taking place as part of ISoLA 2018) aims to explore this combination further.
39.	Ahrendt, Wolfgang, 1967, et al. (author) A Unified Approach for Static and Runtime Verification: Framework and Applications 2012 In: 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. - 9783642340253 ; :PART 1, s. 312-326 Conference paper (peer-reviewed)abstract Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper, we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
40.	Ahrendt, Wolfgang, 1967, et al. (author) A Verification System for Distributed Objects with Asynchronous Method Calls 2009 In: 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. - 9783642103728 ; 5885, s. 387-406 Conference paper (peer-reviewed)abstract We present a verification system for Creol, an object-orientedmodeling language for concurrent distributed applications.The system is an instance of KeY, a framework for object oriented software verification, which has so far been applied foremost to sequential Java. Building on KeY characteristic concepts, like dynamic logic, sequent calculus, explicit substitutions, and the taclet rule language, the system presented in this paper addresses functional correctness of Creol models featuring local cooperative thread parallelism and global communication via asynchronous method calls. The calculus heavily operates on communication histories which describe the interfaces of Creol units. Two example scenarios demonstrate the usage of the system.
41.	Ahrendt, Wolfgang, 1967, et al. (author) Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created 2009 In: 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. - 9783642050886 ; 5850, s. 612 - 627 Conference paper (peer-reviewed)abstract In this paper we give a representation of a weakest precondition calculus for abstract object creation in dynamic logic, the logic underlying the KeY theorem prover. This representation allows to both specify and verify properties of objects at the abstraction level of the (object-oriented) programming language. Objects which are not (yet) created never play any role, neither in the specification nor in the verification of properties. Further, we show how to symbolically execute abstract object creation.
42.	Ahrendt, Wolfgang, 1967, et al. (author) Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics 2005 In: 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. - 354030553X ; LNCS 3835, s. 412 - 426 Conference paper (peer-reviewed)abstract This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic calculus which is implemented in the interactive prover of the KeY system. As a basis for validation, we take an existing SOS style rewriting logic semantics for Java, formalized in the input language of the Maude system. That semantics is `lifted' to cope with schematic programs like the ones appearing in program transformation rules. The rewriting theory is further extended to generate valid initial states for involved program fragments, and to check the final states for equivalence. The result is used in frequent validation runs over the relevant fragment of the calculus in the KeY system.
43.	Ahrendt, Wolfgang, 1967 (author) Deductive Search for Errors in Free Data Type Specifications using Model Generation 2002 In: 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 Conference paper (peer-reviewed)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.
44.	Ahrendt, Wolfgang, 1967, et al. (author) Functional Verification of Smart Contracts via Strong Data Integrity 2020 In: 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. ; 12478 LNCS, s. 9-24 Conference paper (peer-reviewed)abstract We present an invariant-based specification and verification methodology that allows us to conveniently specify and verify strong data integrity properties for Solidity smart contracts. Our approach is able to reason precisely about arbitrary usage of the contracts, which may include re-entrance, a common security pitfall in smart contracts. We implemented the approach in a prototype verification tool, called SolidiKeY, and applied it successfully to a number of smart contracts.
45.	Ahrendt, Wolfgang, 1967, et al. (author) Preface 2020 In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 12165 LNCS, s. v-vi Journal article (other academic/artistic)
46.	Ahrendt, Wolfgang, 1967, et al. (author) Preface 2019 In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 11918 LNCS, s. v-vi Journal article (other academic/artistic)
47.	Ahrendt, Wolfgang, 1967, et al. (author) Proof-based Test Case Generation 2016 In: 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. - 9783319498119 ; 10001 LNCS, s. 415-451 Book chapter (other academic/artistic)abstract KeYTestGen is a white-box test generator for Java methods based on KeY's program analysis and symbolic execution. KeYTestGen generates a JUnit test harness (test driver) which does not only initialize method parameters but also the global state that is defined by the (potentially private) fields of objects and classes. For example, a complex linked data structure may be created as test input. The tests can satisfy different test criteria such as branch coverage, path coverage, and MC/DC coverage. The user may also provide a specification in the Java Modeling Language (JML) from which a test oracle can be generated or which can be used as an abstraction for a loop or method call. KeYTestGen can be used either as a simple stand-alone tool not requiring expert knowledge or it can be used in an advanced way to support and complement formal verification.
48.	Ahrendt, Wolfgang, 1967, et al. (author) Reasoning About Loops Using Vampire in KeY 2015 In: 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. - 9783662488980 ; 9450, s. 434-443 Conference paper (peer-reviewed)abstract We describe symbol elimination and consequence finding in the first-order theorem prover Vampire for automatic generation of quantified invariants, possibly with quantifier alternations, of loops with arrays. Unlike the previous implementation of symbol elimination in Vampire, our work is not limited to a specific programming language but provides a generic framework by relying on a simple guarded command representation of the input loop. We also improve the loop analysis part in Vampire by generating loop properties more easily handled by the saturation engine of Vampire. Our experiments show that, with our changes, the number of generated invariants is decreased, in some cases, by a factor of 20. We also provide a framework to use our approach to invariant generation in conjunction with pre- and post-conditions of program loops. We use the program specification to find relevant invariants as well as to verify the partial correctness of the loop. As a case study, we demonstrate how symbol elimination in Vampire can be used as an interface for realistic imperative languages, by integrating our tool inthe KeY verification system, thus allowing reasoning about loops in Java programs in a fully automated way, without any user guidance.
49.	Ahrendt, Wolfgang, 1967, et al. (author) Selective Presumed Benevolence in Multi-party System Verification 2022 In: 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. ; 13701 LNCS, s. 106-123 Conference paper (peer-reviewed)abstract The functional correctness of particular components in a multi-party system may be dependent on the behaviour of other components and parties. Assumptions about how the other parties will act would thus have to be reflected in the specifications. In fact, one can find a substantial body of work on assume-guarantee reasoning with respect to the functional aspects of the component under scrutiny and those of other components. In this paper, we turn to look at non-functional assumptions about the behaviour of other parties. In particular, we look at smart contract verification under assumptions about presumed benevolence of particular parties and focusing on reentrancy issues—a class of bugs which, in the past few years, has led to huge financial losses. We make a case for allowing, in the specification, fine-grained assumptions on benevolence of certain parties, and show how these assumptions can be exploited in the verification process.
50.	Ahrendt, Wolfgang, 1967, et al. (author) Specification language for static and runtime verification of data and control properties 2015 In: Lecture Notes in Computer Science. FM 2015: FORMAL METHODS. 20th International Symposium on Formal Methods (FM), Oslo, Norway, June 24-26, 2015. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319192482 ; 9109, s. 108-125 Conference paper (peer-reviewed)abstract Static verification techniques can verify properties across all executions of a program, but powerful judgements are hard to achieve automatically. In contrast, runtime verification enjoys full automation, but cannot judge future and alternative runs. In this paper we present a novel approach in which data-centric and control-oriented properties may be stated in a single formalism, amenable to both static and dynamic verification techniques. We develop and formalise a specification notation, ppDATE, extending the control-flow property language used in the runtime verification tool Larva with pre/post-conditions and show how specifications written in this notation can be analysed both using the deductive theorem prover KeY and the runtime verification tool Larva. Verification is performed in two steps: KeY first partially proves the dataoriented part of the specification, simplifying the specification which is then passed on to Larva to check at runtime for the remaining parts of the specification including the control-centric aspects. We apply the approach to Mondex, an electronic purse application.

Skapa referenser, mejla, bekava och länka

Permalink

Träfflista för sökning "L773:1611 3349 OR L773:0302 9743 OR L773:9783030877217 "

Refine your search

Year