SwePub
Sök i SwePub databas

  Extended search

Träfflista för sökning "L773:1611 3349 OR L773:0302 9743 OR L773:9783030877217 srt2:(2020-2024)"

Search: L773:1611 3349 OR L773:0302 9743 OR L773:9783030877217 > (2020-2024)

  • Result 1-50 of 279
Sort/group result
   
EnumerationReferenceCoverFind
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.
  • 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)
  •  
3.
  • 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.
  •  
4.
  • 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.
  •  
5.
  • 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.
  •  
6.
  • 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.
  •  
7.
  • 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)
  •  
8.
  • 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)
  •  
9.
  • 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.
  •  
10.
  • 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. ; 13066 LNCS, 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.
  •  
11.
  • Ahrendt, Wolfgang, 1967, et al. (author)
  • AI Assisted Programming: (AISoLA 2023 Track Introduction)
  • 2024
  • In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 14380 LNCS, s. 351-354
  • Conference paper (peer-reviewed)abstract
    • The paper is an introduction to the track ‘AI Assisted Programming’, organized at the AISoLA conference during the period October 23–28, 2023. The theme of AISoLA 2023 is: ‘Bridging the Gap Between AI and Reality’. The motivation behind the track is the emerging use of Large Language Models for construction and analysis of software artifacts. An overview of the track presentations is provided.
  •  
12.
  • 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.
  •  
13.
  • 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)
  •  
14.
  • 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.
  •  
15.
  • Ahrendt, Wolfgang, 1967, et al. (author)
  • SpecifyThis – Bridging Gaps Between Program Specification Paradigms
  • 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. 3-6
  • Conference paper (peer-reviewed)abstract
    • We motivate and summarise the track SpecifyThis – Bridging gaps between program specification paradigms, taking place at the International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022.
  •  
16.
  • Ahrendt, Wolfgang, 1967, et al. (author)
  • TriCo—Triple Co-piloting of Implementation, Specification and Tests
  • 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. 174-187, s. 174-187
  • Conference paper (peer-reviewed)abstract
    • This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.
  •  
17.
  • Al Sabbagh, Khaled, 1987, et al. (author)
  • Improving Software Regression Testing Using a Machine Learning-Based Method for Test Type Selection
  • 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. ; 13709 LNCS, s. 480-496
  • Conference paper (peer-reviewed)abstract
    • Since only a limited time is available for performing software regression testing, a subset of crucial test cases from the test suites has to be selected for execution. In this paper, we introduce a method that uses the relation between types of code changes and regression tests to select test types that require execution. We work closely with a large power supply company to develop and evaluate the method and measure the total regression testing time taken by our method and its effectiveness in selecting the most relevant test types. The results show that the method reduces the total regression time by an average of 18,33% when compared with the approach used by our industrial partner. The results also show that using a medium window size in the method configuration results in an improved recall rate from 61,11% to 83,33%, but not in considerable time reduction of testing. We conclude that our method can potentially be used to steer the testing effort at software development companies by guiding testers into which regression test types are essential for execution.
  •  
18.
  • Al Sabbagh, Khaled, 1987, et al. (author)
  • The Effect of Class Noise on Continuous Test Case Selection: A Controlled Experiment on Industrial Data
  • 2020
  • In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 12562, s. 287-303
  • Conference paper (peer-reviewed)abstract
    • Continuous integration and testing produce a large amount of data about defects in code revisions, which can be utilized for training a predictive learner to effectively select a subset of test suites. One challenge in using predictive learners lies in the noise that comes in the training data, which often leads to a decrease in classification performances. This study examines the impact of one type of noise, called class noise, on a learner’s ability for selecting test cases. Understanding the impact of class noise on the performance of a learner for test case selection would assist testers decide on the appropriateness of different noise handling strategies. For this purpose, we design and implement a controlled experiment using an industrial data-set to measure the impact of class noise at six different levels on the predictive performance of a learner. We measure the learning performance using the Precision, Recall, F-score, and Mathew Correlation Coefficient (MCC) metrics. The results show a statistically significant relationship between class noise and the learners performance for test case selection. Particularly, a significant difference between the three performance measures (Precision, F-score, and MCC)under all the six noise levels and at 0% level was found, whereas a similar relationship between recall and class noise was found at a level above30%. We conclude that higher class noise ratios lead to missing out more tests in the predicted subset of test suite and increases the rate of false alarms when the class noise ratio exceeds 30%
  •  
19.
  • Alaqra, Ala Sarah, et al. (author)
  • Transparency of Privacy Risks Using PIA Visualizations
  • 2023
  • In: HCI for Cybersecurity, Privacy and Trust. - Cham : Springer. - 9783031358210 - 9783031358227 ; 14045 LNCS, s. 3-17
  • Conference paper (peer-reviewed)abstract
    • Privacy enhancing technologies allow the minimization of risks to online data. However, the transparency of the minimization process is not so clear to all types of end users. Privacy Impact Assessments (PIAs) is a standardized tool that identifies and assesses privacy risks associated with the use of a system. In this work, we used the results of the PIA conducted in our use case to visualize privacy risks to end users in the form of User Interface (UI) mock ups. We tested and evaluated the UI mock-ups via walkthroughs to investigate users' interests by observing their clicking behavior, followed by four focus group workshops. There were 13 participants (two expert groups and two lay user groups) in total. Results reveal general interests in the transparency provided by showing the risks reductions. Generally, although participants appreciate the concept of having detailed information provided about risk reductions and the type of risks, the visualization and usability of the PIA UIs require future development. Specifically, it should be tailored to the target group's mental models and background knowledge.
  •  
