Ändra sökning
Avgränsa sökresultatet
123 1 - 50 av 134
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Träffar per sida
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
Markera
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Artho, Cyrille
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Visser, W.
    Java Pathfinder at SV-COMP 2019 (Competition Contribution)2019Ingår i: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Springer, 2019, Vol. 11429, s. 224-228Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

  • 2.
    Artho, Cyrille
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Ölveczky, P.C.
    Formal Techniques for Safety-Critical Systems (FTSCS 2015)2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 154, s. 1-2Artikel i tidskrift (Refereegranskat)
  • 3.
    Artho, Cyrille
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Ölveczky, P.C.
    Formal Techniques for Safety-Critical Systems (FTSCS 2016)2019Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 175, s. 35-36Artikel i tidskrift (Refereegranskat)
  • 4.
    Asif, Rizwan
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Centrum för autonoma system, CAS.
    Löffel, Hendrik Jan
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Centrum för autonoma system, CAS.
    Assavasangthong, Vorapol
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Centrum för autonoma system, CAS.
    Martinelli, Giulio
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Centrum för autonoma system, CAS.
    Gajland, Phillip
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Rodríguez Gálvez, Borja
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teknisk informationsvetenskap.
    Aerial path planning for multi-vehicles2019Ingår i: Proceedings - IEEE 2nd International Conference on Artificial Intelligence and Knowledge Engineering, AIKE 2019, Institute of Electrical and Electronics Engineers (IEEE), 2019, s. 267-272, artikel-id 8791733Konferensbidrag (Refereegranskat)
    Abstract [en]

    Unmanned Aerial Vehicles (UAV) are a potential solution to fast and cost efficient package delivery services. There are two types of UAVs, namely fixed wing (UAV-FW) and rotor wing (UAV-RW), which have their own advantages and drawbacks. In this paper we aim at providing different solutions to a collaborating multi-agent scenario combining both UAVs types. We show the problem can be reduced to the facility location problem (FLP) and propose two local search algorithms to solve it: Tabu search and simulated annealing.

  • 5.
    Austrin, Per
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Kaski, P.
    Kubjas, K.
    Tensor network complexity of multilinear maps2019Ingår i: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2019Konferensbidrag (Refereegranskat)
    Abstract [en]

    We study tensor networks as a model of arithmetic computation for evaluating multilinear maps. These capture any algorithm based on low border rank tensor decompositions, such as O(nω+ϵ) time matrix multiplication, and in addition many other algorithms such as O(nlog n) time discrete Fourier transform and O∗(2n) time for computing the permanent of a matrix. However tensor networks sometimes yield faster algorithms than those that follow from low-rank decompositions. For instance the fastest known O(n(ω+ϵ)t) time algorithms for counting 3t-cliques can be implemented with tensor networks, even though the underlying tensor has border rank n3t for all t ≥ 2. For counting homomorphisms of a general pattern graph P into a host graph on n vertices we obtain an upper bound of O(n(ω+ϵ) bw(P)/2) where bw(P) is the branchwidth of P. This essentially matches the bound for counting cliques, and yields small improvements over previous algorithms for many choices of P. While powerful, the model still has limitations, and we are able to show a number of unconditional lower bounds for various multilinear maps, including: (a) an Ω(nbw(P)) time lower bound for counting homomorphisms from P to an n-vertex graph, matching the upper bound if ω = 2. In particular for P a v-clique this yields an Ω(nd2v/3e) time lower bound for counting v-cliques, and for P a k-uniform v-hyperclique we obtain an Ω(nv) time lower bound for k ≥ 3, ruling out tensor networks as an approach to obtaining non-trivial algorithms for hyperclique counting and the Max-3-CSP problem. (b) an Ω(20.918n) time lower bound for the permanent of an n × n matrix.

  • 6.
    Austrin, Per
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Kaski, Petteri
    Koivisto, Mikko
    Nederlof, Jesper
    Sharper Upper Bounds for Unbalanced Uniquely Decodable Code Pairs2018Ingår i: IEEE Transactions on Information Theory, ISSN 0018-9448, E-ISSN 1557-9654, Vol. 64, nr 2, s. 1368-1373Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Two sets of 0-1 vectors of fixed length form a uniquely decodeable code pair if their Cartesian product is of the same size as their sumset, where the addition is pointwise over integers. For the size of the sumset of such a pair, van Tilborg has given an upper bound in the general case. Urbanke and Li, and later Ordentlich and Shayevitz, have given better bounds in the unbalanced case, that is, when either of the two sets is sufficiently large. Improvements to the latter bounds are presented.

  • 7.
    Balliu, Musard
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Bastys, Iulia
    Chalmers Univ Technol, Dept Comp Sci & Engn, Gothenburg, Sweden..
    Sabelfeld, Andrei
    Chalmers Univ Technol, Dept Comp Sci & Engn, Gothenburg, Sweden..
    Securing IoT Apps2019Ingår i: IEEE Security and Privacy, ISSN 1540-7993, E-ISSN 1558-4046, Vol. 17, nr 5, s. 22-29Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Users increasingly rely on Internet of Things (IoT) apps to manage their digital lives through the overwhelming diversity of IoT services and devices. Are the IoT app platforms doing enough to protect the privacy and security of their users? By securing IoT apps, how can we help users reclaim control over their data?

  • 8.
    Balliu, Musard
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.Manuskript (preprint) (Övrigt vetenskapligt)
    Abstract [en]

    The recent Spectre attacks has demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. In this paper we present such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of three existing countermeasures: constant time, Retpoline, and ARM's Speculative Store Bypass Safe (SSBS).

  • 9.
    Balliu, Musard
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Merro, Massimo
    University of Verona.
    Pasqua, Michele
    University of Verona.
    Securing Cross-App Interactions in IoT Platforms2019Konferensbidrag (Refereegranskat)
    Abstract [en]

    IoT platforms enable users to connect various smart devices and online services via reactive apps running on the cloud. These apps, often developed by third-parties, perform simple computations on data triggered by external information sources and actuate the results of computation on external information sinks. Recent research shows that unintended or malicious interactions between the different (even benign) apps of a user can cause severe security and safety risks. These works leverage program analysis techniques to build tools for unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we are still lacking a semantic framework for understanding interactions between IoT apps. The question of what security policy cross-app interference embodies remains largely unexplored. This paper proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms. The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notions of security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms. Specifically, we present a calculus that models the behavioral semantics of a system of apps executing concurrently, and use it to define desirable semantic policies in the security and safety context of IoT apps. To demonstrate the usefulness of our framework, we define static mechanisms for enforcing crossapp security and safety, and prove them sound with respect to our semantic conditions. Finally, we leverage real-world apps to validate the practical benefits of our policy framework.

  • 10.
    Bansal, Nikhil
    et al.
    Eindhoven Univ Technol, Eindhoven, Netherlands..
    Chalermsook, Parinya
    Aalto Univ, Helsinki, Finland..
    Laekhanukit, Bundit
    Shanghai Univ Finance & Econ, Shanghai, Peoples R China..
    Na Nongkai, Danupon
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Nederlof, Jesper
    Eindhoven Univ Technol, Eindhoven, Netherlands..
    New Tools and Connections for Exponential-Time Approximation2019Ingår i: Algorithmica, ISSN 0178-4617, E-ISSN 1432-0541, Vol. 81, nr 10, s. 3993-4009Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In this paper, we develop new tools and connections for exponential time approximation. In this setting, we are given a problem instance and an integer r > 1, and the goal is to design an approximation algorithm with the fastest possible running time. We give randomized algorithms that establish an approximation ratio of 1. r for maximum independent set in O*(exp((O) over tilde (n/r log(2) r + r log(2) r))) time, 2. r for chromatic number in O*(exp((O) over tilde (n/r log r + r log(2) r))) time, 3. (2 - 1/r) for minimum vertex cover in O*(exp(n/r(Omega(r)))) time, and 4. (k - 1/r) for minimum k-hypergraph vertex cover in O*(exp(n/(kr)(Omega(kr)))) time. (Throughout, (O) over tilde and O* omit polyloglog(r) and factors polynomial in the input size, respectively.) The best known time bounds for all problems were O*(2n/r) (Bourgeois et al. in Discret Appl Math 159(17): 1954-1970, 2011; Cygan et al. in Exponential-time approximation of hard problems, 2008). For maximum independent set and chromatic number, these bounds were complemented by exp(n(1-o(1))/r(1+o(1))) lower bounds (under the Exponential Time Hypothesis (ETH)) (Chalermsook et al. in Foundations of computer science, FOCS, pp. 370-379, 2013; Laekhanukit in Inapproximability of combinatorial problems in subexponential-time. Ph.D. thesis, 2014). Our results show that the naturally-looking O*(2n/r) bounds are not tight for all these problems. The key to these results is a sparsification procedure that reduces a problem to a bounded-degree variant, allowing the use of approximation algorithms for bounded-degree graphs. To obtain the first two results, we introduce a new randomized branching rule. Finally, we show a connection between PCP parameters and exponential-time approximation algorithms. This connection together with our independent set algorithm refute the possibility to overly reduce the size of Chan's PCP (Chan in J. ACM 63(3): 27: 1-27: 32, 2016). It also implies that a (significant) improvement over our result will refute the gap-ETH conjecture (Dinur in Electron Colloq Comput Complex (ECCC) 23: 128, 2016; Manurangsi and Raghavendra in A birthday repetition theorem and complexity of approximating dense CSPs, 2016).

  • 11. Baumann, Christoph
    et al.
    Schwarz, Oliver
    Dam, Mads
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    On the verification of system-level information flow properties for virtualized execution platforms2019Ingår i: Journal of Cryptographic Engineering, ISSN 2190-8508, Vol. 9, nr 3, s. 243-261Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system-level behavior, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible. To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high-level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage. As a case study, we apply this methodology to the verification of information flow security for an industry-scale security-oriented hypervisor on the ARMv8-A platform and report on the complete verification of guest mode security properties in the HOL4 theorem prover.

  • 12.
    Bergenhem, Carl
    et al.
    Qamcom Research and Technology AB.
    Meinke, Karl
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Ström, Fabian
    KTH, Skolan för elektroteknik och datavetenskap (EECS).
    Quantitative Safety Analysis of a Coordinated Emergency Brake Protocol for Vehicle Platoons2018Ingår i: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018 / [ed] Tiziana Margaria, Bernhard Steffen, Springer, 2018, Vol. 11246, s. 386-404Konferensbidrag (Refereegranskat)
    Abstract [en]

    In this paper, we present a general methodology to estimate safety related parameter values of cooperative cyber-physical system-of- systems. As a case study, we consider a vehicle platoon model equipped with a novel distributed protocol for coordinated emergency braking. The estimation methodology is based on learning-based testing; which is an approach to automated requirements testing that combines machine learning with model checking.

    Our methodology takes into account vehicle dynamics, control algorithm design, inter-vehicle communication protocols and environmental factors such as message packet loss rates. Empirical measurements from road testing of vehicle-to-vehicle communication in a platoon are modeled and used in our case study. We demonstrate that the minimum global time headway for our platoon model equipped with the CEBP function scales well with respect to platoon size.

  • 13.
    Berglund, Lasse
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Executive Summaries in Software Model Checking2018Självständigt arbete på avancerad nivå (masterexamen), 20 poäng / 30 hpStudentuppsats (Examensarbete)
    Abstract [sv]

    Model checking, eller modellkontroll, är en välkänd teknik inom programverifikation som används för att verifiera att en modell, ofta av ett program, uppfyller en given specifikation genom att undersöka alla nåbara tillstånd i modellen. Det är en välutvecklad teknik som lider av några brister, en av de viktigaste är det så kallade state space explosion-problemet. Modellerna kan bestå av så många olika tillstånd att \textit{model checking} inte går att använda. I den här rapporten undersöker vi om vi kan tillämpa så kallade procedur-sammanfattningar för att förbättra prestandan av model checking. Procedur-sammanfattningar är representationer av delar av program, till exempel metoder eller funktioner. Vi presenterar en design och implementation av dynamiskt genererade sammanfattningar i form av ett tillägg till Java PathFinder, en virtuell maskin som exekverar Java bytecode som kan utföra model checking genom att backa körningar för att till exempel utforska olika schemaläggningar. Våra procedur-sammanfattningar har i många fall en negativ effekt på körtid, men visar på lovande resultat i vissa fall, i synnerhet när så kallad stateless model checking används. Vi presenterar också resultat kopplat till fall när våra sammanfattningar är applicerbara som kan leda vägen för fortsatt arbete inom området.

  • 14. Bernstein, A.
    et al.
    Nanongkai, Danupon
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Distributed exact weighted all-pairs shortest paths in near-linear time2019Ingår i: Proceeding STOC 2019 Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, Association for Computing Machinery (ACM), 2019, s. 334-342Konferensbidrag (Refereegranskat)
    Abstract [en]

    In the distributed all-pairs shortest paths problem (APSP), every node in the weighted undirected distributed network (the CONGEST model) needs to know the distance from every other node using least number of communication rounds (typically called time complexity). The problem admits (1 + o(1))-approximation Θ (n)time algorithm and a nearly-tight Ω (n) lower bound [Nanongkai, STOC’14; Lenzen and Patt-Shamir PODC’15]. For the exact case, Elkin [STOC’17] presented an O(n5/3 log2/3 n) time bound, which was later improved to Õ(n5/4) in [Huang, Nanongkai, Saranurak FOCS’17]. It was shown that any super-linear lower bound (in n) requires a new technique [Censor-Hillel, Khoury, Paz, DISC’17], but otherwise it remained widely open whether there exists a Õ(n)-time algorithm for the exact case, which would match the best possible approximation algorithm. This paper resolves this question positively: we present a randomized (Las Vegas) Õ(n)-time algorithm, matching the lower bound up to polylogarithmic factors. Like the previous Õ(n5/4) bound, our result works for directed graphs with zero (and even negative) edge weights. In addition to the improved running time, our algorithm works in a more general setting than that required by the previous Õ(n5/4) bound; in our setting (i) the communication is only along edge directions (as opposed to bidirectional), and (ii) edge weights are arbitrary (as opposed to integers in (1, 2, . . ., poly(n))). The previously best algorithm for this more difficult setting required Õ(n3/2) time [Agarwal and Ramachandran, ArXiv’18] (this can be improved to Õ(n4/3) if one allows bidirectional communication). Our algorithm is extremely simple and relies on a new technique called Random Filtered Broadcast. Given any sets of nodes A, B ⊆ V and assuming that every b ∈ B knows all distances from nodes in A, and every node v ∈ V knows all distances from nodes in B, we want every v ∈ V to know DistThroughB(a,v) = minb∈B dist(a,b) + dist(b,v) for every a ∈ A. Previous works typically solve this problem by broadcasting all knowledge of every b ∈ B, causing super-linear edge congestion and time. We show a randomized algorithm that can reduce edge congestions and thus solve this problem in Õ(n) expected time.

  • 15.
    Bhattacharya, Sayan
    et al.
    Univ Warwick, Dept Comp Sci, Coventry, W Midlands, England..
    Chakrabarty, Deeparnab
    Dartmouth Coll, Dept Comp Sci, Hanover, NH 03755 USA..
    Henzinger, Monika
    Univ Vienna, Fac Comp Sci, Vienna, Austria..
    Na Nongkai, Danupon
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Dynamic Algorithms for Graph Coloring2018Ingår i: SODA'18: PROCEEDINGS OF THE TWENTY-NINTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, ASSOC COMPUTING MACHINERY , 2018, s. 1-20Konferensbidrag (Refereegranskat)
    Abstract [en]

    We design fast dynamic algorithms for proper vertex and edge colorings in a graph undergoing edge insertions and deletions. In the static setting, there are simple linear time algorithms for ( δ + 1)vertex coloring and (2 δ 1)edge coloring in a graph with maximum degree δ. It is natural to ask if we can efficiently maintain such colorings in the dynamic setting as well. We get the following three results. (1) We present a randomized algorithm which maintains a ( δ+1)-vertex coloring with O(log δ) expected amortized update time. (2) We present a deterministic algorithm which maintains a (1 + o(1)) δ-vertex coloring with O(polylog δ) amortized update time. (3) We present a simple, deterministic algorithm which maintains a (2 δ)edge coloring with O(log δ) worst-case update time. This improves the recent O( δ)-edge coloring algorithm with Õ ( p δ) worst-case update time [4].

  • 16.
    Bhattacharya, Sayan
    et al.
    University of Warwick, UK.
    Na Nongkai, Danupon
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Saranurak, Thatchaphol
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Nondeterminism and Completeness for Dynamic AlgorithmsManuskript (preprint) (Övrigt vetenskapligt)
  • 17.
    Bilardi, Gianfranco
    et al.
    Univ Padua, Dept Informat Engn, I-35131 Padua, Italy..
    Scquizzato, Michele
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS. Univ Padua, Padua, Italy.
    Silvestri, Francesco
    Univ Padua, Dept Informat Engn, I-35131 Padua, Italy..
    A Lower Bound Technique for Communication in BSP2018Ingår i: ACM TRANSACTIONS ON PARALLEL COMPUTING, ISSN 2329-4949, Vol. 4, nr 3, artikel-id UNSP 14Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Communication is a major factor determining the performance of algorithms on current computing systems; it is therefore valuable to provide tight lower bounds on the communication complexity of computations. This article presents a lower bound technique for the communication complexity in the bulk-synchronous parallel (BSP) model of a given class of DAG computations. The derived bound is expressed in terms of the switching potential of a DAG, that is, the number of permutations that the DAG can realize when viewed as a switching network. The proposed technique yields tight lower bounds for the fast Fourier transform (FFT), and for any sorting and permutation network. A stronger bound is also derived for the periodic balanced sorting network, by applying this technique to suitable subnetworks. Finally, we demonstrate that the switching potential captures communication requirements even in computational models different from BSP, such as the I/O model and the LPRAM.

  • 18. Bittar, A.
    et al.
    Velupillai, Sumithra
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS. Institute of Psychiatry, Psychology and Neuroscience, King's College London, London, United Kingdom.
    Roberts, A.
    Dutta, R.
    Text classification to inform suicide risk assessment in electronic health records2019Ingår i: 17th World Congress on Medical and Health Informatics, MEDINFO 2019, IOS Press, 2019, Vol. 264, s. 40-44Konferensbidrag (Refereegranskat)
    Abstract [en]

    Assessing a patient's risk of an impending suicide attempt has been hampered by limited information about dynamic factors that change rapidly in the days leading up to an attempt. The storage of patient data in electronic health records (EHRs) has facilitated population-level risk assessment studies using machine learning techniques. Until recently, most such work has used only structured EHR data and excluded the unstructured text of clinical notes. In this article, we describe our experiments on suicide risk assessment, modelling the problem as a classification task. Given the wealth of text data in mental health EHRs, we aimed to assess the impact of using this data in distinguishing periods prior to a suicide attempt from those not preceding such an attempt. We compare three different feature sets, one structured and two text-based, and show that inclusion of text features significantly improves classification accuracy in suicide risk assessment. © 2019 International Medical Informatics Association (IMIA) and IOS Press. This article is published online with Open Access by IOS Press and distributed under the terms of the Creative Commons Attribution Non-Commercial License 4.0 (CC BY-NC 4.0).

  • 19.
    Bosk, Daniel
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Rodríguez-Cano, Guillermo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Greschbach, Benjamin
    KTH.
    Buchegger, Sonja
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Applying privacy-enhancing technologies: One alternative future of protests2018Ingår i: Protests in the Information Age: Social Movements, Digital Practices and Surveillance, Taylor & Francis, 2018, s. 73-94Kapitel i bok, del av antologi (Refereegranskat)
    Abstract [en]

    While current technologies, such as online social networks, can facilitate coordination and communication for protest organization, they can also endanger political activists when the control over their data is ceded to third parties. For technology to be useful for activism, it needs to be trustworthy and protect the users’ privacy; only then can it be viewed as a potential improvement over more traditional, offline methods. Here, we discuss a selection of such privacy-enhancing technologies from a Computer Science perspective in an effort to open a dialogue and elicit input from other perspectives.

  • 20.
    Brown-Cohen, Jonah
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Narayanan, Arvind
    Princeton Univ, Princeton, NJ 08544 USA..
    Psomas, Alexandros
    Carnegie Mellon Univ, Pittsburgh, PA 15213 USA..
    Weinberg, S. Matthew
    Princeton Univ, Princeton, NJ 08544 USA..
    Formal Barriers to Longest-Chain Proof-of-Stake Protocols2019Ingår i: ACM EC '19: PROCEEDINGS OF THE 2019 ACM CONFERENCE ON ECONOMICS AND COMPUTATION, ASSOC COMPUTING MACHINERY , 2019, s. 459-473Konferensbidrag (Refereegranskat)
    Abstract [en]

    The security of most existing cryptocurrencies is based on a concept called Proof-of-Work, in which users must solve a computationally hard cryptopuzzle to authorize transactions ("one unit of computation, one vote"). This leads to enormous expenditure on hardware and electricity in order to collect the rewards associated with transaction authorization. Proof-of-Stake is an alternative concept that instead selects users to authorize transactions proportional to their wealth ("one coin, one vote"). Some aspects of the two paradigms are the same. For instance, obtaining voting power in Proof-of-Stake has a monetary cost just as in Proof-of-Work: a coin cannot be freely duplicated any more easily than a unit of computation. However some aspects are fundamentally different. In particular, exactly because Proof-of-Stake is wasteless, there is no inherent resource cost to deviating (commonly referred to as the "Nothing-at-Stake" problem). In contrast to prior work, we focus on incentive-driven deviations (any participant will deviate if doing so yields higher revenue) instead of adversarial corruption (an adversary may take over a significant fraction of the network, but the remaining players follow the protocol). The main results of this paper are several formal barriers to designing incentive-compatible proof-of-stake cryptocurrencies (that don't apply to proof-of-work).

  • 21.
    Brynielsson, Joel
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Message from the EISIC 2017 program chair2017Konferensbidrag (Refereegranskat)
  • 22.
    Brynielsson, Joel
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Message from the program chair2018Ingår i: Proceedings of the 8th European Intelligence and Security Informatics Conference, EISIC 2018, Institute of Electrical and Electronics Engineers Inc. , 2018, artikel-id 8753044Konferensbidrag (Refereegranskat)
    Abstract [en]

    Intelligence and Security Informatics (ISI) is an interdisciplinary field of research that focuses on the development, use, and evaluation of advanced information technologies, including methodologies, models and algorithms, systems, and tools, for local, national, and international security related applications. Over the past decade, the European ISI research community has matured and delivered an impressive array of research results that are both technically innovative and practically relevant.

  • 23. Buss, S.
    et al.
    Itsykson, D.
    Knop, A.
    Sokolov, Dmitry
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Reordering rule makes OBDD proof systems stronger2018Ingår i: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2018, s. 161-1624Konferensbidrag (Refereegranskat)
    Abstract [en]

    Atserias, Kolaitis, and Vardi showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD(∧, weakening), simulates CP∗ (Cutting Planes with unary coefficients). We show that OBDD(∧, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring tautologies have polynomial size proofs in the OBDD(∧, weakening) system. The reordering rule allows changing the variable order for OBDDs. We show that OBDD (∧, weakening, reordering) is strictly stronger than OBDD(∧, weakening). This is proved using the Clique-Coloring tautologies, and by transforming tautologies using coded permutations and orification. We also give CNF formulas which have polynomial size OBDD(∧) proofs but require superpolynomial (actually, quasipolynomial size) resolution proofs, and thus we partially resolve an open question proposed by Groote and Zantema. Applying dag-like and tree-like lifting techniques to the mentioned results, we completely analyze which of the systems among CP∗, OBDD(∧), OBDD(∧, reordering), OBDD(∧, weakening) and OBDD (∧, weakening, reordering) polynomially simulate each other. For dag-like proof systems, some of our separations are quasipolynomial and some are exponential; for tree-like systems, all of our separations are exponential.

  • 24.
    Bälter, Olle
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Medieteknik och interaktionsdesign, MID.
    Riese, Emma
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Enoksson, Fredrik
    KTH, Skolan för industriell teknik och management (ITM), Lärande.
    Hedin, Björn
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Medieteknik och interaktionsdesign, MID.
    Baltatzis, Alexander
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Medieteknik och interaktionsdesign, MID.
    Josefsson, Pernilla
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Medieteknik och interaktionsdesign, MID.
    The Challenge of Identifying the Importance of Drivers and Barriers for Implementation of Technology Enhanced Learning2018Ingår i: The 11th Pan-Hellenic and International Conference: ICT in Education, 2018, s. 283-290Konferensbidrag (Refereegranskat)
    Abstract [en]

    The potential of technology enhanced learning (TEL) can have both pedagogical and administrative benefits. In a previous study, we investigated the drivers and barriers for TEL in higher education using Force Field Analysis (FFA). In this follow-up study, we collected new data through a questionnaire to a group of pedagogical developers and at a presentation at a university internal conference for teachers. A Kruskal Wallis test was carried out to test if the groups filling out questionnaire deviated from each other in their ranking. A comparison was also done to the scores in the previous study. As a result of this triangulation, deviations were found between ratings for seven of the 20 identified forces. While the assessments of strengths in FFA is debated, we argue that each group’s view is an important component to understand the situation, and triangulation of data is helpful in understanding the different views.

  • 25.
    Bälter, Olle
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Medieteknik och interaktionsdesign, MID.
    Riese, Emma
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Viberg, Olga
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Medieteknik och interaktionsdesign, MID.
    Effective Feedback for Faster Learning2019Ingår i: KTH SoTL 2019, Stockholm: KTH Royal Institute of Technology, 2019Konferensbidrag (Refereegranskat)
    Abstract [en]

    Background and purpose The Open Learning Initiative (OLI) at Carnegie Mellon University and Stanford University showed already in 2008 (Lovett, Meyer & Thille) that by using the OLI methodology, teaching and learning time could be reduced with 50% with maintained results. One key in this methodology is to use online questions with answer-depending feedback. In this workshop we will work with you to formulate OLIinspired questions for your course. Work done/work in progress We have previously worked with online quizzes in several forms (Bälter, Enström & Klingenberg, 2013) and analyzed learning data from OLI courses (Bälter, Zimmaro & Thille, 2018). The online learning material where the questions and feedback is embedded is in campus courses used in flipped classroom settings. In 2017 we ran a pilot of preparatory course in programming based on a Stanford course with OLI methodology in the OpenEdX environment. During the fall semester 2018 questions with answer-depending feedback was added to the course material in an online introductory programming course given in Canvas at KTH. Results/observations/lessons learned While a full implementation of the entire OLI methodology requires infrastructure that is not in place at KTH yet (event handler, analytic engine), the actual learning for the students takes place in the interaction with the questions and their feedback and this part can already be implemented in Canvas at KTH. Take-home message Well-formulated questions with forward focused feedback can dramatically speed up both teaching and 1 2 1 1 2 Page 25 KTH SoTL 2019 (A-K) learning. This workshop brings that speed to your course with practical exercises based on your own course.

  • 26.
    Cabrera Arteaga, Javier
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Baudry, Benoit
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Programvaruteknik och datorsystem, SCS.
    Scalable comparison of JavaScript V8 bytecode traces2019Konferensbidrag (Refereegranskat)
    Abstract [en]

    The comparison and alignment of runtime traces are essential, e.g., for semantic analysis or debugging. However, naive sequence alignment algorithms cannot address the needs of the modern web: (i) the bytecode generation process of V8 is not deterministic; (ii) bytecode traces are large.

    We present STRAC, a scalable and extensible tool tailored to compare bytecode traces generated by the V8 JavaScript engine. Given two V8 bytecode traces and a distance function between trace events, STRAC computes and provides the best alignment. The key insight is to split access between memory and disk. STRAC can identify semantically equivalent web pages and is capable of processing huge V8 bytecode traces whose order of magnitude matches today's web like https://2019.splashcon.org, which generates approx. 150k of V8 bytecode instructions.

  • 27. Chalermsook, P.
    et al.
    Goswami, M.
    Kozma, L.
    Mehlhorn, K.
    Saranurak, Thatchaphol
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Multi-finger binary search trees2018Ingår i: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2018, s. 55:1-55:26Konferensbidrag (Refereegranskat)
    Abstract [en]

    We study multi-finger binary search trees (BSTs), a far-reaching extension of the classical BST model, with connections to the well-studied k-server problem. Finger search is a popular technique for speeding up BST operations when a query sequence has locality of reference. BSTs with multiple fingers can exploit more general regularities in the input. In this paper we consider the cost of serving a sequence of queries in an optimal (offline) BST with k fingers, a powerful benchmark against which other algorithms can be measured. We show that the k-finger optimum can be matched by a standard dynamic BST (having a single root-finger) with an O(log k) factor overhead. This result is tight for all k, improving the O(k) factor implicit in earlier work. Furthermore, we describe new online BSTs that match this bound up to a (log k) O (1) factor. Previously only the “one-finger” special case was known to hold for an online BST (Iacono, Langerman, 2016; Cole et al., 2000). Splay trees, assuming their conjectured optimality (Sleator and Tarjan, 1983), would have to match our bounds for all k. Our online algorithms are randomized and combine techniques developed for the k-server problem with a multiplicative-weights scheme for learning tree metrics. To our knowledge, this is the first time when tools developed for the k-server problem are used in BSTs. As an application of our k-finger results, we show that BSTs can efficiently serve queries that are close to some recently accessed item. This is a (restricted) form of the unified property (Iacono, 2001) that was previously not known to hold for any BST algorithm, online or offline.

  • 28.
    Chattopadhyay, Arkadev
    et al.
    Tata Inst Fundamental Res, Mumbai, India..
    Koucky, Michal
    Charles Univ Prague, Prague, Czech Republic..
    Loff, Bruno
    INESC Tec, Porto, Portugal.;Univ Porto, Porto, Portugal..
    Mukhopadhyay, Sagnik
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Simulation Beats Richness: New Data-Structure Lower Bounds2018Ingår i: STOC'18: PROCEEDINGS OF THE 50TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING / [ed] Diakonikolas, I Kempe, D Henzinger, M, ASSOC COMPUTING MACHINERY , 2018, s. 1013-1020Konferensbidrag (Refereegranskat)
    Abstract [en]

    We develop a technique for proving lower bounds in the setting of asymmetric communication, a model that was introduced in the famous works of Miltersen (STOC'94) and Miltersen, Nisan, Safra and Wigderson (STOC'95). At the core of our technique is a novel simulation theorem: Alice gets a p x n matrix x over F-2 and Bob gets a vector y is an element of F-2(n). Alice and Bob need to evaluate f (x center dot y) for a Boolean function f : {0, 1}(p) -> {0, 1}. Our simulation theorems show that a deterministic/randomized communication protocol exists for this problem, with cost C center dot n for Alice and C for Bob, if and only if there exists a deterministic/randomized parity decision tree of cost Theta As applications of this technique, we obtain the following results: (i) The first strong lower-bounds against randomized data-structure schemes for the Vector-Matrix-Vector product problem over F-2. Moreover, our method yields strong lower bounds even when the data-structure scheme has tiny advantage over random guessing. (ii) The first lower bounds against randomized data-structures schemes for two natural Boolean variants of Orthogonal Vector Counting. (iii) We construct an asymmetric communication problem and obtain a deterministic lower-bound for it which is provably better than any lower-bound that may be obtained by the classical Richness Method of Miltersen et al.. This seems to be the first known limitation of the Richness Method in the context of proving deterministic lower bounds.

  • 29.
    Chattopadhyay, Arkadev
    et al.
    Tata Institute of Fundamental Research, Mumbai, Mumbai, India.
    Koucký, Michal
    Charles University, Prague Praha, Czech Republic.
    Loff, Bruno
    INESC-TEC & U. Porto, Porto, Portugal.
    Mukhopadhyay, Sagnik
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Simulation Theorems via Pseudo-random Properties2019Ingår i: Computational Complexity, ISSN 1016-3328, E-ISSN 1420-8954, Vol. 28, nr 4, s. 617-659Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We generalize the deterministic simulation theorem of Raz & McKenzie (Combinatorica 19(3):403–435, 1999), to any gadget which satisfies a certainhitting property. We prove that inner product and gap-Hammingsatisfy this property, and as a corollary, we obtain a deterministic simulationtheorem for these gadgets, where the gadget’s input size is logarithmicin the input size of the outer function. This yields the firstdeterministic simulation theorem with a logarithmic gadget size, answeringan open question posed by Göös, Pitassi & Watson (in: Proceedingsof the 56th FOCS, 2015). Our result also implies the previous results for the indexing gadget, withbetter parameters than was previously known. Moreover, a simulationtheorem with logarithmic-sized gadget implies a quadratic separationin the deterministic communication complexity and the logarithm ofthe 1-partition number, no matter how high the 1-partition number iswith respect to the input size—something which is not achievable by previous results of Göös, Pitassi & Watson (2015).

  • 30.
    Chen, Zimin
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Kommrusch, S. J.
    Tufano, M.
    Pouchet, L.
    Poshyvanyk, D.
    Monperrus, M.
    SEQUENCER: Sequence-to-Sequence Learning for End-to-End Program Repair2019Ingår i: IEEE Transactions on Software Engineering, ISSN 0098-5589, E-ISSN 1939-3520Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    This paper presents a novel end-to-end approach to program repair based on sequence-to-sequence learning. We devise, implement, and evaluate a technique, called SEQUENCER, for fixing bugs based on sequence-to-sequence learning on source code. This approach uses the copy mechanism to overcome the unlimited vocabulary problem that occurs with big code. Our system is data-driven; we train it on 35,578 samples, carefully curated from commits to open-source repositories. We evaluate SEQUENCER on 4,711 independent real bug fixes, as well on the Defects4J benchmark used in program repair research. SEQUENCER is able to perfectly predict the fixed line for 950/4,711 testing samples, and find correct patches for 14 bugs in Defects4J benchmark. SEQUENCER captures a wide range of repair operators without any domain-specific top-down design.

  • 31.
    Daga, Mohit
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Henzinger, M.
    Nanongkai, Danupon
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Saranurak, T.
    Distributed edge connectivity in sublinear time2019Ingår i: Proceeding STOC 2019 Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, Association for Computing Machinery (ACM), 2019, s. 343-354Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present the first sublinear-time algorithm for a distributed message-passing networks to compute its edge connectivity λ exactly in the CONGEST model, as long as there are no parallel edges. Our algorithm takes Õ(n1−1/353D1/353 + n1−1/706) time to compute λ and a cut of cardinality λ with high probability, where n and D are the number of nodes and the diameter of the network, respectively, and Õ hides polylogarithmic factors. This running time is sublinear in n (i.e. Õ(n1−ϵ)) whenever D is. Previous sublinear-time distributed algorithms can solve this problem either (i) exactly only when λ = O(n1/8−ϵ) [Thurimella PODC’95; Pritchard, Thurimella, ACM Trans. Algorithms’11; Nanongkai, Su, DISC’14] or (ii) approximately [Ghaffari, Kuhn, DISC’13; Nanongkai, Su, DISC’14]. To achieve this we develop and combine several new techniques. First, we design the first distributed algorithm that can compute a k-edge connectivity certificate for any k = O(n1−ϵ) in time Õ(nk + D). The previous sublinear-time algorithm can do so only when k = o(n) [Thurimella PODC’95]. In fact, our algorithm can be turned into the first parallel algorithm with polylogarithmic depth and near-linear work. Previous near-linear work algorithms are essentially sequential and previous polylogarithmic-depth algorithms require Ω(mk) work in the worst case (e.g. [Karger, Motwani, STOC’93]). Second, we show that by combining the recent distributed expander decomposition technique of [Chang, Pettie, Zhang, SODA’19] with techniques from the sequential deterministic edge connectivity algorithm of [Kawarabayashi, Thorup, STOC’15], we can decompose the network into a sublinear number of clusters with small average diameter and without any mincut separating a cluster (except the “trivial” ones). This leads to a simplification of the Kawarabayashi-Thorup framework (except that we are randomized while they are deterministic). This might make this framework more useful in other models of computation. Finally, by extending the tree packing technique from [Karger STOC’96], we can find the minimum cut in time proportional to the number of components. As a byproduct of this technique, we obtain an Õ(n)-time algorithm for computing exact minimum cut for weighted graphs.

  • 32. Danglot, Benjamin
    et al.
    Preux, Philippe
    Baudry, Benoit
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Correctness Attraction: A Study of Stability of Software Behavior Under Runtime Perturbation2018Ingår i: PROCEEDINGS 2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), IEEE , 2018, s. 481-481Konferensbidrag (Refereegranskat)
  • 33. Danglot, Benjamin
    et al.
    Preux, Philippe
    Baudry, Benoit
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS. KTH, Skolan för elektroteknik och datavetenskap (EECS), Centra, Centre for Advanced Software Technology Research (CASTOR).
    Correctness attraction: a study of stability of software behavior under runtime perturbation2018Ingår i: Journal of Empirical Software Engineering, ISSN 1382-3256, E-ISSN 1573-7616, Vol. 23, nr 4, s. 2086-2119Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Can the execution of software be perturbed without breaking the correctness of the output? In this paper, we devise a protocol to answer this question from a novel perspective. In an experimental study, we observe that many perturbations do not break the correctness in ten subject programs. We call this phenomenon “correctness attraction”. The uniqueness of this protocol is that it considers a systematic exploration of the perturbation space as well as perfect oracles to determine the correctness of the output. To this extent, our findings on the stability of software under execution perturbations have a level of validity that has never been reported before in the scarce related work. A qualitative manual analysis enables us to set up the first taxonomy ever of the reasons behind correctness attraction.

  • 34.
    Danglot, Benjamin
    et al.
    Inria Lille Nord Europe, Parc Sci Haute Borne 40,Ave Halley,Bat A,Pk Plaza, F-59650 Villeneuve Dascq, France..
    Vera-Perez, Oscar Luis
    Inria Rennes Bretagne Atlantique, Campus Beaulieu,263 Ave Gen Leclerc, F-35042 Rennes, France..
    Baudry, Benoit
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Programvaruteknik och datorsystem, SCS.
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Automatic test improvement with DSpot: a study with ten mature open-source projects2019Ingår i: Journal of Empirical Software Engineering, ISSN 1382-3256, E-ISSN 1573-7616, Vol. 24, nr 4, s. 2603-2635Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In the literature, there is a rather clear segregation between manually written tests by developers and automatically generated ones. In this paper, we explore a third solution: to automatically improve existing test cases written by developers. We present the concept, design and implementation of a system called DSpot, that takes developer-written test cases as input (JUnit tests in Java) and synthesizes improved versions of them as output. Those test improvements are given back to developers as patches or pull requests, that can be directly integrated in the main branch of the test code base. We have evaluated DSpot in a deep, systematic manner over 40 real-world unit test classes from 10 notable and open-source software projects. We have amplified all test methods from those 40 unit test classes. In 26/40 cases, DSpot is able to automatically improve the test under study, by triggering new behaviors and adding new valuable assertions. Next, for ten projects under consideration, we have proposed a test improvement automatically synthesized by DSpot to the lead developers. In total, 13/19 proposed test improvements were accepted by the developers and merged into the main code base. This shows that DSpot is capable of automatically improving unit-tests in real-world, large scale Java software.

  • 35.
    Danglot, Benjamin
    et al.
    INRIA, Lille, France..
    Vera-Perez, Oscar
    INRIA, Rennes, France..
    Yu, Zhongxing
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Zaidman, Andy
    Delft Univ Technol, Delft, Netherlands..
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Baudry, Benoit
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Programvaruteknik och datorsystem, SCS.
    A snowballing literature study on test amplification2019Ingår i: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 157, artikel-id UNSP 110398Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The adoption of agile approaches has put an increased emphasis on testing, resulting in extensive test suites. These suites include a large number of tests, in which developers embed knowledge about meaningful input data and expected properties as oracles. This article surveys works that exploit this knowledge to enhance manually written tests with respect to an engineering goal (e.g., improve coverage or refine fault localization). While these works rely on various techniques and address various goals, we believe they form an emerging and coherent field of research, which we coin "test amplification". We devised a first set of papers from DBLP, searching for all papers containing "test" and "amplification" in their title. We reviewed the 70 papers in this set and selected the 4 papers that fit the definition of test amplification. We use them as the seeds for our snowballing study, and systematically followed the citation graph. This study is the first that draws a comprehensive picture of the different engineering goals proposed in the literature for test amplification. We believe that this survey will help researchers and practitioners entering this new field to understand more quickly and more deeply the intuitions, concepts and techniques used for test amplification.

  • 36.
    de Rezende, Susanna F.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Lower Bounds and Trade-offs in Proof Complexity2019Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    Propositional proof complexity is a field in theoretical computer science that analyses the resources needed to prove statements. In this thesis, we are concerned about the length of proofs and trade-offs between different resources, such as length and space.

    A classical NP-hard problem in computational complexity is that of determining whether a graph has a clique of size k. We show that for all k ≪ n^(1/4) regular resolution requires length n^Ω(k) to establish that an Erdős–Rényi graph with n vertices and appropriately chosen edge density does not contain a k-clique. In particular, this implies an unconditional lower bound on the running time of state-of-the-artalgorithms for finding a maximum clique.

    In terms of trading resources, we prove a length-space trade-off for the cutting planes proof system by first establishing a communication-round trade-off for real communication via a round-aware simulation theorem. The technical contri-bution of this result allows us to obtain a separation between monotone-AC^(i-1) and monotone-NC^i.

    We also obtain a trade-off separation between cutting planes (CP) with unbounded coefficients and cutting planes where coefficients are at most polynomial in thenumber of variables (CP*). We show that there are formulas that have CP proofs in constant space and quadratic length, but any CP* proof requires either polynomial space or exponential length. This is the first example in the literature showing any type of separation between CP and CP*.

    For the Nullstellensatz proof system, we prove a size-degree trade-off via a tight reduction of Nullstellensatz refutations of pebbling formulas to the reversible pebbling game. We show that for any directed acyclic graph G it holds that G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatzrefutation of the pebbling formula over G in size t + 1 and degree s.

    Finally, we introduce the study of cumulative space in proof complexity, a measure that captures the space used throughout the whole proof and not only the peak space usage. We prove cumulative space lower bounds for the resolution proof system, which can be viewed as time-space trade-offs where, when time is bounded, space must be large a significant fraction of the time.

  • 37.
    de Rezende, Susanna F.
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Meir, Or
    Nordström, Jakob
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Robere, Robert
    Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling2019Ingår i: Proceedings of the 34th Annual Computational Complexity Conference (CCC ’19), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2019, Vol. 137, s. 18:1-18:16Konferensbidrag (Refereegranskat)
    Abstract [en]

    We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if an only if there is a Nullstellensatz refutation of the pebbling formula over G in size t + 1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.

  • 38.
    de Rezende, Susanna F.
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Meir, Or
    Nordström, Jakob
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Toniann, Pitassi
    Robere, Robert
    Vinyals, Marc
    Lifting with Simple Gadgets and Applications to Circuit and Proof ComplexityManuskript (preprint) (Övrigt vetenskapligt)
    Abstract [en]

    We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems:

    • We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomialline space if coefficients are restricted to be of polynomial magnitude.
    • We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known.

    An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

  • 39. Deryck, M.
    et al.
    Vennekens, J
    Devriendt, Jo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Marynissen, S.
    Legislation in the Knowledge Base Paradigm: Interactive Decision Enactment for Registration Duties2019Ingår i: Proceedings - 13th IEEE International Conference on Semantic Computing, ICSC 2019, Institute of Electrical and Electronics Engineers Inc. , 2019, s. 174-177Konferensbidrag (Refereegranskat)
    Abstract [en]

    Recently, a prototype for an interactive decision enactment system for notaries was developed. This prototype follows the Knowledge Base Paradigm (KBP): it consists of purely declarative domain knowledge, to which various logical inference methods can be applied. This paper extends that work in two ways. First, we experimentally validate the claim that the KBP leads to highly maintainable software. Second, we extend the number of additional logical inferences, which allows us to address a number of usability concerns. This provides further evidence for the claim that the KBP is indeed a viable method of developing interactive software systems. The resulting interactive decision enactment prototype is a fully generic system, that can be applied to other domains with minimal effort.

  • 40. Downs, J.
    et al.
    Velupillai, Sumithra
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    George, G.
    Holden, R.
    Kikoler, M.
    Dean, H.
    Fernandes, A.
    Dutta, R.
    Detection of Suicidality in Adolescents with Autism Spectrum Disorders: Developing a Natural Language Processing Approach for Use in Electronic Health Records2017Ingår i: Advances in Printing and Media Technology, ISSN 0892-2284, E-ISSN 1942-597X, Vol. 2017, s. 641-649Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Over 15% of young people with autism spectrum disorders (ASD) will contemplate or attempt suicide during adolescence. Yet, there is limited evidence concerning risk factors for suicidality in childhood ASD. Electronic health records (EHRs) can be used to create retrospective clinical cohort data for large samples of children with ASD. However systems to accurately extract suicidality-related concepts need to be developed so that putative models of suicide risk in ASD can be explored. We present a systematic approach to 1) adapt Natural Language Processing (NLP) solutions to screen with high sensitivity for reference to suicidal constructs in a large clinical ASD EHR corpus (230,465 documents), and 2) evaluate within a screened subset of 500 patients, the performance of an NLP classification tool for positive and negated suicidal mentions within clinical text. When evaluated, the NLP classification tool showed high system performance for positive suicidality with precision, recall, and F1 scores all > 0.85 at a document and patient level. The application therefore provides accurate output for epidemiological research into the factors contributing to the onset and recurrence of suicidality, and potential utility within clinical settings as an automated surveillance or risk prediction tool for specialist ASD services.

  • 41.
    Durieux, Thomas
    et al.
    INRIA, Lille, France.;Univ Lille, Lille, France..
    Hamadi, Youssef
    Ecole Polytech, Paris, France..
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Fully Automated HTML and Javascript Rewriting for Constructing a Self-healing Web Proxy2018Ingår i: 2018 29TH IEEE INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING (ISSRE) / [ed] Ghosh, S Natella, R Cukic, B Poston, R Laranjeiro, N, IEEE , 2018, s. 1-12Konferensbidrag (Refereegranskat)
    Abstract [en]

    Over the last few years, the complexity of web applications has increased to provide more dynamic web applications to users. The drawback of this complexity is the growing number of errors in the front-end applications. In this paper, we present BikiniProxy, a novel technique to provide self-healing for the web. BikiniProxy is designed as an HTTP proxy that uses five self-healing strategies to rewrite the buggy HTML and Javascript code. We evaluate BikiniProxy with a new benchmark of 555 reproducible Javascript errors of which 31.76% can be automatically self-healed.

  • 42.
    Durieux, Thomas
    et al.
    Univ Lille, Lille, France.;INRIA, Le Chesnay, France..
    Hamadi, Youssef
    Ecole Polytech, Palaiseau, France..
    Yu, Zhongxing
    Univ Lille, Lille, France.;INRIA, Le Chesnay, France..
    Baudry, Benoit
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Programvaruteknik och datorsystem, SCS.
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Exhaustive Exploration of the Failure-oblivious Computing Search Space2018Ingår i: 2018 IEEE 11TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), IEEE Press, 2018, s. 139-149Konferensbidrag (Refereegranskat)
    Abstract [en]

    High-availability of software systems requires automated handling of crashes in presence of errors. Failure-oblivious computing is one technique that aims to achieve high availability. We note that failure-obliviousness has not been studied in depth yet, and there is very few study that helps understand why failure-oblivious techniques work. In order to make failure-oblivious computing to have an impact in practice, we need to deeply understand failure-oblivious behaviors in software. In this paper, we study, design and perform an experiment that analyzes the size and the diversity of the failure-oblivious behaviors. Our experiment consists of exhaustively computing the search space of 16 field failures of large-scale open-source Java software. The outcome of this experiment is a much better understanding of what really happens when failure-oblivious computing is used, and this opens new promising research directions.

  • 43.
    Elffers, Jan
    et al.
    KTH.
    Cru, Jesús Giráldez
    KTH.
    Gocht, Stephan
    KTH.
    Nordström, Jakob
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Simon, L.
    Seeking practical CDCL insights from theoretical SAT benchmarks2018Ingår i: IJCAI International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence , 2018, s. 1300-1308Konferensbidrag (Refereegranskat)
    Abstract [en]

    Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

  • 44.
    Elffers, Jan
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Giráldez-Cru, Jakob
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Nordström, Jakob
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Vinyals, Marc
    Tata Institute of Fundamental Research, Mumbai, India.
    Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers2018Ingår i: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Springer, 2018, Vol. 10929, s. 75-93Konferensbidrag (Refereegranskat)
    Abstract [en]

    We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also real-valued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.

  • 45. Fano, E.
    et al.
    Karlgren, Jussi
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Nivre, J.
    Uppsala University and Gavagai at CLEF Erisk: Comparing word embedding models2019Ingår i: CEUR Workshop Proceedings, CEUR-WS , 2019, Vol. 2380Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper describes an experiment to evaluate the performance of three different types of semantic vectors or word embeddings-random indexing, GloVe, and ELMo-and two different classification architectures-linear regression and multi-layer perceptrons-for the specific task of identifying authors with eating disorders from writings they publish on a discussion forum. The task requires the classifier to process texts written by the authors in the sequence they were published, and to identify authors likely to be at risk of suffering from eating disorders as early as possible. The data are part of the eRISK evaluation task of CLEF 2019 and evaluated according to the eRISK metrics. Contrary to our expectations, we did not observe a clear-cut advantage using the recently popular contextualized ELMo vectors over the commonly used and much more light-weight GloVe vectors, or the more handily learnable random indexing vectors.

  • 46. Felderer, M.
    et al.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Huisman, M.
    Lisper, B.
    Schlick, R.
    Formal methods in industrial practice - Bridging the gap (track summary)2018Ingår i: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Springer, 2018, Vol. 11247, s. 77-81Konferensbidrag (Refereegranskat)
    Abstract [en]

    Already for many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief, and many individual success stories, no real change in industrial software development seems to happen. In fact, the software industry is moving fast forward itself, and the gap between what formal methods can achieve, and the daily software development practice does not seem to get smaller (and might even be growing).

  • 47.
    Fernandez, Daniel Mendez
    et al.
    Tech Univ Munich, Munich, Germany..
    Monperrus, Martin
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Feldt, Robert
    Chalmers Univ Technol, Gothenburg, Sweden.;Blekinge Inst Technol, Karlskrona, Sweden..
    Zimmermann, Thomas
    Microsoft Res, Redmond, WA 98052 USA..
    The open science initiative of the Empirical Software Engineering journal2019Ingår i: Journal of Empirical Software Engineering, ISSN 1382-3256, E-ISSN 1573-7616, Vol. 24, nr 3, s. 1057-1060Artikel i tidskrift (Övrigt vetenskapligt)
  • 48. Frezza, S.
    et al.
    Daniels, M.
    Pears, Arnold Neville
    KTH, Skolan för industriell teknik och management (ITM), Lärande.
    Cajander, Å.
    Kann, Viggo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Kapoor, A.
    McDermott, R.
    Peters, A. -K
    Sabin, M.
    Wallace, C.
    Modelling competencies for computing education beyond 2020: A research based approach to defining competencies in the computing disciplines2018Ingår i: Annual Conference on Innovation and Technology in Computer Science Education, ITiCSE, Association for Computing Machinery , 2018, s. 148-174Konferensbidrag (Refereegranskat)
    Abstract [en]

    How might the content and outcomes of tertiary education programmes be described and analysed in order to understand how they are structured and function? To address this question we develop a framework for modelling graduate competencies linked to tertiary degree programmes in the computing disciplines. While the focus of our work is computing the framework is applicable to education more broadly. The work presented here draws upon the pioneering curricular document for information technology (IT2017), curricular competency frameworks, other related documents such as the software engineering competency model (SWECOM), the Skills Framework for the Information Age (SFIA), current research in competency models, and elicitation workshop results from recent computing conferences. The aim is to inform the ongoing Computing Curricula (CC2020) project, an endeavour supported by the Association for Computing Machinery (ACM) and the IEEE Computer Society. We develop the Competency Learning Framework (CoLeaF), providing an internationally relevant tool for describing competencies. We argue that this competency based approach is well suited for constructing learning environments and assists degree programme architects in dealing with the challenge of developing, describing and including competencies relevant to computer and IT professionals. In this paper we demonstrate how the CoLeaF competency framework can be applied in practice, and though a series of case studies demonstrate its effectiveness and analytical power as a tool for describing and comparing degree programmes in the international higher education landscape.

  • 49.
    Garg, Ankit
    et al.
    Microsoft Res, Redmond, WA 98052 USA..
    Goos, Mika
    Harvard Univ, Cambridge, MA 02138 USA..
    Kamath, Pritish
    MIT, Cambridge, MA 02139 USA..
    Sokolov, Dmitry
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Monotone Circuit Lower Bounds from Resolution2018Ingår i: STOC'18: PROCEEDINGS OF THE 50TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING / [ed] Diakonikolas, I Kempe, D Henzinger, M, ASSOC COMPUTING MACHINERY , 2018, s. 902-911Konferensbidrag (Refereegranskat)
    Abstract [en]

    For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols-or, equivalently, that a monotone function associated with F has large monotone circuit complexity. Our result extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.

  • 50.
    Gedin, Emanuel
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Hardness of showing hardness of the minimum circuit size problem2018Självständigt arbete på avancerad nivå (masterexamen), 20 poäng / 30 hpStudentuppsats (Examensarbete)
    Abstract [sv]

    Problemet att finna den minsta storleken på en krets som beräknar en given boolesk funktion, ofta kallat minimum circuit size problem (MCSP), har studerats i många år men det är fortfarande okänt om problemet är NP-svårt eller inte. Med detta i åtankte studerar vi egenskaper hos potentiella reduktioner till det här problemet. Vi fokuserar på naturliga lokala reduktioner som är vanliga i många bevis av NP-svårighet. Vi presenterar en method som visar att det finns en algorithm för att lösa varje problem som har en lokal naturlig reduktion till MCSP. Vi visar att om beslutsproblemet att skilja satisfierbara instanser av 3-SAT från de där som mest 7/8 + o(1) av klausulerna går att satisfiera har en reduktion till MCSP där en godtycklig bit av utdata kan beräknas i O(n1 - ε) tid för varje ε > 0 då kan k-SAT lösas av en krets med djup 3 och storlek 2o(n).

123 1 - 50 av 134
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf