kth.sePublications
Change search
Refine search result
1234567 151 - 200 of 518
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Jacobs, Bart
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Piessens, Frank
    Security Monitor Inlining for Multithreaded Java2009In: ECOOP 2009: OBJECT-ORIENTED PROGRAMMING / [ed] Drossopoulou S, 2009, Vol. 5653, p. 546-569Conference paper (Refereed)
    Abstract [en]

    Program monitoring is a well-established and efficient approach to security policy enforcement. An implementation of program monitoring that is particularly appealing for application-level policy enforcement is monitor inlining: the application is rewritten to push monitoring and policy enforcement code into the application itself. The intention is that the inserted code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). For sequential Java-like languages, provably correct inlining algorithms have been proposed, but for the multithreaded setting, this is still an open problem. We show that no inliner for multithreaded Java can be both secure and transparent. It is however possible to identify a broad class of policies for which all three correctness criteria can be obtained. We propose an inliner that is correct for such policies, implement it for Java, and show that it is practical by reporting on some benchmarks.

  • 152.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Le Guernic, Gurvan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    TreeDroid: A tree automaton based approach to enforcing data processing policies2012In: CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security, ACM , 2012, p. 894-905Conference paper (Refereed)
    Abstract [en]

    Current approaches to security policy monitoring are based on linear control flow constraints such as runQuery may be evaluated only after sanitize. However, realistic security policies must be able to conveniently capture data flow constraints as well. An example is a policy stating that arguments to the function runQuery must be either constants, outputs of a function sanitize, or concatenations of any such values. We present a novel approach to security policy monitoring that uses tree automata to capture constraints on the way data is processed along an execution. We present a λ-calculus based model of the framework, investigate some of the models meta-properties, and show how it can be implemented using labels corresponding to automaton states to reflect the computational histories of each data item. We show how a standard denotational semantics induces the expected monitoring regime on a simple "while" language. Finally we implement the framework for the Dalvik VM using TaintDroid as the underlying data flow tracking mechanism, and evaluate its functionality and performance on five case studies.

  • 153.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Lundblad, Andreas
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    A proof carrying code framework for inlined reference monitors in java bytecode2010Report (Refereed)
    Abstract [en]

    We propose a light-weight approach for certification of monitor inlining for sequential Java bytecode using proof-carrying code. The goal is to enable the use of monitoring for quality assurance at development time, while minimizing the need for post-shipping code rewrites as well as changes to the end-host TCB. Standard automaton-based security policies express constraints on allowed API call/return sequences. Proofs are represented as JML-style program annotations. This is adequate in our case as all proofs generated in our framework are recognized in time polynomial in the size of the program. Policy adherence is proved by comparing the transitions of an inlined monitor with those of a trusted "ghost" monitor represented using JML-style annotations. At time of receiving a program with proof annotations, it is sufficient for the receiver to plug in its own trusted ghost monitor and check the resulting verification conditions, to verify that inlining has been performed correctly, of the correct policy. We have proved correctness of the approach at the Java bytecode level and formalized the proof of soundness in Coq. An implementation, including an application loader running on a mobile device, is available, and we conclude by giving benchmarks for two sample applications.

  • 154.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Decentralized Adaptive Power Control for Process NetworksManuscript (preprint) (Other academic)
    Abstract [en]

    Mobility and location transparency of distributed objects enable efficient resource allocation in networks, and can be effectively realized at the language level using location independent routing. However, the benefits of mobility are restricted by the available resources, e.g., in the form of processing nodes, which may be too few or too many to suit an application. To continually meet an application developer's requirements on computational task throughput, and an infrastructure provider's requirements on energy usage, the network itself must be able to adapt. In this paper, we consider fault-free networks of nodes connected point-to-point by asynchronous message passing channels, and propose a protocol for shutdown of nodes that preserves the integrity of distributed objects. This protocol enables decentralized power control, where nodes are turned on and off in response to computational requirements. We analyze the protocol both by verifying a restricted version in the model checker Spin, and by formulating a transition system model and proving properties by induction in that model for networks of arbitrary size. We define a protocol extension that, while using only a node's neighborhood-local information, is sufficient to ensure networks remain connected after node shutdown, and outline more complex, general local criteria. Finally, we discuss heuristics for node-local decision making on initiating a shutdown process, to meet adaptability requirements.

  • 155.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Efficient and Fully Abstract Routing of Futures in Object Network OverlaysManuscript (preprint) (Other academic)
    Abstract [en]

    In distributed object systems, it is desirable to enable migration of objects between locations, e.g., in order to support efficient resource allocation. Existing approaches build complex routing infrastructures to handle object-to-object communication, typically on top of IP, using, e.g., message forwarding chains or centralized object location servers. These solutions are costly and problematic in terms of efficiency, overhead, and correctness. We show how location independent routing can be used to implement object overlays with complex messaging behavior in a sound, fully abstract, and efficient way, on top of an abstract network of processing nodes connected point-to-point by asynchronous channels. We consider a distributed object language with futures, essentially lazy return values. Futures are challenging in this context due to the strong global consistency requirements they impose. The key conclusion is that execution in a decentralized, asynchronous network can preserve the standard, network-oblivious behavior of objects with futures, in the sense of contextual equivalence. To the best of our knowledge, this is the first such result in the literature. We also believe the proposed execution model may be of interest in its own right in the context of large-scale distributed computing.

    Download full text (pdf)
    fulltext
  • 156.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Efficient and fully abstract routing of futures in object network overlays2013In: AGERE! 2013 - Proceedings of the 2013 ACM Workshop on Programming Based on Actors, Agents, and Decentralized Control, Association for Computing Machinery (ACM), 2013, p. 49-59Conference paper (Refereed)
    Abstract [en]

    In distributed object systems, it is desirable to enable migration of objects between locations, e.g., in order to support efficient resource allocation. Existing approaches build complex routing infrastructures to handle object-to-object communication, typically on top of IP, using, e.g., message forwarding chains or centralized object location servers. These solutions are costly and problematic in terms of efficiency, overhead, and correctness. We show how location independent routing can be used to implement object overlays with complex messaging behavior in a sound, fully abstract, and efficient way, on top of an abstract network of processing nodes connected point-to-point by asynchronous channels. We consider a distributed object language with futures, essentially lazy return values. Futures are challenging in this context due to the global consistency requirements they impose. The key conclusion is that execution in a decentralized, asynchronous network can preserve the standard, network-oblivious behavior of objects with futures, in the sense of contextual equivalence. To the best of our knowledge, this is the first such result in the literature. We also believe the proposed execution model may be of interest in its own right in the context of large-scale distributed computing.

  • 157.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Location independent routing in process network overlays2014In: Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, IEEE Computer Society, 2014, p. 715-724Conference paper (Refereed)
    Abstract [en]

    In distributed computing, location transparency - the decoupling of objects, tasks, and virtual machines from their physical location - is desirable in that it can simplify application development and management, and enable load balancing and efficient resource allocation. Many existing systems for location transparency are built on top of TCP/IP. We argue that addressing mobile objects in terms of the host where they temporarily reside may not be the best design decision. When objects can migrate, it becomes necessary to use a dedicated routing infrastructure to deliver inter-object messages, such as location servers or forwarding chains. This incurs high costs in terms of complexity, overhead, and latency. In this paper, we defer object overlay routing to an underlying networking layer, by assuming a location independent routing scheme in place of TCP/IP. In this scheme, messages are directed to destinations determined by flat identifiers instead of IP addresses. Consequently, messages are delivered directly to a recipient object, instead of a possibly out-of-date location. We explore the scheme in the context of a small object-based language with asynchronous message passing, in the style of core Erlang. We provide a standard, network-oblivious operational semantics of this language, and a network-aware semantics which takes many aspects of distribution and message routing into account. The main result is that execution of a program on top of an abstract network of processing nodes connected by asynchronous point-to-point communication channels preserves the network-oblivious behavior in a sound and fully abstract way, in the sense of contextual equivalence. This is a novel and strong result for such a low-level model. Previous work has addressed distributed implementations only in terms of fully connected TCP underlays. But in this setting, contextual equivalence is typically too strong, due to the need for locking to resolve preemption arising from object mobility.

  • 158.
    Dam, Mads
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Location Independent Routing in Process Network Overlays2014In: Service Oriented Computing and Applications, ISSN 1863-2386, E-ISSN 1863-2394, no Special Issue, p. 1-25Article in journal (Other academic)
    Abstract [en]

    In distributed computing, location transparency - the decoupling of objects, tasks, and virtual machines from their physical location - is desirable in that it can simplify application development and management, and enable load balancing and efficient resource allocation. Many existing systems for location transparency are built on top of TCP/IP. We argue that addressing mobile objects in terms of the host where they temporarily reside may not be the best design decision. When objects can migrate, it becomes necessary to use a dedicated routing infrastructure to deliver inter-object messages, such as location servers or forwarding chains. This incurs high costs in terms of complexity, overhead, and latency. In this paper, we defer object overlay routing to an underlying networking layer, by assuming a location independent routing scheme in place of TCP/IP. In this scheme, messages are directed to destinations determined by flat identifiers instead of IP addresses. Consequently, messages are delivered directly to a recipient object, instead of a possibly out-of-date location. We explore the scheme in the context of a small object-based language with asynchronous message passing, in the style of core Erlang. We provide a standard, network-oblivious operational semantics of this language, and a network-aware semantics which takes many aspects of distribution and message routing into account. The main result is that execution of a program on top of an abstract network of processing nodes connected by asynchronous point-to-point communication channels preserves the network-oblivious behavior in a sound and fully abstract way, in the sense of contextual equivalence. This is a novel and strong result for such a low-level model. Previous work has addressed distributed implementations only in terms of fully connected TCP underlays. But in this setting, contextual equivalence is typically too strong, due to the need for locking to resolve preemption arising from object mobility.

  • 159.
    Datta, Anwitaman
    et al.
    NTU Singapore.
    Buchegger, Sonja
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Vu, Le Hung
    EPFL.
    Rzadca, Krzysztof
    Warsaw University.
    Strufe, Thorsten
    TU Darmstadt.
    Decentralized Online Social Networks2010In: Handbook of Social Network Technologies and Applications / [ed] Borko Furht, Springer, 2010, p. 349-378Chapter in book (Refereed)
    Abstract [en]

    Current Online social networks (OSN) are web services run on logically centralized infrastructure. Large OSN sites use content distribution networks and thus distribute some of the load by caching for performance reasons, nevertheless there is a central repository for user and application data. This centralized nature of OSNs has several drawbacks including scalability, privacy, dependence on a provider, need for being online for every transaction, and a lack of locality. There have thus been several efforts toward decentralizing OSNs while retaining the functionalities offered by centralized OSNs. A decentralized online social network (DOSN) is a distributed system for social networking with no or limited dependency on any dedicated central infrastructure. In this chapter we explore the various motivations of a decentralized approach to online social networking, discuss several concrete proposals and types of DOSN as well as challenges and opportunities associated with decentralization.

  • 160.
    de Carvalho Gomes, Pedro
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Automatic Extraction of Program Models for Formal Software Verification2015Doctoral thesis, monograph (Other academic)
    Abstract [en]

    In this thesis we present a study of the generation of abstract program models from programs in real-world programming languages that are employed in the formal verification of software. The thesis is divided into three parts, which cover distinct types of software systems, programming languages, verification scenarios, program models and properties.The first part presents an algorithm for the extraction of control flow graphs from sequential Java bytecode programs. The graphs are tailored for a compositional technique for the verification of temporal control flow safety properties. We prove that the extracted models soundly over-approximate the program behaviour w.r.t. sequences of method invocations and exceptions. Therefore, the properties that are established with the compositional technique over the control flow graphs also hold for the programs. We implement the algorithm as ConFlEx, and evaluate the tool on a number of test cases.The second part presents a technique to generate program models from incomplete software systems, i.e., programs where the implementation of at least one of the components is not available. We first define a framework to represent incomplete Java bytecode programs, and extend the algorithm presented in the first part to handle missing code. Then, we introduce refinement rules, i.e., conditions for instantiating the missing code, and prove that the rules preserve properties established over control flow graphs extracted from incomplete programs. We have extended ConFlEx to support the new definitions, and re-evaluate the tool, now over test cases of incomplete programs.The third part addresses the verification of multithreaded programs. We present a technique to prove the following property of synchronization with condition variables: "If every thread synchronizing under the same condition variables eventually enters its synchronization block, then every thread will eventually exit the synchronization". To support the verification, we first propose SyncTask, a simple intermediate language for specifying synchronized parallel computations. Then, we propose an annotation language for Java programs to assist the automatic extraction of SyncTask programs, and show that, for correctly annotated programs, the above-mentioned property holds if and only if the corresponding SyncTask program terminates. We reduce the termination problem into a reachability problem on Coloured Petri Nets. We define an algorithm to extract nets from SyncTask programs, and show that a program terminates if and only if its corresponding net always reaches a particular set of dead configurations. The extraction of SyncTask programs and their translation into Petri nets is implemented as the STaVe tool. We evaluate the technique by feeding annotated Java programs to STaVe, then verifying the extracted nets with a standard Coloured Petri Net analysis tool

    Download full text (pdf)
    Thesis
  • 161.
    de Carvalho Gomes, Pedro
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sound Modular Extraction of Control Flow Graphs from Java Bytecode2012Licentiate thesis, monograph (Other academic)
    Abstract [en]

    Control flow graphs (CFGs) are abstract program models that preserve the control flow information. They have been widely utilized for many static analyses in the past decades. Unfortunately, previous studies about the CFG construction from modern languages, such as Java, have either neglected advanced features that influence the control flow, or do not provide a correctness argument. This is a bearable issue for some program analyses, but not for formal methods, where the soundness of CFGs is a mandatory condition for the verification of safety-critical properties. Moreover, when developing open systems, i.e., systems in which at least one component is missing, one may want to extract CFGs to verify the available components. Soundness is even harder to achieve in this scenario, because of the unknown inter-dependencies involving missing components. In this work we present two variants of a CFG extraction algorithm from Java bytecode considering precise exceptional flow, which are sound w.r.t to the JVM behavior. The first algorithm extracts CFGs from fully-provided (closed) programs only. It proceeds in two phases. Initially the Java bytecode is translated into a stack-less intermediate representation named BIR, which provides explicit representation of exceptions, and is more compact than the original bytecode. Next, we define the transformation from BIR to CFGs, which, among other features, considers the propagation of uncaught exceptions within method calls. We then establish its correctness: the behavior of the extracted CFGs is shown to be a sound over-approximation of the behavior of the original programs. Thus, temporal safety properties that hold for the CFGs also hold for the program. We prove this by suitably combining the properties of the two transformations with those of a previous idealized CFG extraction algorithm, whose correctness has been proven directly. The second variant of the algorithm is defined for open systems. We generalize the extraction algorithm for closed systems for a modular set-up, and resolve inter-dependencies involving missing components by using user-provided interfaces. We establish its correctness by defining a refinement relation between open systems, which constrains the instantiation of missing components. We prove that if the relation holds, then the CFGs extracted from the components of the original open system are sound over-approximations of the CFGs for the same components in the refined system. Thus, temporal safety properties that hold for an open system also hold for closed systems that refine it. We have implemented both algorithms as the ConFlEx tool. It uses Sawja, an external library for the static analysis of Java bytecode, to transform bytecode into BIR, and to resolve virtual method calls. We have extended Sawja to support open systems, and improved its exception type analysis. Experimental results have shown that the algorithm for closed systems generates more precise CFGs than the modular algorithm. This was expected, due to the heavy over-approximations the latter has to perform to be sound. Also, both algorithms are linear in the number of bytecode instructions. Therefore, ConFlEx is efficient for the extraction of CFGs from either open, or closed Java bytecode programs.

    Download full text (pdf)
    lic_thesis-pedro_gomes
  • 162.
    de Carvalho Gomes, Pedro
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Verification of symmetric models using semiautomatic abstractions2010Independent thesis Advanced level (degree of Master (Two Years)), 80 credits / 120 HE creditsStudent thesis
  • 163.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Campos, Sérgio
    Universidade Federal de Minas Gerais.
    Borges Vieira, Alex
    Universidade Federal de Juiz de Fora.
    Verification of P2P live streaming systems using symmetry-based semiautomatic abstractions2012In: Proceedings of the 2012 International Conference on High Performance Computing and Simulation, HPCS 2012, IEEE , 2012, p. 343-349Conference paper (Refereed)
    Abstract [en]

    P2P systems are one of the most efficient data transport technologies in use today. Particularly, P2P live streaming systems have been growing in popularity recently. However, analyzing such systems is difficult. Developers are not able to realize a complete test due the due to system size and complex dynamic behavior. This may lead us to develop protocols with errors, unfair or even with low performance. One way of performing such an analysis is using formal methods. Model Checking is one such method that can be used for the formal verification of P2P systems. However it suffers from the combinatory explosion of states. The problem can be minimized with techniques such as abstraction and symmetry reduction. This work combines both techniques to produce reduced models that can be verified in feasible time. We present a methodology to generate abstract models of reactive systems semi-automatically, based on the model's symmetry. It defines modeling premises to make the abstraction procedure semiautomatic, i.e., without modification of the model. Moreover, it presents abstraction patterns based on the system symmetry and shows which properties are consistent with each pattern. The reductions obtained by the methodology were significant. In our test case of a P2P network, it has enabled the verification of liveness properties over the abstract models which did not finish with the original model after more than two weeks of intensive computation. Our results indicate that the use of model checking for the verification of P2P systems is feasible, and that our modeling methodology can increase the efficiency of the verification algorithms enough to enable the analysis of real complex P2P live streaming systems.

  • 164.
    De Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, M.
    Specification and verification of synchronization with condition variables2017In: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Springer, 2017, Vol. 694, p. 3-19Conference paper (Refereed)
    Abstract [en]

    In this paper we propose a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviors. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behavior of the program, which is typically significantly smaller than its overall behavior. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behavior of the underlying program. We prove that every Java program annotated according to the scheme (and satisfying the assumption) has a correct synchronization iff its corresponding SyncTask program terminates. We show how to transform the verification of termination into a standard reachability problem over Colored Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STaVe tool. We evaluate the proposed framework on a number of test cases as a proof-of-concept.

  • 165.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Algorithmic Verification of Synchronization with Condition Variables2015Report (Other academic)
    Abstract [en]

    Condition variables are a common synchronization mechanism present in many programming languages. Still, due to the combinatorial complexity of the behaviours the mechanism induces, it has not been addressed sufficiently with formal techniques. In this paper we propose a fully automated technique to prove the correct synchronization of concurrent programs synchronizing via condition variables, where under correctness we mean the liveness property: "If for every set of condition variables, every thread synchronizing under the variables of the set eventually enters its synchronization block, then every thread will eventually exit the synchronization".First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. Next, we model the constructs of the language as Petri Net components, and define rules to extract and compose nets from a SyncTask program. We show that a SyncTask program terminates if and only if the corresponding Petri Net always reaches a particular final marking. We thus transform the verification of termination into a reachability problem on the net, which can be solved efficiently by existing Petri Net analysis tools. Further, to relieve the programmer from the burden of having to provide specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behaviour of the underlying program. We show that, for the Java programs that can be annotated according to the scheme, the above-mentioned liveness property holds if and only if the corresponding SyncTask program terminates. Both the SyncTask program extraction and the generation of Petri Nets are implemented in the STaVe tool. We evaluate the proposed verification framework on a number of test cases

    Download full text (pdf)
    Report
  • 166.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Picoco, Attilio
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. Polytechnic University of Turin.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs2014In: Fundamental Approaches to Software Engineering: 17th International Conference, FASE 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings / [ed] Stefania Gnesi and Arend Rensink, Springer Berlin/Heidelberg, 2014, p. 215-229Conference paper (Refereed)
    Abstract [en]

    The modular analysis of control flow of incompleteJava bytecode programs is challenging, mainly because of the complex semantics of the language,and the unknown inter-dependencies between the available and unavailable components.In this paper we describe a technique for incremental, modular extraction ofcontrol flow graphs that are provably sound w.r.t.~sequences of method invocations and exceptions.The extracted models are suitable for various program analyses,in particular model-checking of temporal control flow safety properties.Soundness comes at the price of over-approximation,potentially giving rise to false positives reports during verification.Still, our technique supports incremental refinement of the already extracted models,as more components code becomes available.The extraction has been implemented as the ConFlex tool, and test-cases show its utility and efficiency.

  • 167.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Picoco, Attilio
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sound Extraction of Control-Flow Graphs from open Java Bytecode Systems2012Report (Other academic)
    Abstract [en]

    Formal verification techniques have been widely deployed as means to ensure the quality of software products. Unfortunately, they suffer with the combinatorial explosion of the state space. That is, programs have a large number of states, sometimes infinite. A common approach to alleviate the problem is to perform the verification over abstract models from the program. Control-flow graphs (CFG) are one of the most common models, and have been widely studied in the past decades. Unfortunately, previous works over modern programming languages, such as Java, have either neglected features that influence the control-flow, or do not provide a correctness argument about the CFG construction. This is an unbearable issue for formal verification, where soundness of CFGs is a mandatory condition for the verification of safety-critical properties. Moreover, one may want to extract CFGs from the available components of an open system. I.e., a system whose at least one of the components is missing. Soundness is even harder to achieve in this scenario, because of the unknown inter-dependences between software components.

    In the current work we present a framework to extract control-flow graphs from open Java Bytecode systems in a modular fashion. Our strategy requires the user to provide interfaces for the missing components. First, we present a formal definition of open Java bytecode systems. Next, we generalize a previous algorithm that performs the extraction of CFGs for closed programs to a modular set-up. The algorithm uses the user-provided interfaces to resolve inter-dependences involving missing components. Eventually the missing components will arrive, and the open system will become closed, and can execute. However, the arrival of a component may affect the soundness of CFGs which have been extracted previously. Thus, we define a refinement relation, which is a set of constraints upon the arrival of components, and prove that the relation guarantees the soundness of CFGs extracted with the modular algorithm. Therefore, the control-flow safety properties verified over the original CFGs still hold in the refined model.

    We implemented the modular extraction framework in the ConFlEx tool. Also, we have implemented the reusage from previous extractions, to enable the incremental extraction of a newly arrived component. Our technique performs substantial over-approximations to achieve soundness. Despite this, our test cases show that ConFlEx is efficient. Also, the extraction of the CFGs gets considerable speed-up by reusing results from previous analyses.

    Download full text (pdf)
    fulltext
  • 168.
    De Oliveira Oliveira, Mateus
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Canonizable partial order generators2012In: Language and Automata Theory and Applications, Springer Berlin/Heidelberg, 2012, Vol. 7183 LNCS, p. 445-457Conference paper (Refereed)
    Abstract [en]

    In a previous work we introduced slice graphs as a way to specify both infinite languages of directed acyclic graphs (DAGs) and infinite languages of partial orders. Therein we focused on the study of Hasse diagram generators, i.e., slice graphs that generate only transitive reduced DAGs. In the present work we show that any slice graph can be transitive reduced into a Hasse diagram generator representing the same set of partial orders. This result allow us to establish unknown connections between the true concurrent behavior of bounded p/t-nets and traditional approaches for representing infinite families of partial orders, such as Mazurkiewicz trace languages and Message Sequence Chart (MSC) languages. Going further, we identify the family of weakly saturated slice graphs. The class of partial order languages which can be represented by weakly saturated slice graphs is closed under union, intersection and a suitable notion of complementation (bounded cut-width complementation). The partial order languages in this class also admit canonical representatives in terms of Hasse diagram generators, and have decidable inclusion and emptiness of intersection. Our transitive reduction algorithm plays a fundamental role in these decidability results.

  • 169.
    de Oliveira Oliveira, Mateus
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Combinatorial Slice Theory2013Doctoral thesis, monograph (Other academic)
    Abstract [en]

    Slices are digraphs that can be composed together to form larger digraphs.In this thesis we introduce the foundations of a theory whose aim is to provide ways of defining and manipulating infinite families of combinatorial objects such as graphs, partial orders, logical equations etc. We give special attentionto objects that can be represented as sequences of slices. We have successfully applied our theory to obtain novel results in three fields: concurrency theory,combinatorics and logic. Some notable results are:

    • Concurrency Theory:
    1. We prove that inclusion and emptiness of intersection of the causalbehavior of bounded Petri nets are decidable. These problems had been open for almost two decades.
    2. We introduce an algorithm to transitively reduce infinite familiesof DAGs. This algorithm allows us to operate with partial order languages defined via distinct formalisms, such as, Mazurkiewicztrace languages and message sequence chart languages.
    • Combinatorics:
    1. For each constant z ∈ N, we define the notion of z-topological or-der for digraphs, and use it as a point of connection between the monadic second order logic of graphs and directed width measures, such as directed path-width and cycle-rank. Through this connection we establish the polynomial time solvability of a large numberof natural counting problems on digraphs admitting z-topological orderings.
    • Logic:
    1. We introduce an ordered version of equational logic. We show thatthe validity problem for this logic is fixed parameter tractable withrespect to the depth of the proof DAG, and solvable in polynomial time with respect to several notions of width of the equations being proved. In this way we establish the polynomial time provability of equations that can be out of reach of techniques based on completion and heuristic search.
    Download full text (pdf)
    Combinatorial Slice Theory
  • 170.
    De Oliveira Oliveira, Mateus
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Subgraphs satisfying MSO properties on z-topologically orderable digraphs2013In: Parameterized and Exact Computation: 8th International Symposium, IPEC 2013, Sophia Antipolis, France, September 4-6, 2013, Revised Selected Papers, Springer, 2013, p. 123-136Conference paper (Refereed)
    Abstract [en]

    We introduce the notion of z-topological orderings for digraphs. We prove that given a digraph G on n vertices admitting a z-topological ordering, together with such an ordering, one may count the number of subgraphs of G that at the same time satisfy a monadic second order formula φ and are the union of k directed paths, in time f(φ,k,z)·nO(k·z). Our result implies the polynomial time solvability of many natural counting problems on digraphs admitting z-topological orderings for constant values of z and k. Concerning the relationship between z-topological orderability and other digraph width measures, we observe that any digraph of directed path-width d has a z-topological ordering for z ≤ 2d + 1. On the other hand, there are digraphs on n vertices admitting a z-topological order for z = 2, but whose directed path-width is Θ(log n). Since graphs of bounded directed path-width can have both arbitrarily large undirected tree-width and arbitrarily large clique width, our result provides for the first time a suitable way of partially transposing metatheorems developed in the context of the monadic second order logic of graphs of constant undirected tree-width and constant clique width to the realm of digraph width measures that are closed under taking subgraphs and whose constant levels incorporate families of graphs of arbitrarily large undirected tree-width and arbitrarily large clique width.

  • 171.
    de Rezende, Susanna F.
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Vinyals, Marc
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity)2016In: 2016 IEEE 57th Annual Symposium on Foundations of Computer Science (FOCS), IEEE Computer Society, 2016, Vol. 2016, p. 295-304Conference paper (Refereed)
    Abstract [en]

    We obtain the first true size-space trade-offs for the cutting planes proof system, where the upper bounds hold for size and total space for derivations with constant-size coefficients, and the lower bounds apply to length and formula space (i.e., number of inequalities in memory) even for derivations with exponentially large coefficients. These are also the first trade-offs to hold uniformly for resolution, polynomial calculus and cutting planes, thus capturing the main methods of reasoning used in current state-of-the-art SAT solvers. We prove our results by a reduction to communication lower bounds in a round-efficient version of the real communication model of [Krajicek ' 98], drawing on and extending techniques in [Raz and McKenzie ' 99] and [Goos et al. '15]. The communication lower bounds are in turn established by a reduction to trade-offs between cost and number of rounds in the game of [Dymond and Tompa '85] played on directed acyclic graphs. As a by-product of the techniques developed to show these proof complexity trade-off results, we also obtain an exponential separation between monotone-AC(i-1) and monotone-AC(i), improving exponentially over the superpolynomial separation in [Raz and McKenzie ' 99]. That is, we give an explicit Boolean function that can be computed by monotone Boolean circuits of depth log(i) n and polynomial size, but for which circuits of depth O (log(i-1) n) require exponential size.

  • 172.
    Dinges, Peter
    et al.
    University of Illinois at Urbana-Champaign.
    Agha, Gul
    University of Illinois at Urbana-Champaign.
    Palmskog, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dynamic Probabilistic Inference of Atomic SetsManuscript (preprint) (Other academic)
    Abstract [en]

    Concurrent programs often ensure the consistency of their data structures through synchronization.  Because control-centric synchronization primitives, such as locks, are disconnected from the consistency invariants of the data structures, a compiler cannot check and and enforce these invariants - making it hard to detect bugs caused by incorrect synchronization. Moreover, a consistency bug may be the result of some unlikely schedule and therefore not show up in program testing.  In contrast, data-centric synchronization adds annotations to data structures, defining sets of fields that must be accessed atomically. A compiler can check such annotations for consistency, detect deadlock, and automatically add primitives to prevent data races. However, annotating existing code is time consuming and error prone because it requires understanding the concurrency semantics implemented in the code. We propose a novel algorithm, called BAIT, for deriving such annotations automatically from observed program executions using Bayesian probabilistic inference. The algorithm produces atomic set, unit of work, and alias annotations for atomic-set based synchronization. Using our implementation of the algorithm, we have derived annotations for large code bases, for example the Java collections framework, in a matter of seconds. A comparison of the inferred annotations against manually converted programs, and two case studies on large, widely-used programs, show that our implementation derives detailed annotations of high quality.

  • 173. Ehn, Andreas
    et al.
    Niemelä, Fredrik
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kreitz, Gunnar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Strigeus, Ludvig
    Hult, Magnus
    Peer-to-Peer-strömmning av medieinnehåll2007Patent (Other (popular science, discussion, etc.))
  • 174.
    Ekerå, Martin
    et al.
    KTH, School of Computer Science and Communication (CSC). Swedish NCSA, Sweden.
    Håstad, Johan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Quantum algorithms for computing short discrete logarithms and factoring RSA integers2017In: 8th International Workshop on Post-Quantum Cryptography, PQCrypto 2017, Springer, 2017, Vol. 10346, p. 347-363Conference paper (Refereed)
    Abstract [en]

    We generalize the quantum algorithm for computing short discrete logarithms previously introduced by Ekerå [2] so as to allow for various tradeoffs between the number of times that the algorithm need be executed on the one hand, and the complexity of the algorithm and the requirements it imposes on the quantum computer on the other hand. Furthermore, we describe applications of algorithms for computing short discrete logarithms. In particular, we show how other important problems such as those of factoring RSA integers and of finding the order of groups under side information may be recast as short discrete logarithm problems. This gives rise to an algorithm for factoring RSA integers that is less complex than Shor’s general factoring algorithm in the sense that it imposes smaller requirements on the quantum computer. In both our algorithm and Shor’s algorithm, the main hurdle is to compute a modular exponentiation in superposition. When factoring an n bit integer, the exponent is of length 2n bits in Shor’s algorithm, compared to slightly more than n/2 bits in our algorithm.

  • 175.
    Elffers, Jan
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Johannsen, J.
    Lauria, M.
    Magnard, T.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Vinyals, Marc
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Trade-offs between time and memory in a tighter model of CDCL SAT solvers2016In: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Springer, 2016, p. 160-176Conference paper (Refereed)
    Abstract [en]

    A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that cap- tures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL with- out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.

  • 176. Emilio, Tuosto
    et al.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Semantics of global view of choreographies2017In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 95Article in journal (Refereed)
    Abstract [en]

    We propose two abstract semantics of the global view of choreographies given in terms of partial orders. The first semantics is formalised as pomsets of communication events while the second one is based on hypergraphs of events. These semantics can accommodate different levels of abstractions. We discuss the adequacy of our models by considering their relation with communicating machines, that we use to formalise the local view. Our approach increases expressiveness and allows us to overcome some limitations that affect alternative semantics of global views. This will be illustrated by discussing some interesting examples. Finally, we show that the two semantics are equivalent and have different merits. More precisely, the semantics based on pomsets yields a more elegant presentation, but it is less suitable for implementation. The semantics based on hypergraphs instead is amenable to a straightforward implementation.

  • 177.
    Enström, Emma
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dynamic programming - structure, difficulties and teaching2013In: 2013 IEEE Frontiers in Education Conference, New York: IEEE , 2013, p. 1857-1863Conference paper (Refereed)
    Abstract [en]

    In this paper we describe action research on our third year Algorithms, Data structures and Complexity course, in which students have considered dynamic programming hard in comparison to the other topics. Attempting to amend this, we wanted to know which difficulties the students encountered, where they gained their knowledge, and which tasks they were most certain that they could perform after the course. Such work resides in the didactics of the subject taught, but the general methods of attacking perceived difficulties in a course can be tried on any course. We identified subtasks that could be taught separately, and adapted the lectures to Pattern Oriented Instruction in order to help students cope with the cognitive complexity of solving problems using dynamic programming. For this, we prepared new clicker questions, visualisations and a lab assignment. We also constructed self-efficacy items on the course goals for dynamic programming, and administered them before and after the teaching and learning activities. Among the self-efficacy items, determining the evaluation order and solving a problem with dynamic programming with no hints had the lowest score after the course. As for the activities, arguing correctness of a solution was something many students claimed that they did not learn anywhere. Students considered the lab exercise most useful, but they also learned a lot from the other activities.

  • 178.
    Enström, Emma
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    On difficult topics in theoretical computer science education2014Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This thesis primarily reports on an action research project that has been conducted on a course in theoretical computer science (TCS). The course is called Algorithms, data structures, and complexity (ADC) and is given at KTH Royal Institute of Technology in Stockholm, Sweden.

    The ADC course is an introduction to TCS, but resembles and succeeds courses introducing programming, system development best practices, problem solving, proving, and logic. Requiring the completion of four programming projects, the course can easily be perceived as a programming course by the students. Most previous research in computer science education has been on programming and introductory courses.

    The focus of the thesis work has been to understand what subject matter is particularly difficult to students. In three action research cycles, the course has been studied and improved to alleviate the discovered difficulties. We also discuss how the course design may color students’ perceptions of what TCS is. Most of the results are descriptive.

    Additionally, automated assessment has been introduced in the ADC course as well as in introductory courses for non-CS majors. Automated assessment is appreciated by the students and is directing their attention to the importance of program correctness. A drawback is that the exercises in their current form are not likely to encourage students to take responsibility for program correctness.

    The most difficult tasks of the course are related to proving correctness, solving complex dynamic programming problems, and to reductions. A certain confusion regarding the epistemology, tools and discourse of the ADC course and of TCS in general can be glimpsed in the way difficulties manifest themselves. Possible consequences of viewing the highly mathematical problems and tools of ADC in more practical, programming, perspective, are discussed. It is likely that teachers could explicitly address more of the nature and discourse of TCS in order to reduce confusion among the students, for instance regarding the use of such words and constructs as “problem”, “verify a solution”, and “proof sketch”.

    One of the tools used to study difficulties was self-efficacy surveys. No correlation was found between the self-efficacy beliefs and the graded performance on the course. Further investigation of this is beyond the scope of this thesis, but may be done with tasks corresponding more closely and exclusively to each self-efficacy item.

    Didactics is an additional way for a professional to understand his or her subject. Didactics is concerned with the teaching and learning of something, and hence sheds light on that “something” from an angle that sometimes is not reflected on by its professionals. Reflecting on didactical aspects of TCS can enrichen the understanding of the subject itself, which is one goal with this work.

    Download full text (pdf)
    Enstroem2014.pdf
  • 179.
    Enström, Emma
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kann, Viggo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Computer Lab Work on Theory2010In: ITICSE 2010: PROCEEDINGS OF THE 2010 ACM SIGSE ANNUAL CONFERENCE ON INNOVATION AND TECHNOLOGY IN COMPUTER SCIENCE EDUCATION, NEW YORK: ASSOC COMPUTING MACHINERY , 2010, p. 93-97Conference paper (Refereed)
    Abstract [en]

    This paper describes an attempt to introduce computer lab exercises on NP-completeness proofs in a class already containing computer lab exercises on algorithms and data structures. In the article we are interested in the answer of the following question: Can the students feel that their understanding of theoretical computer science is improved by performing a computer lab exercise on the subject? The class is mandatory for students in a computer science program, and is taken by about 130 students each year. Theory of NP-completeness proofs with reductions has previous years been examined on an individual assignment with written solutions handed in and later explained orally by the student to a teacher. The new assignment is performed as a computer lab exercise where students are working in small groups of two. This exercise is placed before the individual assignment, and is examined first by running automated test cases and later by an oral presentation in lab to a teacher. An improvement can be observed of the students' average results since the new assignment was introduced. This is not enough to prove the benefit of using the new assignment. However, the responses to questionnaires at course evaluations show that almost all students think that the assignment redly gave them better understanding of polynomial reductions in NP completeness proofs. The students' result on the new assignment corresponds closely to their results on the following individual assignment. Seemingly, the new assignment predicts accurately who is going to pass the following assignment.

  • 180.
    Enström, Emma
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kann, Viggo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Iteratively Intervening with the “Most Difficult” Topics of an Algorithms and Complexity Course2017In: ACM Transactions on Computing Education, E-ISSN 1946-6226, Vol. 17, no 1, article id 4Article in journal (Refereed)
    Abstract [en]

    When compared to earlier programming and data structure experiences that our students might have, the perspective changes on computers and programming when introducing theoretical computer science into the picture. Underlying computational models need to be addressed, and mathematical tools employed, to understand the quality criteria of theoretical computer science. Focus shifts from doing to proving. Over several years, we have tried to make this perspective transition smoother for the students of a third-year mandatory algorithms, data structures, and computational complexity course. The concepts receiving extra attention in this work are NP-completeness, one of the most central concepts in computer science, and dynamic programming, an algorithm construction method that is powerful but somewhat unintuitive for some students.

    The major difficulties that we attribute to NP-completeness are that the tasks look similar but have a different purpose than in algorithm construction exercises. Students do not immediately see the usefulness of the concept, and hence motivation could be one issue. One line of attacking NP-completeness has been to emphasize its algorithmic aspects using typical tools for teaching algorithms.

    Some potential difficulties associated with dynamic programming are that the method is based on a known difficult concept—recursion—and that there are many ingredients in a dynamic programming solution to a problem.

    For both dynamic programming and NP-completeness, we have invented several new activities and structured the teaching differently, forcing students to think and adopt a standpoint, and practice the concepts in programming assignments. Student surveys show that these activities are appreciated by the students, and our evaluations indicate that they have positive effects on learning. We believe that these activities could be useful in any similar course.

    The approach to improving the course is action research, and the evaluation has been done using course surveys, self-efficacy surveys, rubrics-like grading protocols, and grades. We have also interviewed teaching assistants about their experiences.

  • 181.
    Enström, Emma
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kann, Viggo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Iteratively interventing with the "most difficult" topics of an algorithms and complexity courseManuscript (preprint) (Other academic)
  • 182.
    Enström, Emma
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kreitz, Gunnar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niemelä, Fredrik
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kann, Viggo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Testdriven utbildning — strukturerad formativ examination2010Conference paper (Other academic)
  • 183.
    Enström, Emma
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Kreitz, Gunnar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niemelä, Fredrik
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Söderman, Pehr
    KTH, School of Information and Communication Technology (ICT), Communication: Services and Infrastucture, Telecommunication Systems Laboratory, TSLab.
    Kann, Viggo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Five Years with Kattis – Using an Automated Assessment System in Teaching2011In: 2011 Frontiers in Education Conference (FIE), New York: IEEE , 2011Conference paper (Refereed)
    Abstract [en]

    Automated assessment systems have been employed in computer science (CS) courses at a number of different universities. Such systems are especially applicable in teaching algorithmic problem solving since they can automatically test if an algorithm has been correctly implemented, i.e., that it performs its specified function on a set of inputs. Being able to implement algorithms that work correctly is a crucial skill for CS students in their professional role, but it can be difficult to convey the importance of this in a classroom situation. Programming and problem solving education supported by automated grading has been used since 2002 at our department. We study, using action research methodology, different strategies for deploying automated assessment systems in CS courses. Towards this end, we have developed an automated assessment system and both introduced it into existing courses and constructed new courses structured around it. Our primary data sources for evaluation consists of course evaluations, statistics on students' submitted solutions, and experience teaching the courses. Authors of this paper have been participating in teaching all of the courses mentioned here.

  • 184. Eriksson, Gunnar
    et al.
    Karlgren, Jussi
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Features for modelling characteristics of conversations: Notebook for PAN at CLEF 20122012In: CLEF 2012 Evaluation Labs and Workshop Online Working Notes, 2012Conference paper (Refereed)
    Abstract [en]

    In this experiment, we find that features which model interaction andconversational behaviour contribute well to identifying sexual grooming behaviourin chat and forum text. Together with the obviously useful lexical features —which we find are more valuable if separated by who generates them — weachieve very successful results in identifying behavioural patterns which maycharacterise sexual grooming. We conjecture that the general framework can beused for other purposes than this specific case if the lexical features are exchangedfor other topical models, the conversational features characterise interaction andbehaviour rather than topical choice.

    Download full text (pdf)
    fulltext
  • 185.
    Feng, Lei
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Lundmark, Simon
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Mudassar A.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Wong, Peter Y. H.
    Case studies in learning-based testing2013In: Testing Software and Systems: 25th IFIP WG 6.1 International Conference, ICTSS 2013, Istanbul, Turkey, November 13-15, 2013, Proceedings, Springer, 2013, p. 164-179Conference paper (Refereed)
    Abstract [en]

    We present case studies which show how the paradigm of learning-based testing (LBT) can be successfully applied to black-box requirements testing of industrial reactive systems. For this, we apply a new testing tool LBTest, which combines algorithms for incremental black-box learning of Kripke structures with model checking technology. We show how test requirements can be modeled in propositional linear temporal logic extended by finite data types.We then provide benchmark performance results for LBTest applied to three industrial case studies.

    Download full text (pdf)
    fulltext
  • 186.
    Feng, Lei
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Meinke, Karl
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Niu, Fei
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sindhu, Muddassar
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Wong, Peter Y. H.
    SDL Fredhopper.
    Case Studies in Learning-based Testing2013Report (Other academic)
    Abstract [en]

    We present case studies which show how the paradigm of learning-based testing (LBT) can be successfully applied to black-box requirements testing of reactive systems. For this we apply a new testing tool LBTest, which combines algorithms for incremental black-box learning of Kripke structures with model checking technology. We show how test requirements can be modeled in propositional linear temporal logic extended by finite abstract data types. We provide benchmark performance results for LBTest applied to two industrial case studies. Finally we present a first coverage study for the tool.

  • 187.
    Fetahi, Wuhib
    et al.
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Stadler, Rolf
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Alexander, Clemm
    Cisco Systems, San Jose, CA USA.
    Robust Monitoring of Network-wide Aggregates through Gossiping2009In: IEEE Transactions on Network and Service Management, ISSN 1932-4537, E-ISSN 1932-4537, Vol. 6, no 2, p. 95-109Article in journal (Refereed)
    Abstract [en]

    We investigate the use of gossip protocols for continuousmonitoring of network-wide aggregates under crash failures.Aggregates are computed from local management variablesusing functions such as SUM, MAX, or AVERAGE. For this typeof aggregation, crash failures offer a particular challenge dueto the problem of mass loss, namely, how to correctly accountfor contributions from nodes that have failed. In this paper wegive a partial solution. We present G-GAP, a gossip protocolfor continuous monitoring of aggregates, which is robust againstfailures that are discontiguous in the sense that neighboringnodes do not fail within a short period of each other. We giveformal proofs of correctness and convergence, and we evaluatethe protocol through simulation using real traces. The simulationresults suggest that the design goals for this protocol have beenmet. For instance, the tradeoff between estimation accuracyand protocol overhead can be controlled, and a high estimationaccuracy (below some 5% error in our measurements) is achievedby the protocol, even for large networks and frequent nodefailures. Further, we perform a comparative assessment of GGAPagainst a tree-based aggregation protocol using simulation.Surprisingly, we find that the tree-based aggregation protocolconsistently outperforms the gossip protocol for comparativeoverhead, both in terms of accuracy and robustness.

    Download full text (pdf)
    fulltext
  • 188. Filmus, Y.
    et al.
    Lauria, M.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Thapen, N.
    Ron-Zewi, N.
    Space complexity in polynomial calculus2012In: Computational Complexity (CCC), 2012 IEEE 27th Annual Conference on, IEEE , 2012, p. 334-344Conference paper (Refereed)
    Abstract [en]

    During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving. For the polynomial calculus proof system, the only previously known space lower bound is for CNF formulas of unbounded width in [Alekhnovich et. al.'02], where the lower bound is smaller than the initial width of the clauses in the formulas. Thus, in particular, it has been consistent with current knowledge that polynomial calculus could refute any k-CNF formula in constant space. We prove several new results on space in polynomial calculus (PC) and in the extended proof system polynomial calculus resolution (PCR) studied in [Alekhnovich et.al.~'02]. - For PCR, we prove an Omega(n) space lower bound for a bit wise encoding of the functional pigeonhole principle with m pigeons and n holes. These formulas have width O(log(n)), and hence this is an exponential improvement over [Alekhnovich et.al.~'02] measured in the width of the formulas. - We then present another encoding of the pigeonhole principle that has constant width, and prove an Omega(n) space lower bound in PCR for these formulas as well. - We prove an Omega(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHP(m, n) with m pigeons and n holes, and show that this is tight. - We prove that any k-CNF formula can be refuted in PC in simultaneous exponential size and linear space (which holds for resolution and thus for PCR, but was not known to be the case for PC). We also characterize a natural class of CNF formulas for which the space complexity in resolution and PCR does not change when the formula is transformed into 3-CNF in the canonical way.

  • 189. Filmus, Y.
    et al.
    Lauria, Massimo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Mikša, Mladen
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Vinyals, M.
    From small space to small width in resolution2015In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 16, no 4, article id 28Article in journal (Refereed)
    Abstract [en]

    In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fraïssé games. We give an alternative, more explicit, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexitymeasure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similarmethods.

  • 190. Filmus, Y.
    et al.
    Lauria, Massimo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Mikša, Mladen
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Vinyals, Marc
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    From small space to small width in resolution2014In: 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2014, Vol. 25, p. 300-311Conference paper (Refereed)
    Abstract [en]

    In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.

  • 191. Filmus, Yuval
    et al.
    Lauria, Massimo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Mikša, Mladen
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Vinyals, Marc
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Towards an understanding of polynomial calculus: New separations and lower bounds (extended abstract)2013In: Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part I, Springer, 2013, no PART 1, p. 437-448Conference paper (Refereed)
    Abstract [en]

    During the last decade, an active line of research in proof complexity has been into the space complexity of proofs and how space is related to other measures. By now these aspects of resolution are fairly well understood, but many open problems remain for the related but stronger polynomial calculus (PC/PCR) proof system. For instance, the space complexity of many standard "benchmark formulas" is still open, as well as the relation of space to size and degree in PC/PCR. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PCR space, providing some circumstantial evidence that degree might be a lower bound for space. More importantly, this immediately yields formulas that are very hard for space but very easy for size, exhibiting a size-space separation similar to what is known for resolution. Using related ideas, we show that if a graph has good expansion and in addition its edge set can be partitioned into short cycles, then the Tseitin formula over this graph requires large PCR space. In particular, Tseitin formulas over random 4-regular graphs almost surely require space at least Ω(√n). Our proofs use techniques recently introduced in [Bonacina-Galesi '13]. Our final contribution, however, is to show that these techniques provably cannot yield non-constant space lower bounds for the functional pigeonhole principle, delineating the limitations of this framework and suggesting that we are still far from characterizing PC/PCR space.

  • 192. Filmus, Yuval
    et al.
    Lauria, Massimo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nordstrom, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Ron-Zewi, Noga
    Thapen, Neil
    Space complexity in polynomial calculus2015In: SIAM journal on computing (Print), ISSN 0097-5397, E-ISSN 1095-7111, Vol. 44, no 4, p. 1119-1153Article in journal (Refereed)
    Abstract [en]

    During the last 10 to 15 years, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important concern in SAT solving, and so research has mostly focused on weak systems that are used by SAT solvers. There has been a relatively long sequence of papers on space in resolution, which is now reasonably well-understood from this point of view. For other proof systems of interest, however, such as polynomial calculus or cutting planes, progress has been more limited. Essentially nothing has been known about space complexity in cutting planes, and for polynomial calculus the only lower bound has been for conjunctive normal form (CNF) formulas of unbounded width in [Alekhnovich et al., SIAM J. Comput., 31 (2002), pp. 1184-1211], where the space lower bound is smaller than the initial width of the clauses in the formulas. Thus, in particular, it has been consistent with current knowledge that polynomial calculus could be able to refute any k-CNF formula in constant space. In this paper, we prove several new results on space in polynomial calculus (PC) and in the extended proof system polynomial calculus resolution (PCR) studied by Alekhnovich et al.: (1) We prove an omega(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHPmn with m pigeons and n holes, and show that this is tight. (2) For PCR, we prove an omega(n) space lower bound for a bitwise encoding of the functional pigeonhole principle. These formulas have width O(log n), and hence this is an exponential improvement over Alekhnovich et al. measured in the width of the formulas. (3) We then present another encoding of the pigeonhole principle that has constant width, and prove an omega(n) space lower bound in PCR for these formulas as well. (4) Finally, we prove that any k-CNF formula can be refuted in PC in simultaneous exponential size and linear space (which holds for resolution and thus for PCR, but was not obviously the case for PC). We also characterize a natural class of CNF formulas for which the space complexity in resolution and PCR does not change when the formula is transformed into 3-CNF in the canonical way, something that we believe can be useful when proving PCR space lower bounds for other well-studied formula families in proof complexity.

  • 193. Filmus, Yuval
    et al.
    Lauria, Massimo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nordström, Jakob
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Ron-Zewi, Noga
    Thapen, Neil
    Space Complexity in Polynomial Calculus2012In: Electronic Colloquium on Computational Complexity (ECCC), ISSN 1433-8092, no 132Article in journal (Refereed)
    Abstract [en]

    During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving, and so research has mostly focused on weak systems that are used by SAT solvers.

    There has been a relatively long sequence of papers on space in resolution, which is now reasonably well understood from this point of view.  For other natural candidates to study, however, such as polynomial calculus or cutting planes, very little has been known. We are not aware of any nontrivial space lower bounds for cutting planes, and for polynomial calculus the only lower bound has been for CNF formulas of unbounded width in [Alekhnovich et al. '02], where the space lower bound is smaller than the initial width of the clauses in the formulas.  Thus, in particular, it has been consistent with current knowledge that polynomial calculus could be able to refute any k-CNF formula in constant space.

    In this paper, we prove several new results on space in polynomial calculus (PC), and in the extended proof system polynomial calculus resolution (PCR) studied in [Alekhnovich et al. '02]:

    (1) We prove an Omega(n) space lower bound in PC for the canonical 3-CNF version of the pigeonhole principle formulas PHP^m_n with m pigeons and n holes, and show that this is tight.

    (2) For PCR, we prove an Omega(n) space lower bound for a bitwise encoding of the functional pigeonhole principle.  These formulas have width O(log n), and hence this is an exponential improvement over [Alekhnovich et al. '02] measured in the width of the formulas.

    (3) We then present another encoding of the pigeonhole principle that has constant width, and prove an Omega(n) space lower bound in PCR for these formulas as well.

    (4) Finally, we prove that any k-CNF formula can be refuted in PC in simultaneous exponential size and linear space (which holds for resolution and thus for PCR, but was not obviously the case for PC). We also characterize a natural class of CNF formulas for which the space complexity in resolution and PCR does not change when the formula is transformed into 3-CNF in the canonical way, something that we believe can be useful when proving PCR space lower bounds for other well-studied formula families in proof complexity.

  • 194. Forner, Pamela
    et al.
    Bentivogli, Luisa
    Braschler, Martin
    Choukri, Khalid
    Ferro, Nicola
    Hanbury, Allan
    Karlgren, Jussi
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Müller, Henning
    PROMISE Technology Transfer Day: Spreading the Word on Information Access Evaluation at an Industrial Event: WORKSHOP REPORT2013In: SIGIR Forum, ISSN 0163-5840, E-ISSN 1558-0229, Vol. 47, no 1, p. 53-58Article in journal (Refereed)
    Abstract [en]

    The Technology Transfer Day was held at CeBIT 2013 from March 5 to March 9, at the Deutsche Messe in Hannover, Germany. PROMISE presented three events at CeBIT: a panel in the CeBIT Global Conference (CGC) - Power Stage, a one-day workshop hosted in the CeBIT Convention Center, and a stand "EU Language & Big Data Projects" in Hall 9. The whole program included 4 panelists, 12 invited talks, and an discussions among the speakers and with the public. This report overviews the aims and contents of the events and outlines the major outcomes. 

    Download full text (pdf)
    fulltext
  • 195.
    Fredriksson, Morgan
    et al.
    Liquid Media.
    Königsmann, Jugen
    Liquid Media.
    Bartie, Phil
    Edinburgh University.
    Boye, Johan
    KTH, School of Computer Science and Communication (CSC), Speech, Music and Hearing, TMH.
    Dalmas, Tiphaine
    Edinburgh University.
    Götze, Jana
    KTH, School of Computer Science and Communication (CSC), Speech, Music and Hearing, TMH.
    Mollevik, Johan
    Umeå University.
    Janarthanam, Srini
    Heriot Watt.
    Lemon, Oliver
    Heriot Watt.
    Liu, Xingkun
    Heriot Watt.
    Minock, Michael
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    D5.2.2: Final city search SpaceBook prototype2014Report (Other academic)
  • 196.
    Frenckner, Kerstin
    et al.
    KTH, School of Computer Science and Communication (CSC), Human - Computer Interaction, MDI.
    Hedin, Björn
    KTH, School of Computer Science and Communication (CSC), Media Technology and Graphic Arts, Media.
    Kann, Viggo
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Nilsson, Stefan
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Att utvärderas och utvecklas: om datalogi och medieteknik i ljuset av EAE på KTH2011In: 3:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar, Linköping University Electronic Press , 2011, p. 82-86Conference paper (Refereed)
    Abstract [sv]

    Under 2011 genomförs en stor utvärdering av samtliga utbildningsprogram på KTH. Projektet går under namnet Education Assessment Exercise (EAE) och är den största enskilda aktiviteten inom KTH:s systematiska kvalitetsarbete under året [2]. Projektet går genom tre huvudstadier: självvärdering, extern bedömning och uppföljning. Den första delen skedde under våren 2011, del två i augusti, medan större delen av uppföljning och utveckling var tänkt att ligga efter bedömarnas slutrapport i oktober. Det stadiet påbörjades dock redan i augusti. Syftet med EAE är i första hand att bidra till kvalitetsutveckling, men EAE fungerar också som en förberedelse inför den utvärdering som Högskoleverket planerar att genomföra under 2012.

    Skolan för datavetenskap och kommunikation (CSC) vid KTH ansvarar för civilingenjörs-, master- och kandidatprogram inom datalogi och datateknik, medieteknik, beräkningsteknik och människa-datorinteraktion. Skolan ansvarar också för ett stort utbud av kurser inom skolans ämnen, datalogi, medieteknik, människa-datorinteraktion, numerisk analys och tal- och musikkommunikation, liksom omfattande forskning i dessa ämnen.

    Skolan ger kurser inte bara för studenter på skolans egna program utan även för studenter på andra skolors program. Studenterna på CSC-skolans program läser inte bara CSC-skolans kurser utan även kurser som ges av andra skolor, till exempel matematikkurser från Skolan för teknikvetenskap.

    CSC har länge haft ett systematiskt kvalitetsarbete inom grundutbildningen, som bland annat ledde till att skolan tilldelades Högskoleverkets utmärkelse Framstående utbildningsmiljö 2009. I denna artikel beskriver vi skolans kvalitetsarbete och arbete med EAE, i alla faser av utvärderingsprojektet.

  • 197. Fried, D.
    et al.
    Shimony, S. E.
    Benbassat, A.
    Wenner, Cenny
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Complexity of Canadian traveler problem variants2013In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 487, p. 1-16Article in journal (Refereed)
    Abstract [en]

    The Canadian traveler problem (CTP) is the problem of traversing a given graph, where some of the edges may be blocked-a state which is revealed only upon reaching an incident vertex. Originally stated by Papadimitriou and Yannakakis (1991) [1], the adversarial version of the CTP was shown to be PSPACE-complete, with the stochastic version shown to be in PSPACE and #P-hard. We show that the stochastic CTP is also PSPACE-complete: initially proving PSPACE-hardness for the dependent version of the stochastic CTP, and proceeding with gadgets that allow us to extend the proof to the independent case. Since for disjoint-path graphs, the CTP can be solved in polynomial time, we examine the complexity of the more general remote-sensing CTP, and show that it is NP-hard even for disjoint-path graphs.

  • 198.
    Fu, Jing
    et al.
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Hagsand, Olof
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Karlsson, Gunnar
    KTH, School of Electrical Engineering (EES), Communication Networks.
    An analysis of Queueing Behavior in Network Processor Systems2006In: 4th Swedish National Computer Networking Workshop, SNCNW 2006, Luleå, Sweden, 2006Conference paper (Refereed)
  • 199.
    Fu, Jing
    et al.
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Hagsand, Olof
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Karlsson, Gunnar
    KTH, School of Electrical Engineering (EES), Communication Networks.
    Performance Evaluation and Cache Behavior of LC-Trie for IP-Address Lookup2006In: Proc. of IEEE 2006 Workshop on High Performance Switching and Routing (HPSR 2006), IEEE , 2006, p. 29-35Conference paper (Refereed)
    Abstract [en]

    Many IP-address lookup software algorithms use a trie-like data structure to perform longest prefix match. LC-trie is an efficient algorithm that uses level compression and path compression on tries. By using realistic and synthetically generated traces, we study the performance of the LC-trie algorithm. Our study includes trie search depth, prefix vector access behavior, cache behavior, and packet lookup service time. The results show that for a realistic traffic trace, the LC-trie algorithm is capable of performing 20 million packet lookups per second on a Pentium 4, 2.8 GHz computer, which corresponds to a 40 Gb/s link for average sized packets. Further, the results show that LC-trie performs up to five times better on the realistic trace compared to a synthetically generated network trace. This illustrates that the choice of traces may have a large influence on the results when evaluating lookup algorithms.

  • 200. Gajarský, J.
    et al.
    Lampis, Michael
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Ordyniak, S.
    Parameterized algorithms for modular-width2013In: Parameterized and Exact Computation: 8th International Symposium, IPEC 2013, Sophia Antipolis, France, September 4-6, 2013, Revised Selected Papers, Springer, 2013, p. 163-176Conference paper (Refereed)
    Abstract [en]

    It is known that a number of natural graph problems which are FPT parameterized by treewidth become W-hard when parameterized by clique-width. It is therefore desirable to find a different structural graph parameter which is as general as possible, covers dense graphs but does not incur such a heavy algorithmic penalty. The main contribution of this paper is to consider a parameter called modular-width, defined using the well-known notion of modular decompositions. Using a combination of ILP and dynamic programming we manage to design FPT algorithms for Coloring and Partitioning into paths (and hence Hamiltonian path and Hamiltonian cycle), which are W-hard for both clique-width and its recently introduced restriction, shrub-depth. We thus argue that modular-width occupies a sweet spot as a graph parameter, generalizing several simpler notions on dense graphs but still evading the "price of generality" paid by clique-width.

1234567 151 - 200 of 518
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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