20.
  • Alce, Günter, et al. (author)
  • Comparison of the Effect of Exposing Users for Height While Being Active Versus Passive in a Virtual Environment - A Pilot Study
  • 2022
  • In: Extended Reality - 1st International Conference, XR Salento 2022, Proceedings. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783031155451 ; 13445 LNCS, s. 18-36
  • Conference paper (peer-reviewed)abstract
    • Phobias have historically and evolutionary been vital for humans to escape quickly or fight in dangerous situations. The anxieties that phobias evoke have made people live longer. Evolutionarily, anxiety has been good, but fear and anxiety come in unjustified situations for the civilized population in the 21st century. Some people have an extra sensitive reaction system activated too often in irrelevant contexts. More than 10% of Sweden’s population has some phobia. However, only a few persons search for help to overcome their phobias, partly because they know they have to be exposed to their phobia to overcome it. An alternative exposure treatment is using virtual reality (VR). Recently, we have seen an intensified development of VR headsets such as HTC Vive and Oculus Quest. These headsets come with relatively high display resolution and great tracking of the hand controllers, which opens up opportunities to develop and evaluate more immersive interactive virtual environments that can be used, e.g., for exposure treatment. This paper presents two VR prototypes developed and evaluated using the new generation of VR technology. The two VR prototypes were then compared in a user study with 22 participants exposed to height while being active versus being passive. The main contribution of this paper is to elucidate knowledge about the experiment of comparing AE versus PE of heights.
  •  
21.
  • Alce, Günter, et al. (author)
  • Design and Evaluation of Three User Interfaces for Detecting Unmanned Aerial Vehicles Using Virtual Reality
  • 2022
  • In: Virtual Reality and Mixed Reality - 19th EuroXR International Conference, EuroXR 2022, Proceedings. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783031162336 ; 13484 LNCS, s. 36-49
  • Conference paper (peer-reviewed)abstract
    • Regulations restrict UAVs to fly only within direct view of the pilot, limiting their ability to support critical societal functions. One potential way to move beyond this limitation is by placing a 360-degree camera on the vehicle and using its feed to provide operators with a view that is the equivalent to being on the vehicle. This necessitates a cockpit user interface (UI) that amongst other things highlights flying objects, so that collision with these can be avoided. In this paper, virtual reality (VR) was used to build a prototype of such a system and evaluate three UIs that were designed to facilitate detecting aerial. Conclusions are drawn regarding which UI features support detection performance and a positive user experience.
  •  
22.
  • Alce, Günter, et al. (author)
  • Using augmented reality to train flow patterns for pilot students - An explorative study
  • 2020
  • In: Augmented Reality, Virtual Reality, and Computer Graphics - 7th International Conference, AVR 2020, Proceedings. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783030584641 - 9783030584658 ; 12242, s. 215-231
  • Conference paper (peer-reviewed)abstract
    • Today, just as in the early days of flying, much emphasis is put on the pilot student’s flight training before flying a real commercial aircraft. In the early stages of a pilot student’s education, they must, for example, learn different operating procedures known as flow patterns using very basic tools, such as exhaustive manuals and a so-called paper tiger. In this paper, we present a first design of a virtual and interactive paper tiger using augmented reality (AR), and perform an evaluation of the developed prototype. We evaluated the prototype on twenty-seven pilot students at the Lund University School of Aviation (LUSA), to explore the possibilities and technical advantages that AR can offer, in particular the procedure that is performed before takeoff. The prototype got positive results on perceived workload, and in remembering the flow pattern. The main contribution of this paper is to elucidate knowledge about the value of using AR for training pilot students.
  •  
23.
  • Alkoutli, Anas, et al. (author)
  • Assessing Security of Internal Vehicle Networks
  • 2023
  • In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 0302-9743 .- 1611-3349. - 9783031368882 ; , s. 151-164
  • Book chapter (peer-reviewed)abstract
    • Automotive software grows exponentially in size. In premium vehicles, the size can reach over 100 million lines of code. One of the challenges in such a large software is how it is architecturally designed and whether this design leads to security vulnerabilities. In this paper, we report on a design science research study aimed at understanding the vulnerabilities of modern premium vehicles. We used machine learning to identify and reconstruct signals within the vehicle’s communication networks. The results show that the distributed software architectures can have security vulnerabilities due to the high connectivity of modern vehicles; and that the security needs to be seen holistically – both when constructing the vehicle’s software and when designing communication channels with cloud services. The paper proposed a number of measures that can help to address the identified vulnerabilities.
  •  
24.
  • Almulla, Hussein, et al. (author)
  • Generating Diverse Test Suites for Gson Through Adaptive Fitness Function Selection
  • 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. - 9783030597610 - 9783030597627 ; SSBSE 2020, s. 246-252
  • Conference paper (peer-reviewed)abstract
    • Many fitness functions - such as those targeting test suite diversity—do not yield sufficient feedback to drive test generation. We propose that diversity can instead be improved through adaptive fitness function selection (AFFS), an approach that varies the fitness functions used throughout the generation process in order to strategically increase diversity. We have evaluated our AFFS framework, EvoSuiteFIT, on a set of 18 real faults from Gson, a JSON (de)serialization library. Ultimately, we find that AFFS creates test suites that are more diverse than those created using static fitness functions. We also observe that increased diversity may lead to small improvements in the likelihood of fault detection.
  •  
