uu.seUppsala University Publications
Change search
Refine search result
1234567 151 - 200 of 358
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 151.
    Guan, Nan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Tang, Yue
    Wang, Yang
    Yi, Wang
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Delay analysis of structural real-time workload2015In: Proc. 18th Conference on Design, Automation and Test in Europe, Piscataway, NJ: IEEE, 2015, p. 223-228Conference paper (Refereed)
  • 152. Guan, Nan
    et al.
    Zhao, Mengying
    Xue, Chun Jason
    Liu, Yongpan
    Yi, Wang
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Modular performance analysis of energy-harvesting real-time networked systems2015In: Proc. 36th Real-Time Systems Symposium, IEEE Computer Society, 2015, p. 65-74Conference paper (Refereed)
  • 153.
    Hassani Bijarbooneh, Farshid
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Du, Wei
    Ngai, Edith C.-H.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Fu, Xiaoming
    Liu, Jiangchuan
    Cloud-assisted data fusion and sensor selection for Internet of Things2016In: IEEE Internet of Things Journal, ISSN 2327-4662, Vol. 3, no 3, p. 257-268Article in journal (Refereed)
  • 154.
    Haziza, Frédéric
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Few is Just Enough!: Small Model Theorem for Parameterized Verification and Shape Analysis2015Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This doctoral thesis considers the automatic verification of parameterized systems, i.e. systems with an arbitrary number of communicating components, such as mutual exclusion protocols, cache coherence protocols or heap manipulating programs. The components may be organized in various topologies such as words, multisets, rings, or trees.

    The task is to show correctness regardless of the size of the system and we consider two methods to prove safety:(i) a backward reachability analysis, using the well-quasi ordered framework and monotonic abstraction, and (ii) a forward analysis which only needs to inspect a small number of components in order to show correctness of the whole system. The latter relies on an abstraction function that views the system from the perspective of a fixed number of components. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state-space need not continue.

    Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable property. It has been, for example, successfully applied to verify a fine-grained model of Szymanski's mutual exclusion protocol. Finally, we applied the methods to solve the complex problem of verifying highly concurrent data-structures, in a challenging setting: We do not a priori bound the number of threads, the size of the data-structure, the domain of the data to store nor do we require the presence of a garbage collector. We successfully verified the concurrent Treiber's stack and Michael & Scott's queue, in the aforementioned setting.

    To the best of our knowledge, these verification problems have been considered challenging in the parameterized verification community and could not be carried out automatically by other existing methods.

    List of papers
    1. All for the price of few: (Parameterized verification through view abstraction)
    Open this publication in new window or tab >>All for the price of few: (Parameterized verification through view abstraction)
    2013 (English)In: Verification, Model Checking, and Abstract Interpretation, Springer Berlin/Heidelberg, 2013, p. 476-495Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    Springer Berlin/Heidelberg, 2013
    Series
    Lecture Notes in Computer Science ; 7737
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-190003 (URN)10.1007/978-3-642-35873-9_28 (DOI)978-3-642-35872-2 (ISBN)
    Conference
    VMCAI 2013, January 20-22, Rome, Italy
    Projects
    UPMARC
    Available from: 2013-01-09 Created: 2013-01-07 Last updated: 2015-11-10Bibliographically approved
    2. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
    Open this publication in new window or tab >>An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
    Show others...
    2013 (English)In: Tools and Algorithms for the Construction and Analysis of Systems, 2013Conference paper, Published paper (Refereed)
    Abstract [en]

    We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependen- cies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded num- ber of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state au- tomata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verifica- tion, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have imple- mented our method and used it to verify programs, some of which have not been verified by any other automatic method before.

    Keywords
    verification, pointer program, queue, stack, unbounded concurrency, specification, linearizability
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-191330 (URN)
    Conference
    19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 16-24 March, 2013, Rome, ITALY
    Projects
    UPMARC
    Available from: 2013-01-16 Created: 2013-01-10 Last updated: 2018-01-11Bibliographically approved
    3. Block me if you can!: Context-sensitive parameterized verification
    Open this publication in new window or tab >>Block me if you can!: Context-sensitive parameterized verification
    2014 (English)In: Static Analysis: SAS 2014, Springer, 2014, p. 1-17Conference paper, Published paper (Refereed)
    Abstract [en]

    We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski’s mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

    Place, publisher, year, edition, pages
    Springer, 2014
    Series
    Lecture Notes in Computer Science, ISSN 0302-9743 ; 8723
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-260087 (URN)10.1007/978-3-319-10936-7_1 (DOI)000360204700001 ()978-3-319-10935-0 (ISBN)
    Conference
    21st International Symposium, SAS 2014, September 11–13, Munich, Germany
    Projects
    UPMARC
    Available from: 2014-09-13 Created: 2015-08-15 Last updated: 2015-12-16Bibliographically approved
    4. Monotonic abstraction for programs with dynamic memory heaps
    Open this publication in new window or tab >>Monotonic abstraction for programs with dynamic memory heaps
    Show others...
    2008 (English)In: Computer Aided Verification / [ed] Gupta A, Malik S, Berlin: Springer-Verlag , 2008, p. 341-354Conference paper, Published paper (Refereed)
    Abstract [en]

    We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach.

    Place, publisher, year, edition, pages
    Berlin: Springer-Verlag, 2008
    Series
    Lecture Notes in Computer Science, ISSN 0302-9743 ; 5123
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-106059 (URN)10.1007/978-3-540-70545-1_33 (DOI)000257539900033 ()
    Conference
    20th International Conference on Computer Aided Verification Princeton, NJ, JUL 07, 2008
    Available from: 2009-06-13 Created: 2009-06-13 Last updated: 2018-01-13Bibliographically approved
    5. Parameterized tree systems
    Open this publication in new window or tab >>Parameterized tree systems
    Show others...
    2008 (English)In: Formal Techniques for Networked and Distributed Systems: FORTE 2008 / [ed] Suzuki K, Berlin: Springer-Verlag , 2008, p. 69-83Conference paper, Published paper (Refereed)
    Abstract [en]

    Several recent works have considered parameterized verification, i.e. automatic verification of systems consisting of an arbitrary number of finite-state processes organized in a linear array. The aim of this paper is to extend these works by giving a simple and efficient method to prove safety properties for systems with tree-like architectures. A process in the system is a finite-state automaton and a transition is performed jointly by a process and its parent and children processes. The method derives an over-approximation of the induced transition system, which allows the use of finite trees as symbolic representations of infinite sets of configurations. Compared to traditional methods for parameterized verification of systems with tree topologies, our method does not require the manipulation of tree transducers, hence its simplicity and efficiency. We have implemented a prototype which works well on several nontrivial tree-based protocols.

    Place, publisher, year, edition, pages
    Berlin: Springer-Verlag, 2008
    Series
    Lecture Notes in Computer Science, ISSN 0302-9743 ; 5048
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-106058 (URN)10.1007/978-3-540-68855-6_5 (DOI)000256666500005 ()978-3-540-68854-9 (ISBN)
    Conference
    28th International Conference on Formal Techniques for Networked and Distributed Systems Tokyo, JAPAN, JUN 10-13, 2008
    Available from: 2009-06-13 Created: 2009-06-13 Last updated: 2018-01-13Bibliographically approved
    6. Model checking race-freeness
    Open this publication in new window or tab >>Model checking race-freeness
    2008 (English)In: SIGARCH Computer Architecture News, ISSN 0163-5964, E-ISSN 1943-5851, Vol. 36, no 5, p. 72-79Article in journal (Refereed) Published
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-142914 (URN)10.1145/1556444.1556454 (DOI)
    Available from: 2011-01-17 Created: 2011-01-17 Last updated: 2018-01-12Bibliographically approved
    7. Parameterized verification through view abstraction
    Open this publication in new window or tab >>Parameterized verification through view abstraction
    2016 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, p. 495-516Article in journal (Refereed) Published
    Abstract [en]

    We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

    Keywords
    Parameterized systems; Safety; Small model properties; View abstraction
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-260089 (URN)10.1007/s10009-015-0406-x (DOI)000382011100003 ()
    Projects
    UPMARC
    Available from: 2015-11-23 Created: 2015-08-15 Last updated: 2017-12-04Bibliographically approved
  • 155.
    Haziza, Frédéric
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Biology, Department of Cell and Molecular Biology, Computational Biology and Bioinformatics. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Holík, Lukás
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Brno Univ Technol, CS-61090 Brno, Czech Republic..
    Meyer, Roland
    Univ Kaiserslautern, D-67663 Kaiserslautern, Germany..
    Wolff, Sebastian
    Univ Kaiserslautern, D-67663 Kaiserslautern, Germany..
    Pointer Race Freedom2016In: Verification, Model Checking, And Abstract Interpretation, VMCAI 2016, Springer, 2016, p. 393-412Conference paper (Refereed)
    Abstract [en]

    We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speedup of up to two orders of magnitude.

  • 156.
    Heintz, Fredrik
    et al.
    Linköpings Universitet.
    Mannila, Linda
    Linköpings Universitet.
    Nordén, Lars-Åke
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Parnes, Peter
    Luleå Tekniska Universitet.
    Regnell, Björn
    Lunds Universitet.
    Introducing Programming and Digital Competence in Swedish K–9 Education2017In: Informatics in Schools: Focus on Learning Programming, 2017Conference paper (Refereed)
  • 157.
    Hermans, Frederik
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    McNamara, Liam
    Sörös, Gábor
    Rohner, Christian
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Voigt, Thiemo
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Ngai, Edith
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    FOCUS: Robust visual codes for everyone2016In: Proc. 14th International Conference on Mobile Systems, Applications, and Services, New York: ACM Press, 2016, p. 319-332Conference paper (Refereed)
  • 158.
    Hojjat, Hossein
    et al.
    Rochester Institute of Technology, University of Tehran.
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    The Eldarica Horn Solver2018In: Formal Methods in Computer Aided Design, IEEE, 2018Conference paper (Refereed)
  • 159.
    Hojjat, Hossein
    et al.
    Cornell Univ, Ithaca, NY 14853 USA..
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    McClurg, Jedidiah
    CU Boulder, Boulder, CO USA..
    Cerny, Pavol
    CU Boulder, Boulder, CO USA..
    Foster, Nate
    Cornell Univ, Ithaca, NY 14853 USA..
    Optimizing Horn Solvers for Network Repair2016In: Proceedings of the 2016 16Th Conference on Formal Methods In Computer-Aided Design (FMCAD 2016) / [ed] Piskac, R Talupur, M, IEEE , 2016, p. 73-80Conference paper (Refereed)
    Abstract [en]

    Automatic program repair modifies a faulty program to make it correct with respect to a specification. Previous approaches have typically been restricted to specific programming languages and a fixed set of syntactical mutation techniques-e.g., changing the conditions of if statements. We present a more general technique based on repairing sets of unsolvable Horn clauses. Working with Horn clauses enables repairing programs from many different source languages, but also introduces challenges, such as navigating the large space of possible repairs. We propose a conservative semantic repair technique that only removes incorrect behaviors and does not introduce new behaviors. Our proposed framework allows the user to request the best repairs-it constructs an optimization lattice representing the space of possible repairs, and uses a novel local search technique that exploits heuristics to avoid searching through sub-lattices with no feasible repairs. To illustrate the applicability of our approach, we apply it to problems in software-defined networking (SDN), and illustrate how it is able to help network operators fix buggy configurations by properly filtering undesired traffic. We show that interval and Boolean lattices are effective choices of optimization lattices in this domain, and we enable optimization objectives such as modifying the minimal number of switches. We have implemented a prototype repair tool, and present preliminary experimental results on several benchmarks using real topologies and realistic repair scenarios in data centers and congested networks.

  • 160.
    Holik, Lukas
    et al.
    Brno University of Technology, Czech Republic.
    Janku, Petr
    Brno University of Technology, Czech Republic.
    Lin, Anthony W.
    University of Oxford, United Kingdom.
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Vojnar, Tomas
    Brno University of Technology, Czech Republic.
    String constraints with concatenation and transducers solved efficiently2018In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 2, p. 1-32, article id 4Article in journal (Refereed)
    Abstract [en]

    String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous applications including automatic detection of cross-site scripting, and automatic test-case generation. A popular string analysis technique includes symbolic executions, which at their core use constraint solvers over the string domain, a.k.a. string solvers. Such solvers typically reason about constraints expressed in theories over strings with the concatenation operator as an atomic constraint. In recent years, researchers started to recognise the importance of incorporating the replace-all operator (i.e. replace all occurrences of a string by another string) and, more generally, finite-state transductions in the theories of strings with concatenation. Such string operations are typically crucial for reasoning about XSS vulnerabilities in web applications, especially for modelling sanitisation functions and implicit browser transductions (e.g. innerHTML). Although this results in an undecidable theory in general, it was recently shown that the straight-line fragment of the theory is decidable, and is sufficiently expressive in practice. In this paper, we provide the first string solver that can reason about constraints involving both concatenation and finite-state transductions. Moreover, it has a completeness and termination guarantee for several important fragments (e.g. straight-line fragment). The main challenge addressed in the paper is the prohibitive worst-case complexity of the theory (double-exponential time), which is exponentially harder than the case without finite-state transductions. To this end, we propose a method that exploits succinct alternating finite-state automata as concise symbolic representations of string constraints. In contrast to previous approaches using nondeterministic automata, alternation offers not only exponential savings in space when representing Boolean combinations of transducers, but also a possibility of succinct representation of otherwise costly combinations of transducers and concatenation. Reasoning about the emptiness of the AFA language requires a state-space exploration in an exponential-sized graph, for which we use model checking algorithms (e.g. IC3). We have implemented our algorithm and demonstrated its efficacy on benchmarks that are derived from cross-site scripting analysis and other examples in the literature.

  • 161. Holik, Lukás
    et al.
    Isberner, Malte
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Mediator synthesis in a component algebra with data2015In: Correct System Design, Springer, 2015, p. 238-259Conference paper (Refereed)
    Abstract [en]

    We formulate a compositional specification theory for components that interact by directed synchronous communication actions. The theory is an extension of interface automata which is also able to capture both absence of deadlock as well as constraints on data parameters in interactions. We define refinement, parallel composition, and quotient. The quotient is an adjoint of parallel composition, and produces the most general component that makes the components cooperate to satisfy a given system specification. We show how these operations can be used to synthesize mediators that allow components in networked systems to interoperate. This is illustrated by application to the synthesis of mediators in e-commerce applications.

  • 162. Hu, Xiping
    et al.
    Chu, Terry H. S.
    Leung, Victor C. M.
    Ngai, Edith C.-H.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kruchten, Philippe
    Chan, Henry C. B.
    A survey on mobile social networks: Applications, platforms, system architectures, and future research directions2015In: IEEE Communications Surveys and Tutorials, ISSN 1553-877X, E-ISSN 1553-877X, Vol. 17, no 3, p. 1557-1581Article, review/survey (Refereed)
  • 163. Hu, Xiping
    et al.
    Deng, Junqi
    Zhao, Jidi
    Hu, Wenyan
    Ngai, Edith C.-H.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Wang, Renfei
    Shen, Johnny
    Liang, Min
    Li, Xitong
    Leung, Victor C. M.
    Kwok, Yu-Kwong
    SAfeDJ: A crowd-cloud codesign approach to situation-aware music delivery for drivers2015In: ACM Transactions on Multimedia Computing, Communications, and Applications (TOMCCAP), ISSN 1551-6857, E-ISSN 1551-6865, Vol. 12, no 1s, p. 21:1-24, article id 21Article in journal (Refereed)
    Abstract [en]

    Driving is an integral part of our everyday lives, but it is also a time when people are uniquely vulnerable. Previous research has demonstrated that not only does listening to suitable music while driving not impair driving performance, but it could lead to an improved mood and a more relaxed body state, which could improve driving performance and promote safe driving significantly. In this article, we propose SAfeDJ, a smartphone-based situation-aware music recommendation system, which is designed to turn driving into a safe and enjoyable experience. SAfeDJ aims at helping drivers to diminish fatigue and negative emotion. Its design is based on novel interactive methods, which enable in-car smartphones to orchestrate multiple sources of sensing data and the drivers' social context, in collaboration with cloud computing to form a seamless crowdsensing solution. This solution enables different smartphones to collaboratively recommend preferable music to drivers according to each driver's specific situations in an automated and intelligent manner. Practical experiments of SAfeDJ have proved its effectiveness in music-mood analysis, and mood-fatigue detections of drivers with reasonable computation and communication overheads on smartphones. Also, our user studies have demonstrated that SAfeDJ helps to decrease fatigue degree and negative mood degree of drivers by 49.09% and 36.35%, respectively, compared to traditional smartphone-based music player under similar driving situations.

  • 164. Hu, Xiping
    et al.
    Li, Xitong
    Ngai, Edith C.-H.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Zhao, Jidi
    Leung, Victor C. M.
    Nasiopoulos, Panos
    Health Drive: Mobile healthcare onboard vehicles to promote safe driving2015In: Proc. 48th Hawaii International Conference on System Sciences, IEEE Computer Society, 2015, p. 3074-3083Conference paper (Refereed)
  • 165.
    Hu, Xiping
    et al.
    Chinese Acad Sci, Shenzhen, Peoples R China.
    Ning, Zhaolong
    Dalian Univ Technol, Dalian, Peoples R China.
    Zhang, Kuan
    Univ Waterloo, Waterloo, ON, Canada.
    Ngai, Edith
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bai, Kun
    Tencent Co, Shenzhen, Peoples R China.
    Wang, Fei
    Cornell Univ, Ithaca, NY USA.
    Crowdsourcing for Mobile Networks and IoT2018In: Wireless Communications & Mobile Computing, ISSN 1530-8669, E-ISSN 1530-8677, article id 6231236Article in journal (Other academic)
  • 166.
    Huang, Weiwei
    et al.
    Sun Yat Sen Univ, Sch Data & Comp Sci, Guangzhou 510006, Guangdong, Peoples R China;Sun Yat Sen Univ, Guangdong Prov Key Lab Big Data Anal & Proc, Guangzhou 510006, Guangdong, Peoples R China.
    Zhou, Yipeng
    Macquarie Univ, Dept Comp, Fac Sci & Engn, Sydney, NSW 2109, Australia.
    Xie, Xueyan
    Sun Yat Sen Univ, Sch Data & Comp Sci, Guangzhou 510006, Guangdong, Peoples R China;Sun Yat Sen Univ, Guangdong Prov Key Lab Big Data Anal & Proc, Guangzhou 510006, Guangdong, Peoples R China.
    Wu, Di
    Sun Yat Sen Univ, Sch Data & Comp Sci, Guangzhou 510006, Guangdong, Peoples R China;Sun Yat Sen Univ, Guangdong Prov Key Lab Big Data Anal & Proc, Guangzhou 510006, Guangdong, Peoples R China.
    Chen, Min
    Huazhong Univ Sci & Technol, Sch Comp Sci & Technol, Wuhan 430074, Peoples R China;Huazhong Univ Sci & Technol, Wuhan Natl Lab Optoelect, Wuhan 430074, Peoples R China.
    Ngai, Edith
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Uppsala Univ, Dept Informat Technol, SE-75105 Uppsala, Sweden.
    Buffer State is Enough: Simplifying the Design of QoE-Aware HTTP Adaptive Video Streaming2018In: IEEE transactions on broadcasting, ISSN 0018-9316, E-ISSN 1557-9611, Vol. 64, no 2, p. 590-601Article in journal (Refereed)
    Abstract [en]

    Recently, the prevalence of mobile devices together with the outburst of user-generated contents has fueled the tremendous growth of the Internet traffic taken by video streaming. To improve user-perceived quality-of-experience (QoE), dynamic adaptive streaming via HTTP (DASH) has been widely adopted by practical systems to make streaming smooth under limited bandwidth. However, previous DASH approaches mostly performed complicated rate adaptation based on bandwidth estimation, which has been proven to be unreliable over HTTP. In this paper, we simplify the design by only exploiting client-side buffer state information and propose a pure buffer-based DASH scheme to optimize user QoE. Our approach can not only get rid of the drawback caused by inaccurate bandwidth estimation, but also incur very limited overhead. We explicitly define an integrated user QoE model, which takes playback freezing, bitrate switch, and video quality into account, and then formulate the problem into a non-linear stochastic optimal control problem. Next, we utilize control theory to design a dynamic buffer-based controller for DASH, which determines video bitrate of each chunk to be requested and stabilize the buffer level in the meanwhile. Extensive experiments have been conducted to validate the advantages of our approach, and the results show that our approach can achieve the best performance compared with other alternative approaches.

  • 167.
    Huvila, Isto
    et al.
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of ALM.
    Cajander, Åsa
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computerized Image Analysis and Human-Computer Interaction.
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Åhlfeldt, Rose-Mharie
    Patients' perceptions of their medical records from different subject positions2015In: Journal of the Association for Information Science and Technology, ISSN 2330-1635, E-ISSN 2330-1643, Vol. 66, no 12, p. 2456-2470Article in journal (Refereed)
  • 168.
    Huvila, Isto
    et al.
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of ALM.
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Cajander, Åsa
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computerized Image Analysis and Human-Computer Interaction.
    Åhlfeldt, Rose-Mharie
    Patients reading their medical records: Differences in experiences and attitudes between regular and inexperienced readers2016In: Information research, ISSN 1368-1613, E-ISSN 1368-1613, Vol. 21, no 1, article id 706Article in journal (Refereed)
  • 169.
    Hylamia, Abdullah
    et al.
    KTH Royal Inst Technol, Stockholm, Sweden.
    Spanghero, Marco
    KTH Royal Inst Technol, Stockholm, Sweden.
    Varshney, Ambuj
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Voigt, Thiemo
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. RISE SICS, Stockholm, Sweden.
    Papadimitratos, Panagiotis
    KTH Royal Inst Technol, Stockholm, Sweden.
    Demo: Security on Harvested Power2018In: WISEC'18: PROCEEDINGS OF THE 11TH ACM CONFERENCE ON SECURITY & PRIVACY IN WIRELESS AND MOBILE NETWORKS, ASSOC COMPUTING MACHINERY , 2018, p. 296-298Conference paper (Refereed)
    Abstract [en]

    Security mechanisms for battery-free devices have to operate under severe energy constraints relying on harvested energy. This is challenging, as the energy harvested from the ambient environment is usually scarce, intermittent and unpredictable. One of the challenges for developing security mechanisms for such settings is the lack of hardware platforms that recreate energy harvesting conditions experienced on a battery-free sensor node. In this demonstration, we present an energy harvesting security (EHS) platform that enables the development of security algorithms for battery-free sensors. Our results demonstrate that our platform is able to harvest sufficient energy from indoor lighting to support several widely used cryptography algorithms.

  • 170.
    Hylamia, Abdullah
    et al.
    KTH Royal Inst Technol, Stockholm, Sweden.
    Varshney, Ambuj
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Soleiman, Andreas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Papadimitratos, Panagiotis
    KTH Royal Inst Technol, Stockholm, Sweden.
    Rohner, Christian
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Voigt, Thiemo
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. RISE SICS, Stockholm, Sweden.
    Demo: Towards Battery-free Radio Tomographic Imaging2018In: WISEC'18: PROCEEDINGS OF THE 11TH ACM CONFERENCE ON SECURITY & PRIVACY IN WIRELESS AND MOBILE NETWORKS, ASSOC COMPUTING MACHINERY , 2018, p. 293-295Conference paper (Refereed)
    Abstract [en]

    Radio Tomographic Imaging (RTI) enables novel radio frequency (RF) sensing applications such as intrusion detection systems by observing variations in radio links caused by human actions. RTI applications are, however, severely limited by the requirement to retrofit existing infrastructure with energy-expensive sensors. In this demonstration, we present our ongoing efforts to develop the first battery-free RTI system that operates on minuscule amounts of energy harvested from the ambient environment. Our system eliminates the energy-expensive components employed on state-of-the-art RTI systems achieving two orders of magnitude lower power consumption. Battery-free operation enables a sustainable deployment, as RTI sensors could be deployed for long periods of time with little maintenance effort. Our demonstration showcases an intrusion detection scenario enabled by our system.

  • 171.
    Isbister, Tim
    et al.
    Swedish Def Res Agcy FOI, Stockholm, Sweden..
    Kaati, Lisa
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Swedish Def Res Agcy FOI, Stockholm, Sweden..
    Cohen, Katie
    Swedish Def Res Agcy FOI, Stockholm, Sweden..
    Gender Classification with Data Independent Features in Multiple Languages2017In: 2017 European Intelligence and Security Informatics Conference (EISIC) / [ed] Brynielsson, J, IEEE, 2017, p. 54-60Conference paper (Refereed)
    Abstract [en]

    Gender classification is a well-researched problem, and state-of-the-art implementations achieve an accuracy of over 85%. However, most previous work has focused on gender classification of texts written in the English language, and in many cases, the results cannot be transferred to different datasets since the features used to train the machine learning models are dependent on the data. In this work, we investigate the possibilities to classify the gender of an author on five different languages: English, Swedish, French, Spanish, and Russian. We use features of the word counting program Linguistic Inquiry and Word Count (LIWC) with the benefit that these features are independent of the dataset. Our results show that by using machine learning with features from LIWC, we can obtain an accuracy of 79% and 73% depending on the language. We also, show some interesting differences between the uses of certain categories among the genders in different languages.

  • 172. Isomöttönen, Ville
    et al.
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Cajander, Åsa
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computerized Image Analysis and Human-Computer Interaction.
    Pears, Arnold
    McDermott, Roger
    Searching for global employability: Can students capitalize on enabling learning environments?2019In: ACM Transactions on Computing Education, ISSN 1946-6226, E-ISSN 1946-6226, Vol. 19, no 2, p. 11:1-29, article id 11Article in journal (Refereed)
  • 173.
    Janzén, Johan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Black-Schaffer, David
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Hugo, Andra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Partitioning GPUs for Improved Scalability2016In: Proc. 28th International Symposium on Computer Architecture and High Performance Computing, IEEE Computer Society, 2016, p. 42-49Conference paper (Refereed)
    Abstract [en]

    To port applications to GPUs, developers need to express computational tasks as highly parallel executions with tens of thousands of threads to fill the GPU's compute resources. However, while this will fill the GPU's resources, it does not necessarily deliver the best efficiency, as the task may scale poorly when run with sufficient parallelism to fill the GPU. In this work we investigate how we can improve throughput by co-scheduling poorly-scaling tasks on sub-partitions of the GPU to increase utilization efficiency. We first investigate the scalability of typical HPC tasks on GPUs, and then use this insight to improve throughput by extending the StarPU framework to co-schedule tasks on the GPU. We demonstrate that co-scheduling poorly-scaling GPU tasks accelerates the execution of the critical tasks of a Cholesky Factorization and improves the overall performance of the application by 9% across a wide range of block sizes.

  • 174.
    Jiang, Xu
    et al.
    Hong Kong Polytech Univ, Hong Kong, Hong Kong, Peoples R China.;Beihang Univ, Sch Comp Sci & Engn, State Key Lab Virtual Real Technol & Syst, Beijing, Peoples R China..
    Guan, Nan
    Hong Kong Polytech Univ, Hong Kong, Hong Kong, Peoples R China..
    Long, Xiang
    Beihang Univ, Sch Comp Sci & Engn, State Key Lab Virtual Real Technol & Syst, Beijing, Peoples R China..
    Yi, Wang
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Northeastern Univ, Shenyang, Liaoning, Peoples R China..
    Semi-Federated Scheduling of Parallel Real-Time Tasks on Multiprocessors2017In: 2017 IEEE Real-Time Systems Symposium (RTSS), IEEE, 2017, p. 80-91Conference paper (Refereed)
    Abstract [en]

    Federated scheduling is a promising approach to schedule parallel real-time tasks on multi-cores, where each heavy task exclusively executes on a number of dedicated processors, while light tasks are treated as sequential sporadic tasks and share the remaining processors. However, federated scheduling suffers resource waste since a heavy task with processing capacity requirement x + is an element of (where x is an integer and 0 < is an element of < 1) needs x+ 1 dedicated processors. In the extreme case, almost half of the processing capacity is wasted. In this paper we propose the semi-federate scheduling approach, which only grants x dedicated processors to a heavy task with processing capacity requirement x+ is an element of, and schedules the remaining is an element of part together with light tasks on shared processors. Experiments with randomly generated task sets show the semi-federated scheduling approach significantly outperforms not only federated scheduling, but also all existing approaches for scheduling parallel real-time tasks on multi-cores.

  • 175. Jin, Xi
    et al.
    Guan, Nan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Wang, Jintao
    Zeng, Peng
    Analyzing multimode wireless sensor networks using the network calculus2015In: Journal of Sensors, ISSN 1687-725X, E-ISSN 1687-7268, Vol. 2015, p. 851608:1-12, article id 851608Article in journal (Refereed)
    Abstract [en]

    The network calculus is a powerful tool to analyze the performance of wireless sensor networks. But the original network calculus can only model the single-mode wireless sensor network. In this paper, we combine the original network calculus with the multimode model to analyze the maximum delay bound of the flow of interest in the multimode wireless sensor network. There are two combined methods A-MM and N-MM. The method A-MM models the whole network as a multimode component, and the method N-MM models each node as a multimode component. We prove that the maximum delay bound computed by the method A-MM is tighter than or equal to that computed by the method N-MM. Experiments show that our proposed methods can significantly decrease the analytical delay bound comparing with the separate flow analysis method. For the large-scale wireless sensor network with 32 thousands of sensor nodes, our proposed methods can decrease about 70% of the analytical delay bound.

  • 176. Johansson, Fredrik
    et al.
    Kaati, Lisa
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Timeprints for identifying social media users with multiple aliases2015In: Security Informatics, ISSN 2190-8532, Vol. 4, p. 7:1-11, article id 7Article in journal (Refereed)
  • 177.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    The Quest for Optimality in Stateless Model Checking of Concurrent Programs2018In: Formal Methods For Industrial Critical Systems, FMICS 2018 / [ed] Howar, F Barnat, J, Springer, 2018, p. XI-XIIConference paper (Refereed)
  • 178. Jónsson, Björn Þór
    et al.
    Lárusdóttir, Marta Kristín
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Clear, Alison
    Clear, Tony
    McDermott, Roger
    Aligning quality assurance at the course unit and educational program levels2016In: Proc. 46th ASEE/IEEE Frontiers in Education Conference, Piscataway, NJ: IEEE Press, 2016Conference paper (Refereed)
    Abstract [en]

    Quality assurance is a subject that has grown dramatically in importance in recent times. In previous work, we have described how the ACM Curricula can be used to support the Quality Assurance process of educational programs, using the Computer Science program at Reykjavik University as an example. Faculty members and employers of graduates participated in the process, that resulted in providing both detailed quantitative data and qualitative information. The assessment also raised awareness of how abstract topics and learning outcomes from an international standard can be used when revising the curricula of a particular course in a CS program. Quality assurance is indeed a continuous process, where the results of evaluations should be used to drive improvements. In this paper we focus on how a Database course was re-structured based on a recent quality assurance process.

  • 179.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Johansson, Fredrik
    Countering lone actor terrorism: Weak signals and online activities2016In: Understanding Lone Actor Terrorism: Past experience, future outlook, and response strategies, Abingdon, UK: Routledge, 2016, p. 266-279Chapter in book (Refereed)
  • 180.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Johansson, Fredrik
    Forsman, Elinor
    Semantic technologies for detecting names of new drugs on darknets2016In: Proc. 4th International Conference on Cybercrime and Computer Forensics, IEEE, 2016Conference paper (Refereed)
  • 181.
    Kaati, Lisa
    et al.
    FOI, Stockholm, Sweden..
    Lundeqvist, Elias
    FOI, Stockholm, Sweden..
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Svensson, Maria
    FOI, Stockholm, Sweden..
    Author Profiling in the Wild2017In: 2017 European Intelligence and Security Informatics Conference (EISIC) / [ed] Brynielsson, J, IEEE, 2017, p. 155-158Conference paper (Refereed)
    Abstract [en]

    In this paper, we use machine learning for profiling authors of online textual media. We are interested in determining the gender and age of an author. We use two different approaches, one where the features are learned from raw data and one where features are manually extracted. We are interested in understanding how well author profiling works in the wild and therefore we have tested our models on different domains than they are trained on. Our results show that applying models to a different domain then they were trained on significantly decreases the performance of the models. The results show that more efforts need to be put into making models domain independent if techniques such as author profiling should be used operationally, for example by training on many different datasets and by using domain independent features.

  • 182.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Omer, Enghin
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Prucha, Nico
    ICSR, London, England.
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Detecting multipliers of jihadism on twitter2015In: Proc. 15th ICDM Workshops, IEEE Computer Society, 2015, p. 954-960Conference paper (Refereed)
    Abstract [en]

    Detecting terrorist related content on social media is a problem for law enforcement agency due to the large amount of information that is available. In this paper we describe a first step towards automatically classifying twitter user accounts (tweeps) as supporters of jihadist groups who disseminate propaganda content online. We use a machine learning approach with two set of features: data dependent features and data independent features. The data dependent features are features that are heavily influenced by the specific dataset while the data independent features are independent of the dataset and that can be used on other datasets with similar result. By using this approach we hope that our method can be used as a baseline to classify violent extremist content from different kind of sources since data dependent features from various domains can be added.

  • 183.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Cohen, Katie
    Linguistic analysis of lone offender manifestos2016In: Proc. 4th International Conference on Cybercrime and Computer Forensics, IEEE, 2016Conference paper (Refereed)
  • 184.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Cohen, Katie
    Lindquist, Sinna
    Automatic detection of xenophobic narratives: A case study on Swedish alternative media2016In: Proc. 14th International Conference on Intelligence and Security Informatics, IEEE, 2016, p. 121-126Conference paper (Refereed)
  • 185.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Sardella, Tony
    Washington Univ, St Louis, MO USA..
    Identifying Warning Behaviors of Violent Lone Offenders in Written Communication2016In: 2016 IEEE 16Th International Conference On Data Mining Workshops (ICDMW) / [ed] Domeniconi, C Gullo, F Bonchi, F DomingoFerrer, J BaezaYates, R Zhou, ZH Wu, X, New York: IEEE, 2016, p. 1053-1060Conference paper (Refereed)
    Abstract [en]

    Violent lone offenders such as school shooters and lone actor terrorists pose a threat to the modern society but since they act alone or with minimal help form others they are very difficult to detect. Previous research has shown that violent lone offenders show signs of certain psychological warning behaviors that can be viewed as indicators of an increasing or accelerating risk of committing targeted violence. In this work, we use a machine learning approach to identify potential violent lone offenders based on their written communication. The aim of this work is to capture psychological warning behaviors in written text and identify texts written by violent lone offenders. We use a set of features that are psychologically meaningful based on the different categories in the text analysis tool Linguistic Inquiry and Word Count (LIWC). Our study only contains a small number of known perpetrators and their written communication but the results are promising and there are many interesting directions for future work in this area.

  • 186.
    Kaati, Lisa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Shrestha, Amendra
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Sardella, Tony
    Identifying warning behaviors of violent lone offenders in written communication2016In: Proc. 16th ICDM Workshops, IEEE Computer Society, 2016, p. 1053-1060Conference paper (Refereed)
  • 187.
    Kahsai, Temesghen
    et al.
    Carnegie Mellon University, Silicon Valley; NASA Ames.
    Kersten, Rody
    Carnegie Mellon University, Silicon Valley.
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Schäf, Martin
    SRI International.
    Quantified heap invariants for object-oriented programs2017In: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017, p. 368-384Conference paper (Refereed)
  • 188.
    Kahsai, Temesghen
    et al.
    Nasa Ames CMU, Moffett Field, CA USA.
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Sanchez, Huascar
    SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA.
    Schäf, Martin
    SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA.
    JayHorn: A framework for verifying Java programs2016In: Computer Aided Verification: Part I, Springer, 2016, p. 352-358Conference paper (Refereed)
    Abstract [en]

    Building a competitive program verifiers is becoming cheaper. On the front-end side, openly available compiler infrastructure and optimization frameworks take care of hairy problems such as alias analysis, and break down the subtleties of modern languages into a handful of simple instructions that need to be handled. On the back-end side, theorem provers start providing full-fledged model checking algorithms, such as PDR, that take care looping control-flow. In this spirit, we developed JayHorn, a verification framework for Java with the goal of having as few moving parts as possible. Most steps of the translation from Java into logic are implemented as bytecode transformations, with the implication that their soundness can be tested easily. From the transformed bytecode, we generate a set of constrained Horn clauses that are verified using state-of-the-art Horn solvers. We report on our implementation experience and evaluate JayHorn on benchmarks.

  • 189.
    Kaxiras, Stefanos
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Carlson, Trevor E.
    Natl Univ Singapore, Dept Comp Sci, Singapore, Singapore.
    Alipour, Mehdi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Ros, Alberto
    Univ Murcia, Comp Engn Dept, Murcia, Spain.
    Non-Speculative Load Reordering in Total Store Ordering2018In: IEEE Micro, ISSN 0272-1732, E-ISSN 1937-4143, Vol. 38, no 3, p. 48-57Article in journal (Refereed)
    Abstract [en]

    Load reordering is important for performance. It allows a core to continue performing accesses to the memory system even when there are older, in-program-order, unperformed accesses (for example, due to long latency misses). The only known solution to allow such reordering in a strong consistency model such as total store ordering (TSO) has been to reorder speculatively and squash-and-re-execute if caught. We show, for the first time, that we can do the load reordering non-speculatively and leave it to the coherence protocol to handle conflicts. We can do this efficiently (without perceptible hardware or performance cost) and without deadlocks or livelocks. The important new result is that we can now irrevocably bind speculative loads. Our solution allows us to commit reordered loads out of order without having to wait (for the loads to become non-speculative) or checkpoint committed state (and rollback if needed), just to ensure correctness in the rare case of another core seeing the reordering.

  • 190. Kinnunen, Päivi
    et al.
    Butler, Matthew
    Morgan, Michael
    Nylén, Aletta
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Peters, Anne-Kathrin
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Sinclair, Jane
    Kalvala, Sara
    Pesonen, Erkki
    Understanding initial undergraduate expectations and identity in computing studies2018In: European Journal of Engineering Education, ISSN 0304-3797, E-ISSN 1469-5898, Vol. 43, no 2, p. 201-218Article in journal (Refereed)
    Abstract [en]

    There is growing appreciation of the importance of understanding thestudent perspective in Higher Education (HE) at both institutional andinternational levels. This is particularly important in Science, Technology,Engineering and Mathematics subjects such as Computer Science (CS)and Engineering in which industry needs are high but so are studentdropout rates. An important factor to consider is the management ofstudents’initial expectations of university study and career. This paperreports on a study of CSfirst-year students’expectations across threeEuropean countries using qualitative data from student surveys andessays. Expectation is examined from both short-term (topics to bestudied) and long-term (career goals) perspectives. Tackling these issueswill help paint a picture of computing education through students’eyesand explore their vision of its and their role in society. It will also helpeducators prepare students more effectively for university study and toimprove the student experience.

  • 191.
    Klebanov, Vladimir
    et al.
    Karlsruhe Inst Technol, Inst Theoret Informat, Karlsruhe, Germany.
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Ulbrich, Mattias
    Karlsruhe Inst Technol, Inst Theoret Informat, Karlsruhe, Germany.
    Automating regression verification of pointer programs by predicate abstraction2018In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 52, no 3, p. 229-259Article in journal (Refereed)
    Abstract [en]

    Regression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a novel automated approach for regression verification that reduces the equivalence of two related imperative pointer programs to constrained Horn clauses over uninterpreted predicates. Subsequently, state-of-the-art SMT solvers are used to solve the clauses. We have implemented the approach, and our experiments show that non-trivial programs with integer and pointer arithmetic can now be proved equivalent without further user input.

  • 192.
    Krcal, Jan
    et al.
    Univ Saarland, Comp Sci, Saarbrucken, Germany..
    Krcal, Pavel
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Lloyds Register Consulting, Stockholm, Sweden..
    Scalable Analysis of Fault Trees with Dynamic Features2015In: 2015 45Th Annual IEEE/IFIP International Conference On Dependable Systems And Networks, 2015, p. 89-100Conference paper (Refereed)
    Abstract [en]

    Fault trees constitute one of the essential formalisms for static safety analysis of various industrial systems. Dynamic fault trees (DFT) enrich the formalism by time-dependent behavior, e.g., repairs or functional dependencies. Analysis of DFT is so far limited to substantially smaller models than those required for, e.g., nuclear power plants. We propose a fault tree formalism that combines both static and dynamic features, called SD fault trees. It gives the user the freedom to express each equipment failure either statically, without modeling temporal information, or dynamically, allowing repairs and other timed interdependencies. We introduce an analysis algorithm for an important subclass of SD fault trees. The algorithm (1) scales similarly to static algorithms and (2) allows for a more realistic analysis compared to static algorithms as it takes into account temporal interdependencies. Finally, we demonstrate the applicability of the method by an experimental evaluation on fault trees of nuclear power plants.

  • 193.
    Krzywda, Jakub
    et al.
    Umea Univ, Dept Comp Sci, SE-90187 Umea, Sweden..
    Ali-Eldin, Ahmed
    Umea Univ, Dept Comp Sci, SE-90187 Umea, Sweden..
    Carlson, Trevor E.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Natl Univ Singapore, Sch Comp, 13 Comp Dr, Singapore 117417, Singapore.
    Östberg, Per-Olov
    Umea Univ, Dept Comp Sci, SE-90187 Umea, Sweden..
    Elmroth, Erik
    Umea Univ, Dept Comp Sci, SE-90187 Umea, Sweden..
    Power-performance tradeoffs in data center servers: DVFS, CPU pinning, horizontal, and vertical scaling2018In: Future generations computer systems, ISSN 0167-739X, E-ISSN 1872-7115, Vol. 81, p. 114-128Article in journal (Refereed)
    Abstract [en]

    Dynamic Voltage and Frequency Scaling (DVFS), CPU pinning, horizontal, and vertical scaling, are four techniques that have been proposed as actuators to control the performance and energy consumption on data center servers. This work investigates the utility of these four actuators, and quantifies the power-performance tradeoffs associated with them. Using replicas of the German Wikipedia running on our local testbed, we perform a set of experiments to quantify the influence of DVFS, vertical and horizontal scaling, and CPU pinning on end-to-end response time (average and tail), throughput, and power consumption with different workloads. Results of the experiments show that DVFS rarely reduces the power consumption of underloaded servers by more than 5%, but it can be used to limit the maximal power consumption of a saturated server by up to 20% (at a cost of performance degradation). CPU pinning reduces the power consumption of underloaded server (by up to 7%) at the cost of performance degradation, which can be limited by choosing an appropriate CPU pinning scheme. Horizontal and vertical scaling improves both the average and tail response time, but the improvement is not proportional to the amount of resources added. The load balancing strategy has a big impact on the tail response time of horizontally scaled applications.

  • 194.
    Kumar, Rakesh
    et al.
    Norwegian Univ Sci & Technol NTNU, Trondheim, Norway.
    Alipour, Mehdi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Black-Schaffer, David
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Freeway: Maximizing MLP for Slice-Out-of-Order Execution2019In: 2019 25th IEEE International Symposium On High Performance Computer Architecture (HPCA), IEEE, 2019, p. 558-569Conference paper (Refereed)
    Abstract [en]

    Exploiting memory level parallelism (MLP) is crucial to hide long memory and last level cache access latencies. While out-of-order (OoO) cores, and techniques building on them, are effective at exploiting MLP, they deliver poor energy efficiency due to their complex hardware and the resulting energy overheads. As energy efficiency becomes the prime design constraint, we investigate low complexity/energy mechanisms to exploit MLP. This work revisits slice-out-of-order (sOoO) cores as an energy efficient alternative to OoO cores for MLP exploitation. These cores construct slices of MLP generating instructions and execute them out-of-order with respect to the rest of instructions. However, the slices and the remaining instructions, by themselves, execute in-order. Though their energy overhead is low compared to full OoO cores, sOoO cores fall considerably behind in terms of MLP extraction. We observe that their dependence-oblivious inorder slice execution causes dependent slices to frequently block MLP generation. To boost MLP generation in sOoO cores, we introduce Freeway, a sOoO core based on a new dependence-aware slice execution policy that tracks dependent slices and keeps them out of the way of MLP extraction. The proposed core incurs minimal area and power overheads, yet approaches the MLP benefits of fully OoO cores. Our evaluation shows that Freeway outperforms the state-of-the-art sOoO core by 12% and is within 7% of the MLP limits of full OoO execution.

  • 195.
    Kumar, Rakesh
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Univ Edinburgh, Edinburgh, Midlothian, Scotland.
    Grot, Boris
    Univ Edinburgh, Edinburgh, Midlothian, Scotland.
    Nagarajan, Vijay
    Univ Edinburgh, Edinburgh, Midlothian, Scotland.
    Blasting Through The Front-End Bottleneck With Shotgun2018In: ACM Sigplan Notices, 2018, Vol. 53, no 2, p. 30-42Conference paper (Refereed)
    Abstract [en]

    The front-end bottleneck is a well-established problem in server workloads owing to their deep software stacks and large instruction working sets. Despite years of research into effective L1-I and BTB prefetching, state-of-the-art techniques force a trade-off between performance and metadata storage costs. This work introduces Shotgun, a BTB-directed front-end prefetcher powered by a new BTB organization that maintains a logical map of an application's instruction footprint, which enables high-efficacy prefetching at low storage cost. To map active code regions, Shotgun precisely tracks an application's global control flow (e.g., function and trap routine entry points) and summarizes local control flow within each code region. Because the local control flow enjoys high spatial locality, with most functions comprised of a handful of instruction cache blocks, it lends itself to a compact region-based encoding. Meanwhile, the global control flow is naturally captured by the application's unconditional branch working set (calls, returns, traps). Based on these insights, Shotgun devotes the bulk of its BTB capacity to branches responsible for the global control flow and a spatial encoding of their target regions. By effectively capturing a map of the application's instruction footprint in the BTB, Shotgun enables highly effective BTB-directed prefetching. Using a storage budget equivalent to a conventional BTB, Shotgun outperforms the state-of-the-art BTB-directed front-end prefetcher by up to 14% on a set of varied commercial workloads.

  • 196.
    Lampka, Kai
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bondorf, Steffen
    TU Kaiserslautern, Kaiserslautern, Germany..
    Schmitt, Jens
    TU Kaiserslautern, Kaiserslautern, Germany..
    Achieving Efficiency Without Sacrificing Model Accuracy: Network Calculus on Compact Domains2016In: 2016 IEEE 24Th International Symposium On Modeling, Analysis And Simulation Of Computer And Telecommunication Systems (MASCOTS), 2016, p. 313-318Conference paper (Refereed)
    Abstract [en]

    Messages traversing a network commonly experience waiting times due to sharing the forwarding resources. During those times, the crossed systems must provide sufficient buffer space for queueing messages. Network Calculus (NC) is a mathematical methodology for bounding flow delays and system buffer requirements. The accuracy of these performance bounds depends mainly on two factors: the principles manifesting in the NC flow equation and the functions describing the system. We focus on the latter aspect. Common implementations of NC overapproximate these functions in order to keep the analysis computationally feasible. However, overapproximation often results in a loss of accuracy of the performance bounds. In this paper, we make such compromising tradeoffs between model accuracy and computational effort obsolete. We limit the accurate system description to functions of a compact domain, such that the accuracy of the NC analysis is preserved. Tying the domain bound to the algebraic operators of NC instead of the operational semantics of components, allows us to directly apply our solution to algebraic NC analyses that implement principles such as pay burst only once and pay multiplexing only once.

  • 197.
    Lampka, Kai
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Elektrobit Automot, Erlangen, Germany..
    Bondorf, Steffen
    Univ Kaiserslautern, Distributed Comp Syst DISCO Lab, Kaiserslautern, Germany..
    Schmitt, Jens B.
    Univ Kaiserslautern, Distributed Comp Syst DISCO Lab, Kaiserslautern, Germany..
    Guan, Nan
    Hong Kong Polytech Univ, Dept Comp, Hong Kong, Hong Kong, Peoples R China..
    Wang, Yi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Generalized Finitary Real-Time Calculus2017In: IEEE INFOCOM 2017 - IEEE Conference on Computer Communications, IEEE, 2017Conference paper (Other academic)
    Abstract [en]

    Real-time Calculus (RTC) is a non-stochastic queuing theory to the worst-case performance analysis of distributed real-time systems. Workload as well as resources are modelled as piece-wise linear, pseudo-periodic curves and the system under investigation is modelled as a sequence of algebraic operations over these curves. The memory footprint of computed curves increases exponentially with the sequence of operations and RTC may become computationally infeasible fast. Recently, Finitary RTC has been proposed to counteract this problem. Finitary RTC restricts curves to finite input domains and thereby counteracts the memory demand explosion seen with pseudo periodic curves of common RTC implementations. However, the proof to the correctness of Finitary RTC specifically exploits the operational semantic of the greed processing component (GPC) model and is tied to the maximum busy window size. This is an inherent limitation, which prevents a straight-forward generalization. In this paper, we provide a generalized Finitary RTC that abstracts from the operational semantic of a specific component model and reduces the finite input domains of curves even further. The novel approach allows for faster computations and the extension of the Finitary RTC idea to a much wider range of RTC models.

  • 198.
    Lampka, Kai
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Forsberg, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Keep it slow and in time: Online DVFS with hard real-time workloads2016In: Proc. 19th Conference on Design, Automation and Test in Europe, Piscataway, NJ: IEEE , 2016, p. 385-390Conference paper (Refereed)
    Abstract [en]

    To handle hot spots or power shortages, modern multicore processors are equipped with a supervisory dynamic thermal and power management (DTPM) system. When necessary, the DTPM system autonomously adapts the capacity of the cooling system or throttles the speed of core-local clocks via dynamic voltage and frequency scaling (DVFS) techniques. Opposed to best-effort scenarios, online DVFS with real-time workloads also needs to consider completion times of computations. Whereas execution times can be bounded adequately with worst-case estimates, arrival times of computation requests are potentially unknown. A deadline for completing a computation can easily be missed, if workloads suddenly peak and past clock speed assignments have built-up a non-negligible backlog of computations. To overcome this problem, we introduce an online DVFS management scheme which is history-aware. It operates a core at higher speed levels only if the future workload has the potential to result in timing violations, if not anticipated by rising clock speed assignments. We present an implementation of the scheme running on the GemS hardware simulator.

  • 199.
    Lampka, Kai
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Forsberg, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Spiliopoulos, Vasileios
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Keep it cool and in time: With runtime monitoring to thermal-aware execution speeds for deadline constrained systems2016In: Journal of Parallel and Distributed Computing, ISSN 0743-7315, E-ISSN 1096-0848, Vol. 95, p. 79-91Article in journal (Refereed)
    Abstract [en]

    The Dynamic Power and Thermal Management (DPTM) system of Dynamic Voltage Frequency Scaling (DVFS) enabled processors compensates peak temperatures by slowing or even powering parts of the system down. While ensuring the integrity of computations, this comes with the drawback of losing performance. In the context of hard real-time systems, such unpredictable losses in performance are unacceptable, as they may lead to deadline misses which may yet compromise the integrity of the system. To safely execute hard real-time workloads on such systems, this article presents an online scheme for assigning speeds in such a way that (a) the system executes at low clock speed as often as possible, while (b) deadline violations are strictly ruled out. The proposed scheme is compared with an offline scheme which has complete knowledge about arrival times and execution demands of the workload. The benchmarking shows that for a workload which is always very close to the modelled maximum, our approach performs on-par with the offline scheme. In case of a workload which diverges from the modelled maximum more often, the speed assignments produced by our scheme become more pessimistic, as to ensure that all deadlines are met.

  • 200.
    Lampka, Kai
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Lackorzynski, Adam
    Resolving contention for networks-on-chips: Combining time-triggered application scheduling with dynamic budgeting of memory bus use2016In: Measurement, Modelling and Evaluation of Dependable Computer and Communication Systems, Springer, 2016, p. 137-152Conference paper (Refereed)
1234567 151 - 200 of 358
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf