uu.seUppsala universitets publikationer
Ändra sökning
Avgränsa sökresultatet
123456 1 - 50 av 252
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Träffar per sida
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
Markera
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1. Aarts, Fides
    et al.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Uijen, Johan
    Vaandrager, Frits
    Generating models of infinite-state communication protocols using regular inference with abstraction2015Ingår i: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 46, nr 1, s. 1-41Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.

  • 2.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Optimal dynamic partial order reduction2014Ingår i: Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York: ACM Press, 2014, s. 373-384Konferensbidrag (Refereegranskat)
    Abstract [en]

    Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.

  • 3.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    IRIF Université Paris Diderot, Paris, France.
    Ngo, Tuan Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Context-bounded analysis for POWER2017Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2017, s. 56-74Konferensbidrag (Refereegranskat)
    Abstract [en]

    We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis initiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.

  • 4.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    Ngo, Tuan Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Replacing store buffers by load buffers in TSO2018Ingår i: Verification and Evaluation of Computer and Communication Systems, Springer, 2018, s. 22-28Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider the weak memory model of Total Store Ordering (TSO). In the classical definition of TSO, an unbounded buffer is inserted between each process and the shared memory. The buffers contains pending store operations of the processes. We introduce a new model where we replace the store buffers by load buffers. In contrast to the classical model, the buffers now contain load operations. We show that the models have equivalent behaviors in the sense that the processes reach identical sets of states when the input program is run under the two models.

  • 5.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bui, Phi Diep
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Counter-Example Guided Program Verification2016Ingår i: FM 2016: Formal Methods, Springer, 2016, s. 25-42Konferensbidrag (Refereegranskat)
  • 6.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Institute of Information Science, Academia Sinica .
    Holik, Lukas
    Brno University.
    Rezine, Ahmed
    Linköping University.
    Rümmer, Philipp
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    String Constraints for Verification2014Ingår i: Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Springer, 2014, s. 150-166Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.

  • 7.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hofman, Piotr
    Mayr, Richard
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Totzke, Patrick
    Infinite-state energy games2014Ingår i: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, New York: ACM Press, 2014Konferensbidrag (Refereegranskat)
    Abstract [en]

    Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this.

    We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata.

    Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

  • 8.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verification of Directed Acyclic Ad Hoc Networks2013Ingår i: Formal Techniques for Distributed Systems: FORTE 2013, Springer Berlin/Heidelberg, 2013, s. 193-208Konferensbidrag (Refereegranskat)
  • 9.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stenman, Jari
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Computing optimal reachability costs in priced dense-timed pushdown automata2014Ingår i: Language and Automata Theory and Applications: LATA 2014, Springer Berlin/Heidelberg, 2014, s. 62-75Konferensbidrag (Refereegranskat)
  • 10.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stenman, Jari
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Zenoness for Timed Pushdown Automata2014Ingår i: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., 2014, s. -47Konferensbidrag (Refereegranskat)
    Abstract [en]

    Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.

  • 11.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Clemente, Lorenzo
    Mayr, Richard
    Sandberg, Sven
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stochastic Parity Games on Lossy Channel Systems2014Ingår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 10, nr 4, artikel-id 21Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, under the constraint that both players are restricted to finitememory strategies. First, we describe a general framework, where we consider the class of 21/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.

  • 12.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Dwarkadas, Sandhya
    University of Rochester, U.S.A..
    Rezine, Ahmed
    Linköping University.
    Shriraman, Arrvindh
    Simon Fraser University, Canada .
    Yunyun, Zhu
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verifying safety and liveness for the FlexTM hybrid transactional memory2013Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider the verification of safety (strict serializability and abort consistency) and liveness obstruction and livelock freedom) for the hybrid transactional memory framework FlexTM. This framework allows for flexible implementations of transactional memories based on an adaptation of the MESI coherence protocol. FlexTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use of the latest antichain based techniques to handle systems with tens of thousands of states.

  • 13.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Block me if you can!: Context-sensitive parameterized verification2014Ingår i: Static Analysis: SAS 2014, Springer, 2014, s. 1-17Konferensbidrag (Refereegranskat)
    Abstract [en]

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

  • 14.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Brno Univ Technol, Brno, Czech Republic.
    Parameterized verification through view abstraction2016Ingår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, nr 5, s. 495-516Artikel i tidskrift (Refereegranskat)
    Abstract [en]

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

  • 15.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukáš
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    All for the price of few: (Parameterized verification through view abstraction)2013Ingår i: Verification, Model Checking, and Abstract Interpretation, Springer Berlin/Heidelberg, 2013, s. 476-495Konferensbidrag (Refereegranskat)
  • 16.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Trinh, Cong Quy
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Automated Verification of Linearization Policies2016Ingår i: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, 2016Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.

  • 17.
    Abdullah, Jakaria
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Dai, Gaoyang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Mohaqeqi, Morteza
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Schedulability Analysis and Software Synthesis for Graph-Based Task Models with Resource Sharing2018Ingår i: Proc. 24th Real-Time and Embedded Technology and Applications Symposium, IEEE Computer Society, 2018, s. 261-270Konferensbidrag (Refereegranskat)
  • 18.
    Alipour, Mehdi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Carlson, Trevor E.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    A Taxonomy of Out-of-Order Instruction Commit2017Ingår i: 2017 Ieee International Symposium On Performance Analysis Of Systems And Software (Ispass), Los Alamitos: IEEE Computer Society, 2017, s. 135-136Konferensbidrag (Refereegranskat)
    Abstract [en]

    While in-order instruction commit has its advantages, such as providing precise interrupts and avoiding complications with the memory consistency model, it requires the core to hold on to resources (reorder buffer entries, load/store queue entries, registers) until they are released in program order. In contrast, out-of-order commit releases resources much earlier, yielding improved performance without the need for additional hardware resources. In this paper, we revisit out-of-order commit from a different perspective, not by proposing another hardware technique, but by introducing a taxonomy and evaluating three different micro-architectures that have this technique enabled. We show how smaller processors can benefit from simple out-oforder commit strategies, but that larger, aggressive cores require more aggressive strategies to improve performance.

  • 19.
    Alipour, Mehdi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kumar, Rakesh
    Norwegian Univ Sci & Technol, Dept Comp Sci, Trondheim, Norway.
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Black-Schaffer, David
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    FIFOrder MicroArchitecture: Ready-Aware Instruction Scheduling for OoO Processors2019Ingår i: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE, 2019, s. 716-721Konferensbidrag (Refereegranskat)
    Abstract [en]

    The number of instructions a processor's instruction queue can examine (depth) and the number it can issue together (width) determine its ability to take advantage of the ILP in an application. Unfortunately, increasing either the width or depth of the instruction queue is very costly due to the content-addressable logic needed to wakeup and select instructions out-of-order. This work makes the observation that a large number of instructions have both operands ready at dispatch, and therefore do not benefit from out-of-order scheduling. We leverage this to place such ready-at-dispatch instructions in separate, simpler, in-order FIFO queues for scheduling. With such additional queues, we can reduce the size and width of the expensive out-of-order instruction queue, without reducing the processor's overall issue width and depth. Our design, FIFOrder, is able to steer more than 60% of instructions to the cheaper FIFO queues, providing a 50% energy savings over a traditional out-of-order instruction queue design, while delivering 8% higher performance.

  • 20.
    Antonova, M.
    et al.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Asfandiyarov, R.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Bayes, R.
    Univ Glasgow, Sch Phys & Astron, Glasgow, Lanark, Scotland..
    Benoit, P.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Blondel, A.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Bogomilov, M.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Bross, A.
    Fermilab Natl Accelerator Lab, POB 500, Batavia, IL 60510 USA..
    Cadoux, F.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Cervera, A.
    CSIC, IFIC, Valencia, Spain.;Univ Valencia, Valencia, Spain..
    Chikuma, N.
    Univ Tokyo, Tokyo, Japan..
    Dudarev, A.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Ekelöf, Tord
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Fysiska sektionen, Institutionen för fysik och astronomi, Högenergifysik.
    Favre, Y.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Fedotov, S.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Hallsjo, S-P
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Ichikawa, A. K.
    Kyoto Univ, Kyoto, Japan..
    Izmaylov, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Karadzhov, Y.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Khabibullin, M.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Khotyantsev, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Kleymenova, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Koga, T.
    Univ Tokyo, Tokyo, Japan..
    Kostin, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Kudenko, Y.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Likhacheva, V.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Martinez, B.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Matev, R.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Medvedeva, M.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Mefodiev, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Minamino, A.
    Yokohama Natl Univ, Yokohama, Kanagawa, Japan..
    Mineev, O.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Mitev, G.
    Bulgarian Acad Sci, Inst Nucl Res & Nucl Energy, Sofia, Bulgaria..
    Nessi, M.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Nicola, L.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Noah, E.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Ovsiannikova, T.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Da Silva, H. Pais
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Parsa, S.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Rayner, M.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Rolando, G.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Shaykhiev, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Simion, P.
    Uppsala universitet.
    Soler, P.
    Univ Glasgow, Sch Phys & Astron, Glasgow, Lanark, Scotland..
    Suvorov, S.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Tsenov, R.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Ten Kate, H.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Vankova-Kirilova, G.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Yershov, N.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Synchronization of the distributed readout frontend electronics of the Baby MIND detector2017Ingår i: 2017 XXVI International Scientific Conference Electronics (ET), IEEE, 2017Konferensbidrag (Refereegranskat)
    Abstract [en]

    Baby MIND is a new downstream muon range detector for the WGASCI experiment. This article discusses the distributed readout system and its timing requirements. The paper presents the design of the synchronization subsystem and the results of its test.

  • 21.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Lystig Fritchie, Scott
    VMware, Cambridge, MA, USA.
    Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking2017Konferensbidrag (Refereegranskat)
    Abstract [en]

    Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.

  • 22.
    Asada, Akira
    et al.
    Osaka Inst Technol, Fac Informat Sci & Technol, Osaka, Japan.
    Hayashi, Masaki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Hirayama, Makoto J.
    Osaka Inst Technol, Fac Informat Sci & Technol, Osaka, Japan.
    TV production tool to make art programmes based on a simple scenario2019Ingår i: INTERNATIONAL WORKSHOP ON ADVANCED IMAGE TECHNOLOGY (IWAIT) 2019 / [ed] Kemao, Q Hayase, K Lau, PY Lie, WN Lee, YL Srisuk, S Yu, L, SPIE-INT SOC OPTICAL ENGINEERING , 2019, artikel-id 1104921Konferensbidrag (Refereegranskat)
    Abstract [en]

    We have been studying and developing the real-time Computer Graphics (CG) based virtual museum where a user can walk through to appreciate artworks digitized in high-resolution. Our virtual museum also has a function to automatically create TV program-like CG animations using 3D CG models in the virtual space as it is so that the user can learn about individual works by watching the art shows. The CG animation is produced with TVML (TV program Making Language) engine implemented on the virtual museum. However, the current problem is that it requires a lot of work for a developer to write the complicated TVML scripts manually Therefore, this time we have developed a special tool to help the developer to prepare the TVML scripts easily. With this tool, the developer can produce the TVML-based art program simply by writing out a simple scenario on an ordinary text editor. In order to design this tool, TV art programs actually broadcasted are analyzed to determine the syntax of the simple scenario. Based on the analysis, we have developed the tool with TVML engine working on the Unity game Engine. We have also used this tool to imitate the broadcasted TV program to validate its usability.

  • 23. Ashjaei, Mohammad
    et al.
    Clegg, Kester
    Corneo, Lorenzo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hawkins, Richard
    Jaradat, Omar
    Gulisano, Vincenzo Massimiliano
    Nikolakopoulos, Yiannis
    Service Level Agreements for Safe and Configurable Production Environments2018Ingår i: 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), IEEE, 2018, s. 1252-1255Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper focuses on Service Level Agreements (SLAs) for industrial applications that aim to port some of the control functionalities to the cloud. In such applications, industrial requirements should be reflected in SLAs. In this paper, we present an approach to integrate safety-related aspects of an industrial application to SLAs. We also present the approach in a use case. This is an initial attempt to enrich SLAs for industrial settings to consider safety aspects, which has not been investigated thoroughly before.

  • 24.
    Atig, Mohamed Faouzi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bollig, Benedikt
    CNRS, LSV, Paris, France.;ENS Paris Saclay, Paris, France.
    Habermehl, Peter
    CNRS, IRIF, Paris, France.;Univ Paris Diderot, Paris, France..
    Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete2017Ingår i: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 28, nr 8, s. 945-975Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We consider ordered multi-pushdown automata, a multi-stack extension of pushdown automata that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). We show that the emptiness problem for multi-pushdown automata is 2ETIME-complete. Containment in 2ETIME is shown by translating an automaton into a grammar for which we can check if the generated language is empty. The lower bound is established by simulating the behavior of an alternating Turing machine working in exponential space. We also compare ordered multi-pushdown automata with the model of bounded-phase (visibly) multi-stack pushdown automata, which do not impose an ordering on stacks, but restrict the number of alternations of pop operations on different stacks.

  • 25.
    Atig, Mohamed Faouzi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    LIAFA, CNRS and University of Paris Diderot.
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Saivasan, Prakash
    Chennai Mathematical Institute, Chennai.
    On Bounded Reachability Analysis of Shared Memory Systems2014Ingår i: {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014, New Delhi, India, 2014Konferensbidrag (Refereegranskat)
  • 26.
    Atig, Mohamed Faouzi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    LIAFA, CNRS and University of Paris Diderot.
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Saivasan, Prakash
    TU Braunschweig, Germany.
    Parity Games on Bounded Phase Multi-pushdown Systems2017Ingår i: Networked Systems: 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings / [ed] Amr El Abbadi and Benoit Garbinato, Cham, 2017, Vol. 10299, s. 272-287Konferensbidrag (Refereegranskat)
    Abstract [en]

    In this paper we address the problem of solving parity games over the configuration graphs of bounded phase multi-pushdown systems. A non-elementary decision procedure was proposed for this problem by A. Seth. In this paper, we provide a simple and inductive construction to solve this problem. We also prove a non-elementary lower-bound, answering a question posed by A. Seth.

  • 27.
    Atig, Mohamed Faouzi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    LIAFA, CNRS and University of Paris Diderot.
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Saivasan, Prakash
    TU Braunschweig, Germany.
    Verification of Asynchronous Programs with Nested Locks2017Ingår i: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India / [ed] Satya Lokam and R. Ramanujam, Dagstuhl, Germany, 2017, Vol. 93, s. 11:1-11:14Konferensbidrag (Refereegranskat)
    Abstract [en]

    In this paper, we consider asynchronous programs consisting of multiple recursive threads running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronise through a finite set of locks. In this paper, we show that the reachability problem for such class of asynchronous programs is undecidable even under the nested locking policy. We then show that the reachability problem becomes decidable (Exp-space-complete) when the locks are not allowed to be held across tasks. Finally, we show that the problem is NP-complete when in addition to previous restrictions, threads always read tasks from the same state.

  • 28.
    Atig, Mohamed Faouzi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    LIAFA, CNRS and University of Paris Diderot.
    Parlato, Gennaro
    University of Southampton.
    Context-Bounded Analysis of TSO Systems2014Ingår i: From Programs to Systems: The Systems perspective in Computing / [ed] Bensalem, S; Lakhneck, Y; Legay, A, Springer, 2014, s. 21-38Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    We address the state reachability problem in concurrent programs running over the TSO weak memory model. This problem has been shown to be decidable with non-primitive recursive complexity in the case of finite-state threads. For recursive threads this problem is undecidable. The aim of this paper is to provide under-approximate analyses for TSO systems that are decidable and have better (elementary) complexity. We propose three bounding concepts for TSO behaviors that are inspired from the concept of bounding the number of context switches introduced by Qadeer and Rehof for the sequentially consistent (SC) model. We investigate the decidability and the complexity of the state reachability problems under these three bounding concepts for TSO, and provide reduction of these problems to known reachability problems of concurrent systems under the SC semantics.

  • 29.
    Atig, Mohamed Faouzi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kumar, K. Narayan
    Saivasan, Prakash
    Acceleration in Multi-PushDown Systems2016Ingår i: Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2016, s. 698-714Konferensbidrag (Refereegranskat)
  • 30.
    Ayyalasomayajula, Kalyan Ram
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion.
    Learning based segmentation and generation methods for handwritten document images2019Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    Computerized analysis of handwritten documents is an active research area in image analysis and computer vision. The goal is to create tools that can be available for use at university libraries and for researchers in the humanities. Working with large collections of handwritten documents is very time consuming and many old books and letters remain unread for centuries. Efficient computerized methods could help researchers in history, philology and computer linguistics to cost-effectively conduct a whole new type of research based on large collections of documents. The thesis makes a contribution to this area through the development of methods based on machine learning. The passage of time degrades historical documents. Humidity, stains, heat, mold and natural aging of the materials for hundreds of years make the documents increasingly difficult to interpret. The first half of the dissertation is therefore focused on cleaning the visual information in these documents by image segmentation methods based on energy minimization and machine learning. However, machine learning algorithms learn by imitating what is expected of them. One prerequisite for these methods to work is that ground truth is available. This causes a problem for historical documents because there is a shortage of experts who can help to interpret and interpret them. The second part of the thesis is therefore about automatically creating synthetic documents that are similar to handwritten historical documents. Because they are generated from a known text, they have a given facet. The visual content of the generated historical documents includes variation in the writing style and also imitates degradation factors to make the images realistic. When machine learning is trained on synthetic images of handwritten text, with a known facet, in many cases they can even give an even better result for real historical documents.

    Delarbeten
    1. Document binarization using topological clustering guided Laplacian Energy Segmentation
    Öppna denna publikation i ny flik eller fönster >>Document binarization using topological clustering guided Laplacian Energy Segmentation
    2014 (Engelska)Ingår i: Proceedings International Conference on Frontiers in Handwriting Recognition (ICFHR), 2014, 2014, s. 523-528Konferensbidrag, Publicerat paper (Refereegranskat)
    Abstract [en]

    The current approach for text binarization proposesa clustering algorithm as a preprocessing stage toan energy-based segmentation method. It uses a clusteringalgorithm to obtain a coarse estimate of the background (BG)and foreground (FG) pixels. These estimates are used as a priorfor the source and sink points of a graph cut implementation,which is used to efficiently find the minimum energy solution ofan objective function to separate the BG and FG. The binaryimage thus obtained is used to refine the edge map that guidesthe graph cut algorithm. A final binary image is obtained byonce again performing the graph cut guided by the refinededges on a Laplacian of the image.

    Serie
    Frontiers in Handwriting Recognition, ISSN 2167-6445 ; 14
    Nyckelord
    Image Processing; Classification; Machine Learning; Graph-theoretic methods.
    Nationell ämneskategori
    Datorsystem Signalbehandling
    Forskningsämne
    Datavetenskap
    Identifikatorer
    urn:nbn:se:uu:diva-238316 (URN)10.1109/ICFHR.2014.94 (DOI)978-1-4799-4335-7 (ISBN)
    Konferens
    International Conference on Frontiers in Handwriting Recognition (ICFHR),September 1-4, 2014, Crete, Greece.
    Forskningsfinansiär
    Vetenskapsrådet, 2012-5743
    Tillgänglig från: 2014-12-11 Skapad: 2014-12-11 Senast uppdaterad: 2019-03-19Bibliografiskt granskad
    2. Historical document binarization combining semantic labeling and graph cuts
    Öppna denna publikation i ny flik eller fönster >>Historical document binarization combining semantic labeling and graph cuts
    2017 (Engelska)Ingår i: Image Analysis: Part I, Springer, 2017, s. 386-396Konferensbidrag, Publicerat paper (Refereegranskat)
    Abstract [en]

    Most data mining applications on collections of historical documents require binarization of the digitized images as a pre-processing step. Historical documents are often subjected to degradations such as parchment aging, smudges and bleed through from the other side. The text is sometimes printed, but more often handwritten. Mathematical modeling of appearance of the text, background and all kinds of degradations, is challenging. In the current work we try to tackle binarization as pixel classification problem. We first apply semantic segmentation, using fully convolutional neural networks. In order to improve the sharpness of the result, we then apply a graph cut algorithm. The labels from the semantic segmentation are used as approximate estimates of the text and background, with the probability map of background used for pruning the edges in the graph cut. The results obtained show significant improvement over the state of the art approach.

    Ort, förlag, år, upplaga, sidor
    Springer, 2017
    Serie
    Lecture Notes in Computer Science, ISSN 0302-9743 ; 10269
    Nationell ämneskategori
    Datorseende och robotik (autonoma system)
    Forskningsämne
    Datoriserad bildbehandling
    Identifikatorer
    urn:nbn:se:uu:diva-335335 (URN)10.1007/978-3-319-59126-1_32 (DOI)000454359300032 ()978-3-319-59125-4 (ISBN)
    Konferens
    SCIA 2017, June 12–14, Tromsø, Norway
    Forskningsfinansiär
    Vetenskapsrådet, 2012-5743Riksbankens Jubileumsfond, NHS14-2068:1
    Tillgänglig från: 2017-05-19 Skapad: 2017-12-04 Senast uppdaterad: 2019-03-19Bibliografiskt granskad
    3. PDNet: Semantic segmentation integrated with a primal-dual network for document binarization
    Öppna denna publikation i ny flik eller fönster >>PDNet: Semantic segmentation integrated with a primal-dual network for document binarization
    2019 (Engelska)Ingår i: Pattern Recognition Letters, ISSN 0167-8655, E-ISSN 1872-7344, Vol. 121, s. 52-60Artikel i tidskrift (Refereegranskat) Published
    Nationell ämneskategori
    Datorseende och robotik (autonoma system)
    Forskningsämne
    Datoriserad bildbehandling
    Identifikatorer
    urn:nbn:se:uu:diva-366933 (URN)10.1016/j.patrec.2018.05.011 (DOI)000459876700008 ()
    Forskningsfinansiär
    Vetenskapsrådet, 2012-5743Riksbankens Jubileumsfond, NHS14-2068:1
    Tillgänglig från: 2018-05-16 Skapad: 2018-11-27 Senast uppdaterad: 2019-04-04Bibliografiskt granskad
    4. Feature evaluation for handwritten character recognition with regressive and generative Hidden Markov Models
    Öppna denna publikation i ny flik eller fönster >>Feature evaluation for handwritten character recognition with regressive and generative Hidden Markov Models
    2016 (Engelska)Ingår i: Advances in Visual Computing: Part I, Springer, 2016, s. 278-287Konferensbidrag, Publicerat paper (Refereegranskat)
    Ort, förlag, år, upplaga, sidor
    Springer, 2016
    Serie
    Lecture Notes in Computer Science ; 10072
    Nationell ämneskategori
    Datorseende och robotik (autonoma system)
    Forskningsämne
    Datoriserad bildbehandling
    Identifikatorer
    urn:nbn:se:uu:diva-308662 (URN)10.1007/978-3-319-50835-1_26 (DOI)978-3-319-50834-4 (ISBN)
    Konferens
    ISVC 2016, December 12–14, Las Vegas, NV
    Projekt
    q2b – From Quill to Bytes
    Tillgänglig från: 2016-12-10 Skapad: 2016-11-29 Senast uppdaterad: 2019-03-19Bibliografiskt granskad
    5. CalligraphyNet: Augmenting handwriting generation with quill based stroke width
    Öppna denna publikation i ny flik eller fönster >>CalligraphyNet: Augmenting handwriting generation with quill based stroke width
    2019 (Engelska)Manuskript (preprint) (Övrigt vetenskapligt)
    Abstract [en]

    Realistic handwritten document generation garners a lot ofinterest from the document research community for its abilityto generate annotated data. In the current approach we haveused GAN-based stroke width enrichment and style transferbased refinement over generated data which result in realisticlooking handwritten document images. The GAN part of dataaugmentation transfers the stroke variation introduced by awriting instrument onto images rendered from trajectories cre-ated by tracking coordinates along the stylus movement. Thecoordinates from stylus movement are augmented with thelearned stroke width variations during the data augmentationblock. An RNN model is then trained to learn the variationalong the movement of the stylus along with the stroke varia-tions corresponding to an input sequence of characters. Thismodel is then used to generate images of words or sentencesgiven an input character string. A document image thus cre-ated is used as a mask to transfer the style variations of the inkand the parchment. The generated image can capture the colorcontent of the ink and parchment useful for creating annotated data.

    Nationell ämneskategori
    Datorsystem
    Forskningsämne
    Datoriserad bildbehandling
    Identifikatorer
    urn:nbn:se:uu:diva-379633 (URN)
    Konferens
    26th IEEE International Conference on Image Processing
    Anmärkning

    Currently under review

    Tillgänglig från: 2019-03-19 Skapad: 2019-03-19 Senast uppdaterad: 2019-04-08
  • 31.
    Ayyalasomayajula, Kalyan Ram
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion.
    Brun, Anders
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion.
    Document binarization using topological clustering guided Laplacian Energy Segmentation2014Ingår i: Proceedings International Conference on Frontiers in Handwriting Recognition (ICFHR), 2014, 2014, s. 523-528Konferensbidrag (Refereegranskat)
    Abstract [en]

    The current approach for text binarization proposesa clustering algorithm as a preprocessing stage toan energy-based segmentation method. It uses a clusteringalgorithm to obtain a coarse estimate of the background (BG)and foreground (FG) pixels. These estimates are used as a priorfor the source and sink points of a graph cut implementation,which is used to efficiently find the minimum energy solution ofan objective function to separate the BG and FG. The binaryimage thus obtained is used to refine the edge map that guidesthe graph cut algorithm. A final binary image is obtained byonce again performing the graph cut guided by the refinededges on a Laplacian of the image.

  • 32.
    Ayyalasomayajula, Kalyan Ram
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion.
    Wilkinson, Tomas
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion.
    Malmberg, Filip
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion. Uppsala universitet, Medicinska och farmaceutiska vetenskapsområdet, Medicinska fakulteten, Institutionen för kirurgiska vetenskaper, Radiologi.
    Brun, Anders
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion.
    CalligraphyNet: Augmenting handwriting generation with quill based stroke width2019Manuskript (preprint) (Övrigt vetenskapligt)
    Abstract [en]

    Realistic handwritten document generation garners a lot ofinterest from the document research community for its abilityto generate annotated data. In the current approach we haveused GAN-based stroke width enrichment and style transferbased refinement over generated data which result in realisticlooking handwritten document images. The GAN part of dataaugmentation transfers the stroke variation introduced by awriting instrument onto images rendered from trajectories cre-ated by tracking coordinates along the stylus movement. Thecoordinates from stylus movement are augmented with thelearned stroke width variations during the data augmentationblock. An RNN model is then trained to learn the variationalong the movement of the stylus along with the stroke varia-tions corresponding to an input sequence of characters. Thismodel is then used to generate images of words or sentencesgiven an input character string. A document image thus cre-ated is used as a mask to transfer the style variations of the inkand the parchment. The generated image can capture the colorcontent of the ink and parchment useful for creating annotated data.

  • 33.
    Bachelder, Steven
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Hayashi, Masaki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Nakajima, Masayuki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    4K/8K Ultra High-resolution Interactive Display System for Museum Collections: Providing Information and Context2013Konferensbidrag (Övrigt vetenskapligt)
  • 34.
    Bachelder, Steven
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Ohta, Takashi
    Tokyo University of Technology.
    Nakajima, Masayuki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Hayashi, Masaki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Kondo, Kunio
    Tokyo University of Technology.
    Andreasson, Joakim
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Böstrom, Pelle
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Khatib, Youssef
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Lau, Kakee
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Lewis, Jonas
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Research Work-Package Methodology exemplified by the Multiple Screens Project: Pinch Game using Unity for Android2013Konferensbidrag (Övrigt vetenskapligt)
  • 35.
    Badiozamany, Sobhan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datalogi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Real-time data stream clustering over sliding windows2016Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    In many applications, e.g. urban traffic monitoring, stock trading, and industrial sensor data monitoring, clustering algorithms are applied on data streams in real-time to find current patterns. Here, sliding windows are commonly used as they capture concept drift.

    Real-time clustering over sliding windows is early detection of continuously evolving clusters as soon as they occur in the stream, which requires efficient maintenance of cluster memberships that change as windows slide.

    Data stream management systems (DSMSs) provide high-level query languages for searching and analyzing streaming data. In this thesis we extend a DSMS with a real-time data stream clustering framework called Generic 2-phase Continuous Summarization framework (G2CS).  G2CS modularizes data stream clustering by taking as input clustering algorithms which are expressed in terms of a number of functions and indexing structures. G2CS supports real-time clustering by efficient window sliding mechanism and algorithm transparent indexing. A particular challenge for real-time detection of a high number of rapidly evolving clusters is efficiency of window slides for clustering algorithms where deletion of expired data is not supported, e.g. BIRCH. To that end, G2CS includes a novel window maintenance mechanism called Sliding Binary Merge (SBM). To further improve real-time sliding performance, G2CS uses generation-based multi-dimensional indexing where indexing structures suitable for the clustering algorithms can be plugged-in.

    Delarbeten
    1. Scalable ordered indexing of streaming data
    Öppna denna publikation i ny flik eller fönster >>Scalable ordered indexing of streaming data
    2012 (Engelska)Ingår i: 3rd International Workshop on Accelerating Data Management Systems using Modern Processor and Storage Architectures, 2012, s. 11-Konferensbidrag, Publicerat paper (Refereegranskat)
    Nationell ämneskategori
    Datavetenskap (datalogi)
    Identifikatorer
    urn:nbn:se:uu:diva-185068 (URN)
    Konferens
    ADMS 2012, Istanbul, Turkey
    Projekt
    eSSENCE
    Tillgänglig från: 2012-08-27 Skapad: 2012-11-19 Senast uppdaterad: 2018-01-12Bibliografiskt granskad
    2. Grand challenge: Implementation by frequently emitting parallel windows and user-defined aggregate functions
    Öppna denna publikation i ny flik eller fönster >>Grand challenge: Implementation by frequently emitting parallel windows and user-defined aggregate functions
    Visa övriga...
    2013 (Engelska)Ingår i: Proc. 7th ACM International Conference on Distributed Event-Based Systems, New York: ACM Press, 2013, s. 325-330Konferensbidrag, Publicerat paper (Refereegranskat)
    Ort, förlag, år, upplaga, sidor
    New York: ACM Press, 2013
    Nationell ämneskategori
    Datavetenskap (datalogi)
    Identifikatorer
    urn:nbn:se:uu:diva-211954 (URN)10.1145/2488222.2488284 (DOI)978-1-4503-1758-0 (ISBN)
    Externt samarbete:
    Konferens
    DEBS 2013
    Tillgänglig från: 2013-06-29 Skapad: 2013-12-03 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
    3. Distributed multi-query optimization of continuous clustering queries
    Öppna denna publikation i ny flik eller fönster >>Distributed multi-query optimization of continuous clustering queries
    2014 (Engelska)Ingår i: Proc. VLDB 2014 PhD Workshop, 2014Konferensbidrag, Publicerat paper (Refereegranskat)
    Abstract [en]

    This work addresses the problem of sharing execution plans for queries that continuously cluster streaming data to provide an evolving summary of the data stream. This is challenging since clustering is an expensive task, there might be many clustering queries running simultaneously, each continuous query has a long life time span, and the execution plans often overlap. Clustering is similar to conventional grouped aggregation but cluster formation is more expensive than group formation, which makes incremental maintenance more challenging. The goal of this work is to minimize response time of continuous clustering queries with limited resources through multi-query optimization. To that end, strategies for sharing execution plans between continuous clustering queries are investigated and the architecture of a system is outlined that optimizes the processing of multiple such queries. Since there are many clustering algorithms, the system should be extensible to easily incorporate user defined clustering algorithms.

    Nationell ämneskategori
    Datavetenskap (datalogi)
    Forskningsämne
    Datavetenskap med inriktning mot databasteknik
    Identifikatorer
    urn:nbn:se:uu:diva-302790 (URN)
    Externt samarbete:
    Konferens
    VLDB 2014
    Tillgänglig från: 2016-09-09 Skapad: 2016-09-09 Senast uppdaterad: 2018-01-10Bibliografiskt granskad
    4. Framework for real-time clustering over sliding windows
    Öppna denna publikation i ny flik eller fönster >>Framework for real-time clustering over sliding windows
    2016 (Engelska)Ingår i: Proc. 28th International Conference on Scientific and Statistical Database Management, New York: ACM Press, 2016, s. 1-13, artikel-id 19Konferensbidrag, Publicerat paper (Refereegranskat)
    Ort, förlag, år, upplaga, sidor
    New York: ACM Press, 2016
    Nationell ämneskategori
    Datavetenskap (datalogi)
    Identifikatorer
    urn:nbn:se:uu:diva-302792 (URN)10.1145/2949689.2949696 (DOI)978-1-4503-4215-5 (ISBN)
    Externt samarbete:
    Konferens
    SSDBM 2016
    Tillgänglig från: 2016-07-18 Skapad: 2016-09-09 Senast uppdaterad: 2018-01-10Bibliografiskt granskad
  • 36. Baird, Ryan
    et al.
    Gavin, Peter
    Själander, Magnus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Whalley, David
    Uh, Gang-Ryung
    Optimizing transfers of control in the static pipeline architecture2015Ingår i: Proc. 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, New York: ACM Press, 2015, s. 7-16Konferensbidrag (Refereegranskat)
    Abstract [en]

    Statically pipelined processors offer a new way to improve the performance beyond that of a traditional in-order pipeline while simultaneously reducing energy usage by enabling the compiler to control more fine-grained details of the program execution. This paper describes how a compiler can exploit the features of the static pipeline architecture to apply optimizations on transfers of control that are not possible on a conventional architecture. The optimizations presented in this paper include hoisting the target address calculations for branches, jumps, and calls out of loops, performing branch chaining between calls and jumps, hoisting the setting of return addresses out of loops, and exploiting conditional calls and returns. The benefits of performing these transfer of control optimizations include a 6.8% reduction in execution time and a 3.6% decrease in estimated energy usage.

  • 37. Bardizbanyan, Alen
    et al.
    Själander, Magnus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Whalley, David
    Larsson-Edefors, Per
    Improving data access efficiency by using context-aware loads and stores2015Ingår i: Proc. 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, New York: ACM Press, 2015, s. 27-36Konferensbidrag (Refereegranskat)
    Abstract [en]

    Memory operations have a significant impact on both performance and energy usage even when an access hits in the level-one data cache (L1 DC). Load instructions in particular affect performance as they frequently result in stalls since the register to be loaded is often referenced before the data is available in the pipeline. L1 DC accesses also impact energy usage as they typically require significantly more energy than a register file access. Despite their impact on performance and energy usage, L1 DC accesses on most processors are performed in a general fashion without regard to the context in which the load or store operation is performed. We describe a set of techniques where the compiler enhances load and store instructions so that they can be executed with fewer stalls and/or enable the L1 DC to be accessed in a more energy-efficient manner. We show that using these techniques can simultaneously achieve a 6% gain in performance and a 43% reduction in L1 DC energy usage.

  • 38.
    Basirat, Ali
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Språkvetenskapliga fakulteten, Institutionen för lingvistik och filologi.
    Principal Word Vectors2018Doktorsavhandling, monografi (Övrigt vetenskapligt)
    Abstract [en]

    Word embedding is a technique for associating the words of a language with real-valued vectors, enabling us to use algebraic methods to reason about their semantic and grammatical properties. This thesis introduces a word embedding method called principal word embedding, which makes use of principal component analysis (PCA) to train a set of word embeddings for words of a language. The principal word embedding method involves performing a PCA on a data matrix whose elements are the frequency of seeing words in different contexts. We address two challenges that arise in the application of PCA to create word embeddings. The first challenge is related to the size of the data matrix on which PCA is performed and affects the efficiency of the word embedding method. The data matrix is usually a large matrix that requires a very large amount of memory and CPU time to be processed. The second challenge is related to the distribution of word frequencies in the data matrix and affects the quality of the word embeddings. We provide an extensive study of the distribution of the elements of the data matrix and show that it is unsuitable for PCA in its unmodified form.

    We overcome the two challenges in principal word embedding by using a generalized PCA method. The problem with the size of the data matrix is mitigated by a randomized singular value decomposition (SVD) procedure, which improves the performance of PCA on the data matrix. The data distribution is reshaped by an adaptive transformation function, which makes it more suitable for PCA. These techniques, together with a weighting mechanism that generalizes many different weighting and transformation approaches used in literature, enable the principal word embedding to train high quality word embeddings in an efficient way.

    We also provide a study on how principal word embedding is connected to other word embedding methods. We compare it to a number of word embedding methods and study how the two challenges in principal word embedding are addressed in those methods. We show that the other word embedding methods are closely related to principal word embedding and, in many instances, they can be seen as special cases of it.

    The principal word embeddings are evaluated in both intrinsic and extrinsic ways. The intrinsic evaluations are directed towards the study of the distribution of word vectors. The extrinsic evaluations measure the contribution of principal word embeddings to some standard NLP tasks. The experimental results confirm that the newly proposed features of principal word embedding (i.e., the randomized SVD algorithm, the adaptive transformation function, and the weighting mechanism) are beneficial to the method and lead to significant improvements in the results. A comparison between principal word embedding and other popular word embedding methods shows that, in many instances, the proposed method is able to generate word embeddings that are better than or as good as other word embeddings while being faster than several popular word embedding methods.

  • 39. Basirat, Ali
    Random Word Vectors2019Konferensbidrag (Övrigt vetenskapligt)
  • 40. Basirat, Ali
    et al.
    Faili, Heshaam
    Bridge the gap between statistical and hand-crafted grammars2013Ingår i: Computer speech & language (Print), ISSN 0885-2308, E-ISSN 1095-8363, Vol. 27, nr 5, s. 1085-1104Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    LTAG is a rich formalism for performing NLP tasks such as semantic interpretation, parsing, machine translation and information retrieval. Depend on the specific NLP task, different kinds of LTAGs for a language may be developed. Each of these LTAGs is enriched with some specific features such as semantic representation and statistical information that make them suitable to be used in that task. The distribution of these capabilities among the LTAGs makes it difficult to get the benefit from all of them in NLP applications.

    This paper discusses a statistical model to bridge between two kinds LTAGs for a natural language in order to benefit from the capabilities of both kinds. To do so, an HMM was trained that links an elementary tree sequence of a source LTAG onto an elementary tree sequence of a target LTAG. Training was performed by using the standard HMM training algorithm called Baum–Welch. To lead the training algorithm to a better solution, the initial state of the HMM was also trained by a novel EM-based semi-supervised bootstrapping algorithm.

    The model was tested on two English LTAGs, XTAG (XTAG-Group, 2001) and MICA's grammar (Bangalore et al., 2009) as the target and source LTAGs, respectively. The empirical results confirm that the model can provide a satisfactory way for linking these LTAGs to share their capabilities together.

  • 41.
    Basirat, Ali
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Språkvetenskapliga fakulteten, Institutionen för lingvistik och filologi.
    Nivre, Joakim
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Språkvetenskapliga fakulteten, Institutionen för lingvistik och filologi.
    Greedy Universal Dependency Parsing with Right Singular Word Vectors2016Konferensbidrag (Refereegranskat)
    Abstract [en]

    A set of continuous feature vectors formed by right singular vectors of a transformed co-occurrence matrix are used with the Stanford neural dependency parser to train parsing models for a limited number of languages in the corpus of universal dependencies. We show that the feature vector can help the parser to remain greedy and be as accurate as (or even more accurate than) some other greedy and non-greedy parsers.

  • 42.
    Basirat, Ali
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Språkvetenskapliga fakulteten, Institutionen för lingvistik och filologi.
    Nivre, Joakim
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Språkvetenskapliga fakulteten, Institutionen för lingvistik och filologi.
    Real-valued syntactic word vectors2019Ingår i: Journal of experimental and theoretical artificial intelligence (Print), ISSN 0952-813X, E-ISSN 1362-3079Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We introduce a word embedding method that generates a set of real-valued word vectors from a distributional semantic space. The semantic space is built with a set of context units (words) which are selected by an entropy-based feature selection approach with respect to the certainty involved in their contextual environments. We show that the most predictive context of a target word is its preceding word. An adaptive transformation function is also introduced that reshapes the data distribution to make it suitable for dimensionality reduction techniques. The final low-dimensional word vectors are formed by the singular vectors of a matrix of transformed data. We show that the resulting word vectors are as good as other sets of word vectors generated with popular word embedding methods.

  • 43.
    Benaceur, Amel
    et al.
    INRIA Rocquencourt.
    Chilton, Chris
    University of Oxford.
    Isberner, Malte
    Technical University of Dortmund.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning2013Ingår i: SEFM 2013, 11th Int. Conf. on Software Engineering and Formal Methods / [ed] Robert M. Hierons, Mercedes G. Merayo, Mario Bravetti, Springer, 2013, s. 274-288Konferensbidrag (Refereegranskat)
    Abstract [en]

    Software systems are increasingly composed of independentlydeveloped heterogeneous components. To ensure interoperability, medi-ators are needed that coordinate actions and translate exchanged mes-sages between the components. We present a technique for automatedsynthesis of mediators, by means of a quotient operator, that is based onbehavioural models of the components and an ontological model of thedata domain. By not requiring a specification of the composed system,the method supports both off-line and run-time synthesis. The obtainedmediator is the most general component that ensures freedom of bothcommunication mismatches and deadlock in the composition. Validationof the approach is given by implementation of a prototype tool, while ap-plicability is illustrated on heterogeneous holiday booking components.

  • 44.
    Bengtsson, Ewert
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för visuell information och interaktion. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Bildanalys och människa-datorinteraktion.
    Image processing and its hardware support: Analysis vs synthesis - historical trends2017Ingår i: Image Analysis, SCIA 2017, Pt I / [ed] P Sharma, F M Bianchi, Switzerland, 2017, s. 3-14Konferensbidrag (Refereegranskat)
    Abstract [en]

    Computers can be used to handle images in two fundamen-tally dierent ways. They can be used to analyse images to obtain quan-titative data or some image understanding. And they can be used tocreate images that can be displayed through computer graphics and vi-sualization. For both of these purposes it is of interest to develop ecientways of representing, compressing and storing the images. While SCIA,the Scandinavia Conference of Image Analysis, according to its name ismainly concerned with the former aspect of images, it is interesting tonote that image analysis throughout its history has been strongly in u-enced also by developments on the visualization side. When the confer-ence series now has reached its 20th milestone it may be worth re ectingon what factors have been important in forming the development of theeld. To understand where you are it is good to know where you comefrom and it may even help you understand where you are going.

  • 45.
    Berglund, Anders
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Understanding Network Protocols. A Phenomenographic study: Invited seminar at the 2nd Annual Finnish/Baltic Sea Conference on Computer Science Education2002Övrigt (Övrigt vetenskapligt)
    Abstract [en]

    How students who participate in a project-centered, internationally distributed, university course in computer systems taught jointly by two universities understand a network protocol, TCP, is described in this paper. Insights into students' understanding are gained through an empirical phenomenographic research approach. The use of phenomenography as a research approach makes it possible to learn about computer science, as it is experienced by the students. Some aspects that indicate good learning outcomes are identified, such as being capable of understanding a protocol in different ways and of making relevant choices between the ways it could be experienced according to the context in which it appears. Based on these results a discussion on learning and teaching is developed.

  • 46.
    Berglund, Anders
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Sundin, Peter
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, För teknisk-naturvetenskapliga fakulteten gemensamma enheter, International Science Programme (ISP).
    The Development of Cooperation Between Al Baha University and Uppsala University, Sweden2014Ingår i: International Exhibition and Conference on Higher Education, Riyadh, Saudi Arabia, 2014Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    Developing new master level education is a complex task. Not only is the competence within the discipline crucial; teaching and as a consequence, learning, must also be research-focused and must aim to encourage the students to develop into independent scholars.

    In this collaborative, multi-facetted project Al Baha University, Saudi Arabia, (ABU) and Uppsala University, Sweden, (UU) work jointly to develop ABU into a leading actor in master level education with a corresponding research profile. The schools/departments take their own decisions on design and priorities of the activities. In this way the project profits from the local competencies at both sites and becomes locally situated and thus closer to the needs and expectations of the ABU staff.

    The partners entered into collaboration 2011. Among initial achievements was the common identification of the need of a bridging year for tentative master’s students, to complement the skills from the undergraduate (UG) level, and reinforce the command of English, which is a necessary tool in international education. In addition, computer science and mathematics were selected as the initial development areas.

    Within mathematics, the Department of Mathematics at UU was engaged in a discussion aiming primarily to develop the UG curriculum to match the needs of a future master programme, and secondly to develop the curriculum of a ABU master programme in mathematics to match UU standards, with the possibility in mind of student exchange targeting specific courses and thesis studies.

    Meanwhile, in the autumn 2013 a female staff member of ABU was admitted as PhD student in mathematics at UU, and has now started her second semester of full time studies.

    Within computer science (CS), the project tackles the significant challenges to encourage students, teachers and the formal university structures to embrace the ideas of Scholarship of Teaching and Learning (SoTL). The aim is to promote staff and students to broaden their perspective on what research and investigation means and to critically examine teaching and learning. As a consequence, the ways to relate to the students, the subject area, the teaching and the colleagues must be scrutinised, with the intent of finding new teaching and learning forms.

    The project implements these ideas in several ways. Currently a staff development course is given as a starting point for the project within CS. With a focus on the changes needed to implement the ideas of SoTL, the course participants make their own pedagogical development projects, and study their own practice and its outcomes using rigorous research-based methods. As a continuation, during the coming years, the two universities will run a set of workshops, mainly with a methodological focus, followed by a series of three conferences, with the first one serving the local area, and the last being an internationally recognised Institute of Electrical and Electronics Engineers (IEEE) sponsored conference. 

  • 47.
    Berglund, Emil
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Samhällsvetenskapliga fakulteten, Institutionen för informatik och media.
    Facklam, Alexander
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Samhällsvetenskapliga fakulteten, Institutionen för informatik och media.
    Framgång eller förfall?: Utvecklingen, riskerna och potentialen av BYOD2016Självständigt arbete på grundnivå (kandidatexamen), 10 poäng / 15 hpStudentuppsats (Examensarbete)
    Abstract [sv]

    Uppsatsen undersöker fenomenet Bring Your Own Device (BYOD), dess för- och nackdelar samt hur riskerna BYOD medför kan hanteras. För att uppnå detta har en litteraturstudie genomförts. Denna kompletteras av en enkätstudie på Stockholms Läns Landsting och tre intervjuer på Uppsala Kommun med målet att se hur dessa organisationer hanterar BYOD. Arbetet ger en djup insikt i BYOD olika aspekter och visar även på hur de risker som uppkommer kan hanteras.

  • 48.
    Bischoff, Sascha
    et al.
    University of Southampton, Southampton, UK.
    Sandberg, Andreas
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hansson, Andreas
    ARM, Cambridge, UK.
    Dam, Sunwoo
    ARM, Austin, TX, USA.
    Saidi, Ali
    ARM, Austin, TX, USA.
    Horsnell, Matthew
    ARM, Cambridge, UK.
    Al-Hashimi, Bashir
    University of Southampton, Southampton, UK.
    Flexible and High-Speed System-Level Performance Analysis using Hardware-Accelerated Simulation2013Konferensbidrag (Övrigt vetenskapligt)
  • 49.
    Bollig, Benedikt
    et al.
    LSV, ENS Cachan.
    Cyriac, Aiswarya
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Gastin, Paul
    LSV, ENS Cachan.
    Zeitoun, Marc
    University of Bordeaux.
    Temporal logics for concurrent recursive programs: Satisfiability and model checking2014Ingår i: Journal of Applied Logic, ISSN 1570-8683, E-ISSN 1570-8691, Vol. 12, nr 4, s. 395-416Artikel i tidskrift (Refereegranskat)
  • 50.
    Boström, Carl
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Herelius, Johan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Hugosson, Mathias
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Maleev, Sergej
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Automatic reading and interpretation of paper invoices: ADC invoice2016Självständigt arbete på grundnivå (kandidatexamen), 10 poäng / 15 hpStudentuppsats (Examensarbete)
    Abstract [sv]

    Manuell inmatning av alla långa nummer på en pappersfaktura är ett tråkigt och tidskrävande arbete. Uppgiften att skriva in alla fält från en faktura till en ordbehandlare gavs till några personer som jobbar med bokföring. Tiden mättes till ett snitt på 5 minuter. Tiden det tar och den kostnad det medför kommer att ackumuleras för företag som får regelbundna fakturor från sina leverantörer. Swedbank, och andra banker, har adresserat problemet med en mobil applikation som kan läsa och tolka nummer på en faktura via mobilkameran. Den här lösningen riktar sig mot privatpersoner och den extraherade informationen skickas direkt till banken och kan inte importeras i ett bokföringsprogram. Ett fristående program för digital läsning och tolkning av inskannade fakturor är vår lösning till företagen för detta problem.

    Det finns redan väldigt kraftfull teknologi för att tolka skriven text. Dessa tekniker användes i vårt arbete, men svårigheten i detta projekt var att implementera algoritmer för att lokalisera ett nummer och lista ut vilken bokförings referens det representerar, t.ex. OCR, IBAN etc. Detta försvåras av avsaknaden av ett generellt faktura format.

    52% av den önskade information var korrekt extraherad och nästan 95% av bokförings-detaljerna som ändras mest mellan fakturor med samma avsändare extraherades korrekt. Tiden det tog var i genomsnitt för programmet att extrahera informationen var vid dessa försök 30-40 sekunder.

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