25.
  • Alshareef, Hanaa, 1985, et al. (author)
  • Refining Privacy-Aware Data Flow Diagrams
  • 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. ; 13085, s. 121-140
  • Conference paper (peer-reviewed)abstract
    • Privacy, like security, is a non-functional property, yet most software design tools are focused on functional aspects, using for instance Data Flow Diagrams (DFDs). In previous work, a conceptual model was introduced where DFDs were extended into so-called Privacy-Aware Data Flow Diagrams (PA-DFDs) with the aim of adding specific privacy checks to existing DFDs. An implementation to add such automatic checks has also been developed. In this paper, we define the notion of refinement for both DFDs and PA-DFDs as a special type of structure-preserving map (or graph homomorphism). We also provide three algorithms to find, check and transform refinements, and we show that the standard diagram "transform→refine/refine→transform" commutes. We have implemented our algorithms in a proof-of-concept tool called DFD Refinery , and have applied it to realistic scenarios.
  •  
26.
  • Altenkirch, Thorsten, et al. (author)
  • Constructing a universe for the setoid model
  • 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. ; 12650, s. 1-21
  • Conference paper (peer-reviewed)abstract
    • The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent propositions. The appeal of this model construction is that it can be constructed in a small, intensional, type theoretic metatheory, therefore giving a method to boostrap extensionality. The setoid model has been recently adapted into a formal system, namely Setoid Type Theory (SeTT). SeTT is an extension of intensional Martin-Löf type theory with constructs that give full access to the extensionality principles that hold in the setoid model. Although already a rich theory as currently defined, SeTT currently lacks a way to internalize the notion of type beyond propositions, hence we want to extend SeTT with a universe of setoids. To this aim, we present the construction of a (non-univalent) universe of setoids within the setoid model, first as an inductive-recursive definition, which is then translated to an inductive-inductive definition and finally to an inductive family. These translations from more powerful definition schemas to simpler ones ensure that our construction can still be defined in a relatively small metatheory which includes a proof-irrelevant identity type with a strong transport rule.
  •  
27.
  • Arafat, Naheed Anjum, et al. (author)
  • Construction and random generation of hypergraphs with prescribed degree and dimension sequences
  • 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. ; 12392 LNCS, s. 130-145
  • Conference paper (peer-reviewed)abstract
    • We propose algorithms for construction and random generation of hypergraphs without loops and with prescribed degree and dimension sequences. The objective is to provide a starting point for as well as an alternative to Markov chain Monte Carlo approaches. Our algorithms leverage the transposition of properties and algorithms devised for matrices constituted of zeros and ones with prescribed row- and column-sums to hypergraphs. The construction algorithm extends the applicability of Markov chain Monte Carlo approaches when the initial hypergraph is not provided. The random generation algorithm allows the development of a self-normalised importance sampling estimator for hypergraph properties such as the average clustering coefficient. We prove the correctness of the proposed algorithms. We also prove that the random generation algorithm generates any hypergraph following the prescribed degree and dimension sequences with a non-zero probability. We empirically and comparatively evaluate the effectiveness and efficiency of the random generation algorithm. Experiments show that the random generation algorithm provides stable and accurate estimates of average clustering coefficient, and also demonstrates a better effective sample size in comparison with the Markov chain Monte Carlo approaches.
  •  
28.
  • Aranha, Diego F., et al. (author)
  • Count Me In! Extendability for Threshold Ring Signatures
  • 2022
  • In: Public-Key Cryptography - PKC 2022 : 25th IACR International Conference on Practice and Theory of Public-Key Cryptography, Proceedings, Part II - 25th IACR International Conference on Practice and Theory of Public-Key Cryptography, Proceedings, Part II. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783030971311 - 9783030971304 ; 13178, s. 379-406
  • Conference paper (peer-reviewed)abstract
    • Ring signatures enable a signer to sign a message on behalf of a group anonymously, without revealing her identity. Similarly, threshold ring signatures allow several signers to sign the same message on behalf of a group; while the combined signature reveals that some threshold t of the group members signed the message, it does not leak anything else about the signers’ identities. Anonymity is a central feature in threshold ring signature applications, such as whistleblowing, e-voting and privacy-preserving cryptocurrencies: it is often crucial for signers to remain anonymous even from their fellow signers. When the generation of a signature requires interaction, this is difficult to achieve. There exist threshold ring signatures with non-interactive signing—where signers locally produce partial signatures which can then be aggregated—but a limitation of existing threshold ring signature constructions is that all of the signers must agree on the group on whose behalf they are signing, which implicitly assumes some coordination amongst them. The need to agree on a group before generating a signature also prevents others—from outside that group—from endorsing a message by adding their signature to the statement post-factum. We overcome this limitation by introducing extendability for ring signatures, same-message linkable ring signatures, and threshold ring signatures. Extendability allows an untrusted third party to take a signature, and extend it by enlarging the anonymity set to a larger set. In the extendable threshold ring signature, two signatures on the same message which have been extended to the same anonymity set can then be combined into one signature with a higher threshold. This enhances signers’ anonymity, and enables new signers to anonymously support a statement already made by others. For each of those primitives, we formalize the syntax and provide a meaningful security model which includes different flavors of anonymous extendability. In addition, we present concrete realizations of each primitive and formally prove their security relying on signatures of knowledge and the hardness of the discrete logarithm problem. We also describe a generic transformation to obtain extendable threshold ring signatures from same-message-linkable extendable ring signatures. Finally, we implement and benchmark our constructions.
  •  
29.
  • Aranha, Diego, et al. (author)
  • LOVE a Pairing
  • 2021
  • In: Progress in Cryptology – LATINCRYPT 2021 : 7th International Conference on Cryptology and Information Security in Latin America, Bogotá, Colombia, October 6–8, 2021, Proceedings - 7th International Conference on Cryptology and Information Security in Latin America, Bogotá, Colombia, October 6–8, 2021, Proceedings. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783030882372 - 9783030882389 ; 12912, s. 320-340
  • Conference paper (peer-reviewed)abstract
    • The problem of securely outsourcing the computation of a bilinear pairing has been widely investigated in the literature. Designing an efficient protocol with the desired functionality has, however, been an open challenge for a long time. Recently, Di Crescenzo et al. (CARDIS’20) proposed the first suite of protocols for securely and efficiently delegating pairings with online inputs under the presence of a malicious server. We progress along this path with the aim of LOVE (Lowering the cost of Outsourcing and Verifying Efficiently) a pairing. Our contributions are threefold. First, we propose a protocol (LOVE) that improves the efficiency of Di Crescenzo et al.’s proposal for securely delegating pairings with online, public inputs. Second, we provide the first implementation of efficient protocols in this setting. Finally, we evaluate the performance of our LOVE protocol in different application scenarios by benchmarking an implementation using BN, BLS12 and BLS24 pairing-friendly curves. Interestingly, compared to Di Crescenzo et al.’s protocol, LOVE is up to 29.7% faster for the client, up to 24.9% for the server and requires 23–24% less communication cost depending on the choice of parameters. Furthermore, we note that our LOVE protocol is especially suited for subgroup-secure groups: checking the correctness of the delegated pairing requires up to 56.2% less computations than evaluating the pairing locally (no delegation). This makes LOVE the most efficient protocol to date for securely outsourcing the computation of a pairing with online public inputs, even when the server is malicious.
  •  
30.
  • Atiiq, Syafiq Al, et al. (author)
  • X-Pro : Distributed XDP Proxies Against Botnets of Things
  • 2021
  • In: Secure IT Systems - 26th Nordic Conference, NordSec 2021, Proceedings. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783030916244 ; 13115 LNCS, s. 51-71
  • Conference paper (peer-reviewed)abstract
    • The steadily increasing Internet of Things (IoT) devices are vulnerable to be used as bots to launch distributed-denial-of-service (DDoS) attacks. In this paper, we present X-Pro, a distributed XDP proxy to counteract DDoS attacks. We propose a source-based defense mechanism where proxies located between the IoT devices and the victim performs flow policing on all IoT traffic from a single administrative domain. The proposed proxy architecture can be integrated in widely used IoT frameworks as well as telecommunication networks. The proxies are working synchronously to block bogus messages and to detect traffic levels above predefined thresholds. Our implementation leverages eXpress Data Path (XDP), a programmable packet processing in the Linux kernel, as the main engine in the proxy. We evaluate X-Pro from several standpoints and conclude that our solution offers efficient DoS traffic blocking for both low-rate or massive attacks. Depending on the device side implementation selection, the computational overhead is cheap at the cost of some bandwidth loss.
  •  
31.
  • Azzopardi, Shaun, 1992, et al. (author)
  • AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
  • 2022
  • In: Lecture Notes in Computer Science book series (LNCS, volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
  • Conference paper (peer-reviewed)abstract
    • Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.
  •  
32.
  • Azzopardi, Shaun, 1992, et al. (author)
  • On the Specification and Monitoring of Timed Normative Systems
  • 2021
  • 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
    • In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.
  •  
33.
  • Azzopardi, Shaun, 1992, et al. (author)
  • ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae
  • 2023
  • In: Automated Technology for Verification and Analysis (ATVA). - Germany : Springer. - 0302-9743 .- 1611-3349. - 9783031453311
  • Conference paper (peer-reviewed)abstract
    • This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such as LTL-to-automata translators and reactive synthesis tools, to support a richer input language. Namely, with ppLTLTT, tools that accept LTL input are also made to handle pure-past LTL as atomic formulae. While the addition of past operators does not increase the expressive power of LTL, it opens up the possibility of writing more intuitive and succinct specifications. We illustrate this intended use of ppLTLTT for Slugs, Strix, and Spot ’s command line tool LTL2TGBA by describing three corresponding wrapper tools pSlugs, pStrix, and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools are designed to seamlessly fit this paradigm, by staying as close to the respective syntax of each underlying tool as possible.
  •  
34.
  • Azzopardi, Shaun, 1992, et al. (author)
  • Runtime Verification Meets Controller Synthesis
  • 2022
  • In: Lecture Notes in Computer Science book series (LNCS,volume 13701). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031198489
  • Conference paper (peer-reviewed)abstract
    • Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to interact with an environment, but the more precise the model of the environment used for synthesis, the greater the cost of synthesis. This can be avoided by using suitable abstractions of the environment, but this in turn requires appropriate techniques to mediate between controllers and the real environment. Runtime verification can help here, with monitors acting as these mediators, and even as activators or orchestrators of the desired controllers. In this paper we survey literature for combinations of monitors with controller synthesis, and consider other potential combinations as future research directions.
  •  
35.
  • Azzopardi, Shaun, 1992, et al. (author)
  • Tainting in Smart Contracts: Combining Static and Runtime Verification
  • 2022
  • In: Lecture Notes in Computer Science book series (LNCS,volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
  • Conference paper (peer-reviewed)abstract
    • Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains—open for interaction with any other smart contract and offchain entity. Interaction, for instance with off-chain oracles, can affect the state of the smart contract, and correctness of these smart contracts may depend on the trustworthiness of the data they manipulate or events they generate which, in turn, would depend on which parties or what information contributed to them. In this paper, we develop and present dynamic taint analysis techniques to enable data tainting in smart contracts. We propose an extension of Solidity that enables labelling inputs of interaction endpoints with dynamic data-carrying labels that capture actionable information about the sender. These labels can then be propagated dynamically across transactions to transitively dependent data. Specifications can then refer to such taints, for instance for ensuring that certain data could not have been influenced through interaction by a certain party. We further allow the use of taints as part of the language, affecting the control flow of the smart contract. To manage the overheads of such runtime tainting we develop sound static analysis-based techniques to prune away unnecessary instrumentation. We give a case study as a proof-of-concept, and measure the overheads associated with our additions before and after optimisation.
  •  
36.
  • Balkenius, Christian, et al. (author)
  • Elements of cognition for general intelligence
  • 2023
  • In: Artificial General Intelligence : 16th International Conference, AGI 2023, Stockholm, Sweden, June 16–19, 2023, Proceedings - 16th International Conference, AGI 2023, Stockholm, Sweden, June 16–19, 2023, Proceedings. - 1611-3349 .- 2945-9133 .- 0302-9743 .- 2945-9141. - 9783031334689 - 9783031334696 ; 13921, s. 11-20
  • Conference paper (peer-reviewed)abstract
    • What can artificial intelligence learn from the cognitive sciences? We review some fundamental aspects of how human cognition works and relate it to different brain structures and their function. A central theme is that cognition is very different from how it is envisioned in classical artificial intelligence which offers a novel path toward intelligent systems that in many ways is both simpler and more attainable. We also argue that artificial intelligent systems takes more than a single silver bullet. It requires a large number of interacting subsystem that are coupled to both the body and to the environment. We argue for an approach to artificial general intelligence based on a faithful reproduction of known brain processes in a system-level model that incorporates a large number of components modelled after the human brain.
  •  
37.
  • Barath, Daniel, et al. (author)
  • Making Affine Correspondences Work in Camera Geometry Computation
  • 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. ; 12356 LNCS, s. 723-740
  • Conference paper (peer-reviewed)abstract
    • Local features e.g. SIFT and its affine and learned variants provide region-to-region rather than point-to-point correspondences. This has recently been exploited to create new minimal solvers for classical problems such as homography, essential and fundamental matrix estimation. The main advantage of such solvers is that their sample size is smaller, e.g., only two instead of four matches are required to estimate a homography. Works proposing such solvers often claim a significant improvement in run-time thanks to fewer RANSAC iterations. We show that this argument is not valid in practice if the solvers are used naively. To overcome this, we propose guidelines for effective use of region-to-region matches in the course of a full model estimation pipeline. We propose a method for refining the local feature geometries by symmetric intensity-based matching, combine uncertainty propagation inside RANSAC with preemptive model verification, show a general scheme for computing uncertainty of minimal solvers results, and adapt the sample cheirality check for homography estimation. Our experiments show that affine solvers can achieve accuracy comparable to point-based solvers at faster run-times when following our guidelines. We make code available at https://github.com/danini/affine-correspondences-for-camera-geometry.
  •  
38.
  • Bastajic, Milos, et al. (author)
  • Operationalizing Machine Learning Using Requirements-Grounded MLOps
  • 2024
  • In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 14588 LNCS, s. 231-248
  • Conference paper (peer-reviewed)abstract
    • [Context & Motivation] Machine learning (ML) use has increased significantly, [Question/Problem] however, organizations still struggle with operationalizing ML. [Principle results] In this paper, we explore the intersection between machine learning operations (MLOps) and Requirements engineering (RE) by investigating the current problems and best practices associated with developing an MLOps process. The goal is to create an artifact that would guide MLOps implementation from an RE perspective, aiming for a more systematic approach to managing ML models in production by identifying and documenting the goals and objectives. The study adopted a Design Science Research methodology, examining the difficulties currently faced in creating an MLOps process, identified potential solutions to these difficulties, and assessed the effectiveness of one particular solution, an artifact containing guiding Requirements Questions sorted by ML stages and practitioner roles. [Contribution] By establishing a more thorough understanding of how the two domains interact and by offering practical guidance for implementing MLOps processes from an RE perspective, this study advances both the MLOps and RE fields.
  •  
39.
  • Bastys, Iulia, 1986, et al. (author)
  • Automatic Annotation of Confidential Data in Java Code
  • 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. ; 13291, s. 146-161
  • Conference paper (peer-reviewed)abstract
    • The problem of confidential information leak can be addressed by using automatic tools that take a set of annotated inputs (the source ) and track their flow to public sinks . Unfortunately, manually annotating the code with labels specifying the secret sources is one of the main obstacles in the adoption of such trackers. In this work, we present an approach for the automatic generation of labels for confidential data in Java programs. Our solution is based on a graph-based representation of Java methods: starting from a minimal set of known API calls, it propagates the labels both intra- and inter-procedurally until a fix-point is reached. In our evaluation, we encode our synthesis and propagation algorithm in Datalog and assess the accuracy of our technique on seven previously annotated internal code bases, where we can reconstruct 75% of the preexisting manual annotations. In addition to this single data point, we also perform an assessment using samples from the SecuriBench-micro benchmark, and we provide additional sample programs that demonstrate the capabilities and the limitations of our approach.
  •  
40.
  • Bastys, Iulia, 1986, et al. (author)
  • SecWasm: Information Flow Control for WebAssembly
  • 2022
  • In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer Nature Switzerland. - 1611-3349 .- 0302-9743. ; 13790 LNCS, s. 74-103
  • Conference paper (peer-reviewed)abstract
    • We introduce SecWasm, the first general purpose information-flow control system for WebAssembly (Wasm), thus extending the safety guarantees offered by Wasm with guarantees that applications manipulate sensitive data in a secure way. SecWasm is a hybrid system enforcing termination-insensitive noninterference which overcomes the challenges posed by the uncommon characteristics for machine languages of Wasm in an elegant and thorough way.
  •  
41.
  • Basu, Debabrota, 1992, et al. (author)
  • BelMan: An Information-Geometric Approach to Stochastic Bandits
  • 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. ; 11908 LNAI, s. 167-183
  • Conference paper (peer-reviewed)abstract
    • We propose a Bayesian information-geometric approach to the exploration–exploitation trade-off in stochastic multi-armed bandits. The uncertainty on reward generation and belief is represented using the manifold of joint distributions of rewards and beliefs. Accumulated information is summarised by the barycentre of joint distributions, the pseudobelief-reward. While the pseudobelief-reward facilitates information accumulation through exploration, another mechanism is needed to increase exploitation by gradually focusing on higher rewards, the pseudobelief-focal-reward. Our resulting algorithm, BelMan, alternates between projection of the pseudobelief-focal-reward onto belief-reward distributions to choose the arm to play, and projection of the updated belief-reward distributions onto the pseudobelief-focal-reward. We theoretically prove BelMan to be asymptotically optimal and to incur a sublinear regret growth. We instantiate BelMan to stochastic bandits with Bernoulli and exponential rewards, and to a real-life application of scheduling queueing bandits. Comparative evaluation with the state of the art shows that BelMan is not only competitive for Bernoulli bandits but in many cases also outperforms other approaches for exponential and queueing bandits.
  •  
42.
  • Berg, Jeremias, et al. (author)
  • Certified Core-Guided MaxSAT Solving
  • 2023
  • In: Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. - 0302-9743 .- 1611-3349. - 9783031384981 ; 14132 LNAI, s. 1-22
  • Conference paper (peer-reviewed)abstract
    • In the last couple of decades, developments in SAT-based optimization have led to highly efficient maximum satisfiability (MaxSAT) solvers, but in contrast to the SAT solvers on which MaxSAT solving rests, there has been little parallel development of techniques to prove the correctness of MaxSAT results. We show how pseudo-Boolean proof logging can be used to certify state-of-the-art core-guided MaxSAT solving, including advanced techniques like structure sharing, weight-aware core extraction and hardening. Our experimental evaluation demonstrates that this approach is viable in practice. We are hopeful that this is the first step towards general proof logging techniques for MaxSAT solvers.
  •  
43.
  • Bergström, Emil, et al. (author)
  • Exploring the Design Context of AI-Powered Services : A Qualitative Investigation of Designers’ Experiences with Machine Learning
  • 2022
  • In: Lecture Notes in Computer Science. - Heidelberg : Springer. - 0302-9743 .- 1611-3349. ; 13336, s. 3-21
  • Journal article (peer-reviewed)abstract
    • Artificial Intelligence (AI) has provided user experience (UX) designers with a richer toolset. To use technologies such as Machine Learning (ML) that can expand their creative capacity to design intelligent services. ML has the capability to enhance the user experience, for example, by improving efficiency, personalization, and context-aware adaptation. However, research suggests ML as a challenging design material in UX practice, such as difficulties in comprehending data dependencies when prototyping, or the lack of tools and methods for evaluating adaptive user experiences. Previous research indicates that lack of knowledge transfer into the UX design practice may hamper innovative potential. This work aims to provide new insights on how designers think about – and experience – design for AI-powered services. It is important to make ML-powered services beneficial and sustainable for end-users, organizations, and society. Therefore, we explore UX designers’ reflections and experiences of using ML in a design context. We have performed nine deep explorative interviews with professional designers that work with ML. The respondents have different backgrounds, seniority, and work in different sectors. The collected interview material was qualitatively analyzed and resulted in five conceptual themes for how UX designers experience the design context surrounding AI-powered services: 1) Absence of competence, 2) Lack of incentive for competence development, 3) Challenges in articulating design criteria, 4) Mature vs. Immature clients, and 5) Lack of support for ethical concerns. We provide implications for how these themes affect the design context and practice. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
  •  
44.
  • Bollina, Srujana, et al. (author)
  • Bytecode-Based Multiple Condition Coverage: An Initial Investigation
  • 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. - 9783030597627 ; SSBSE 2020, s. 220-236
  • Conference paper (peer-reviewed)abstract
    • Masking occurs when one condition prevents another from influencing the output of a Boolean expression. Adequacy criteria such as Multiple Condition Coverage (MCC) overcome masking within one expression, but offer no guarantees about subsequent expressions. As a result, a Boolean expression written as a single complex statement will yield more effective test cases than when written as a series of simple expressions. Many approaches to automated test case generation for Java operate not on the source code, but on bytecode. The transformation to bytecode simplifies complex expressions into multiple expressions, introducing masking. We propose Bytecode-MCC, a new adequacy criterion designed to group bytecode expressions and reformulate them into complex expressions. Bytecode-MCC should produce test obligations that are more likely to reveal faults in program logic than tests covering the simplified bytecode. A preliminary study shows potential improvements from attaining Bytecode-MCC coverage. However, Bytecode-MCC is difficult to optimize, and means of increasing coverage are needed before the technique can make a difference in practice. We propose potential methods to improve coverage.
  •  
45.
  • Boschini, Cecilia, et al. (author)
  • Progressive and efficient verification for digital signatures
  • 2022
  • In: Applied Cryptography and Network Security : 20th International Conference, ACNS 2022, Rome, Italy, June 20–23, 2022, Proceedings - 20th International Conference, ACNS 2022, Rome, Italy, June 20–23, 2022, Proceedings. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783031092343 - 9783031092336 ; 13269, s. 440-458
  • Conference paper (peer-reviewed)abstract
    • Digital signatures are widely deployed to authenticate the source of incoming information, or to certify data integrity. Common signature verification procedures return a decision (accept/reject) only at the very end of the execution. If interrupted prematurely, however, the verification process cannot infer any meaningful information about the validity of the given signature. We notice that this limitation is due to the algorithm design solely, and it is not inherent to signature verification.In this work, we provide a formal framework to handle interruptions during signature verification. In addition, we propose a generic way to devise alternative verification procedures that progressively build confidence on the final decision. Our transformation builds on a simple but powerful intuition and applies to a wide range of existing schemes considered to be post-quantum secure including the NIST finalist Rainbow.While the primary motivation of progressive verification is to mitigate unexpected interruptions, we show that verifiers can leverage it in two innovative ways. First, progressive verification can be used to intentionally adjust the soundness of the verification process. Second, progressive verifications output by our transformation can be split into a computationally intensive offline set-up (run once) and an efficient online verification that is progressive.
  •  
46.
  • Brakerski, Zvika, et al. (author)
  • Simple Tests of Quantumness Also Certify Qubits
  • 2023
  • In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 14085 LNCS, s. 162-191
  • Conference paper (peer-reviewed)abstract
    • A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as [KCVY21, KLVY22], can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation. Certifying qubits was previously only known to be possible based on families of post-quantum trapdoor claw-free functions (TCF) with an advanced “adaptive hardcore bit” property, which have only been constructed based on the hardness of the Learning with Errors problem [BCM+21] and recently isogeny-based group actions [AMR23]. Our framework allows certification of qubits based only on the existence of post-quantum TCF, without the adaptive hardcore bit property, or on quantum fully homomorphic encryption. These can be instantiated, for example, from Ring Learning with Errors. This has the potential to improve the efficiency of qubit certification and derived functionalities. On the technical side, we show that the quantum soundness of any such protocol can be reduced to proving a bound on a simple algorithmic task: informally, answering “two challenges simultaneously” in the protocol. Our reduction formalizes the intuition that these protocols demonstrate quantumness by leveraging the impossibility of rewinding a general quantum prover. This allows us to prove tight bounds on the quantum soundness of [KCVY21] and [KLVY22], showing that no quantum polynomial-time prover can succeed with probability larger than cos2π8≈0.853. Previously, only an upper bound on the success probability of classical provers, and a lower bound on the success probability of quantum provers, were known. We then extend this proof of quantum soundness to show that provers that approach the quantum soundness bound must perform almost anti-commuting measurements. This certifies that the prover holds a qubit.
  •  
47.
  • Brambilla, Andrea, et al. (author)
  • Complex Projects Assessment. The Impact of Built Environment on Healthcare Staff Wellbeing
  • 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. ; 12253 LNCS, s. 345-354
  • Conference paper (peer-reviewed)abstract
    • Projects, plans and programmes for complex environments such as healthcare facilities need to be designed with specific consideration of the multitude of users, technologies and policies in order to address a sustainable and resilient development. Several Evidence Based Design (EBD) studies highlight the deep interrelation between built and natural systems with human or organizations-related outcomes, but the effect on healthcare staff such as Medical Doctors (MD) is still underexplored. The paper investigates the assessment of self-reported satisfaction and wellbeing of MDs in healthcare facilities. A multidimensional assessment model composed of 53 Likert scale questions has been developed from literature review and existing tools, and submitted to a statistically significant sample of workers in 2 different office settings of an Italian hospital. Since MDs spend a considerable amount of their working time in offices, the qualities of such space are very important. The study highlights and confirms that localization, indoor environment, natural and artificial light are relevant drivers for staff satisfaction and wellbeing. Further investigations on a wider and diverse sample are encouraged.
  •  
48.
  • Brorsson, Joakim, et al. (author)
  • PAPR : Publicly Auditable Privacy Revocation for Anonymous Credentials
  • 2023
  • In: Topics in Cryptology – CT-RSA 2023 - Cryptographers’ Track at the RSA Conference 2023, Proceedings. - 1611-3349 .- 0302-9743. - 9783031308710 ; 13871 LNCS, s. 163-190
  • Conference paper (peer-reviewed)abstract
    • We study the notion of anonymous credentials with Publicly Auditable Privacy Revocation (PAPR). PAPR credentials simultaneously provide conditional user privacy and auditable privacy revocation. The first property implies that users keep their identity private when authenticating unless and until an appointed authority requests to revoke this privacy, retroactively. The second property enforces that auditors can verify whether or not this authority has revoked privacy from an issued credential (i.e. learned the identity of the user who owns that credential), holding the authority accountable. In other words, the second property enriches conditionally anonymous credential systems with transparency by design, effectively discouraging such systems from being used for mass surveillance. In this work, we introduce the notion of a PAPR anonymous credential scheme, formalize it as an ideal functionality, and present constructions that are provably secure under standard assumptions in the Universal Composability framework. The core tool in our PAPR construction is a mechanism for randomly selecting an anonymous committee which users secret share their identity information towards, while hiding the identities of the committee members from the authority. As a consequence, in order to initiate the revocation process for a given credential, the authority is forced to post a request on a public bulletin board used as a broadcast channel to contact the anonymous committee that holds the keys needed to decrypt the identity connected to the credential. This mechanism makes the user de-anonymization publicly auditable.
  •  
49.
  • Brunetta, Carlo, 1992, et al. (author)
  • Non-Interactive, Secure Verifiable Aggregation for Decentralized, Privacy-Preserving Learning
  • 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. ; 13083 LNCS, s. 510-5128
  • Conference paper (peer-reviewed)abstract
    • We propose a novel primitive called NIVA that allows the distributed aggregation of multiple users’ secret inputs by multiple untrusted servers. The returned aggregation result can be publicly verified in a non-interactive way, i.e. the users are not required to participate in the aggregation except for providing their secret inputs. NIVA allows the secure computation of the sum of a large amount of users’ data and can be employed, for example, in the federated learning setting in order to aggregate the model updates for a deep neural network. We implement NIVA and evaluate its communication and execution performance and compare it with the current state-of- the-art, i.e. Segal et al. protocol (CCS 2017) and Xu et al. VerifyNet protocol (IEEE TIFS 2020), resulting in better user’s communicated data and execution time.
  •  
50.
  • Brunetta, Carlo, 1992, et al. (author)
  • Turn-Based Communication Channels
  • 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. ; 13059 LNCS, s. 376-392
  • Conference paper (peer-reviewed)abstract
    • We introduce the concept of turn-based communication channel between two mutually distrustful parties with communication consistency, i.e. both parties have the same message history, and happens in sets of exchanged messages across a limited number of turns. Our construction leverages on timed primitives. Namely, we consider a Δ -delay hash function definition and use it to establish turns in the channel. Concretely, we introduce the one-way turn-based communication scheme and the two-way turn-based communication protocol and provide a concrete instantiation that achieves communication consistency.
  •  
Skapa referenser, mejla, bekava och länka
  • Result 1-50 of 279
Type of publication
conference paper (246)
journal article (20)
book chapter (13)
Type of content
peer-reviewed (265)
other academic/artistic (13)
pop. science, debate, etc. (1)
Author/Editor
Ahrendt, Wolfgang, 1 ... (10)
Schneider, Gerardo, ... (10)
Gay, Gregory, 1987 (8)
Nordström, Jakob (8)
Azzopardi, Shaun, 19 ... (7)
Johansson, Thomas (7)
show more...
Horkoff, Jennifer, 1 ... (7)
Knauss, Eric, 1977 (7)
Lingas, Andrzej (6)
Schiller, Elad, 1974 (6)
Pagnin, Elena (6)
Zach, Christopher, 1 ... (6)
Staron, Miroslaw, 19 ... (5)
Piterman, Nir, 1971 (5)
King, Ross, 1962 (5)
Mitrokotsa, Aikateri ... (5)
Bosch, Jan, 1967 (5)
Sattler, Torsten, 19 ... (5)
Myreen, Magnus, 1983 (4)
Afshari, Bahareh, 19 ... (4)
Leigh, Graham E., 19 ... (4)
Sabelfeld, Andrei, 1 ... (4)
Tsigas, Philippas, 1 ... (4)
Pericas, Miquel, 197 ... (4)
Runeson, Per (4)
Simonis, Helmut (4)
Felsberg, Michael (4)
Hell, Martin (4)
Guo, Qian (4)
Di Stefano, Luca, 19 ... (3)
Hughes, John, 1958 (3)
Tan, Yong Kiam (3)
Damaschke, Peter, 19 ... (3)
Wohlrab, Rebekka, 19 ... (3)
Pace, Gordon J. (3)
Johansson, Moa, 1981 (3)
Hebig, Regina, 1984 (3)
Alce, Günter (3)
Gulisano, Vincenzo M ... (3)
Oskarsson, Magnus (3)
Balkenius, Christian (3)
Taibi, Davide (3)
Johansson, Birger (3)
Tjøstheim, Trond A. (3)
Sminchisescu, Cristi ... (3)
Heyn, Hans-Martin, 1 ... (3)
Oertel, Andy (3)
Xie, Long (3)
Brunetta, Carlo, 199 ... (3)
Tsaloli, Georgia, 19 ... (3)
show less...
University
Chalmers University of Technology (138)
Lund University (80)
University of Gothenburg (67)
Royal Institute of Technology (7)
University West (6)
RISE (5)
show more...
Halmstad University (4)
Mälardalen University (4)
Malmö University (4)
Umeå University (3)
Uppsala University (3)
Stockholm University (3)
Luleå University of Technology (2)
University of Skövde (2)
Linnaeus University (2)
Karlstad University (2)
University of Gävle (1)
Örebro University (1)
Linköping University (1)
Jönköping University (1)
University of Borås (1)
Swedish Museum of Natural History (1)
Blekinge Institute of Technology (1)
VTI - The Swedish National Road and Transport Research Institute (1)
show less...
Language
English (279)
Research subject (UKÄ/SCB)
Natural sciences (239)
Engineering and Technology (114)
Social Sciences (38)
Humanities (11)
Medical and Health Sciences (7)

Year

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Close

Copy and save the link in order to return to this view