uu.seUppsala universitets publikationer
Ändra sökning
Avgränsa sökresultatet
1234567 1 - 50 av 350
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 Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Cyriac, Aiswarya
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Chennai Math Inst, Madras, Tamil Nadu, India..
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Data Communicating Processes with Unreliable Channels2016Ingår i: Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), 2016, s. 166-175Konferensbidrag (Refereegranskat)
    Abstract [en]

    We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.

  • 3.
    Abdulla, Parosh A.
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Univ Genoa, DIBRIS, Genoa, Italy..
    Parameterized verification2016Ingår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, nr 5, s. 469-473Artikel i tidskrift (Övrigt vetenskapligt)
    Abstract [en]

    The goal of parameterized verification is to prove the correctness of a system specification regardless of the number of its components. The problem is of interest in several different areas: verification of hardware design, multithreaded programs, distributed systems, and communication protocols. The problem is undecidable in general. Solutions for restricted classes of systems and properties have been studied in areas like theorem proving, model checking, automata and logic, process algebra, and constraint solving. In this introduction to the special issue, dedicated to a selection of works from the Parameterized Verification workshop PV '14 and PV '15, we survey some of the works developed in this research area.

  • 4.
    Abdulla, Parosh A.
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Univ Genoa, Genoa, Italy..
    Montali, Marco
    Free Univ Bolzano, Bolzano, Italy..
    Well Structured Transition Systems with History2015Ingår i: Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180, E-ISSN 2075-2180, nr 193, s. 115-128Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We propose a formal model of concurrent systems in which the history of a computation is explicitly represented as a collection of events that provide a view of a sequence of configurations. In our model events generated by transitions become part of the system configurations leading to operational semantics with historical data. This model allows us to formalize what is usually done in symbolic verification algorithms. Indeed, search algorithms often use meta-information, e.g., names of fired transitions, selected processes, etc., to reconstruct (error) traces from symbolic state exploration. The other interesting point of the proposed model is related to a possible new application of the theory of well-structured transition systems (wsts). In our setting wsts theory can be applied to formally extend the class of properties that can be verified using coverability to take into consideration (ordered and unordered) historical data. This can be done by using different types of representation of collections of events and by combining them with wsts by using closure properties of well-quasi orderings.

  • 5.
    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.
    Comparing source sets and persistent sets for partial order reduction2017Ingår i: Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Springer, 2017, s. 516-536Kapitel i bok, del av antologi (Övrigt vetenskapligt)
    Abstract [en]

    Partial order reduction has traditionally been based on persistent sets, ample sets, stubborn sets, or variants thereof. Recently, we have presented a strengthening of this foundation, using source sets instead of persistent/ample/stubborn sets. Source sets subsume persistent sets and are often smaller than persistent sets. We introduced source sets as a basis for Dynamic Partial Order Reduction (DPOR), in a framework which assumes that processes are deterministic and that all program executions are finite. In this paper, show how to use source sets for partial order reduction in a framework which does not impose these restrictions. We also compare source sets with persistent sets, providing some insights into conditions under which source sets and persistent sets do or do not differ.

  • 6.
    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, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction2017Ingår i: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 64, nr 4, artikel-id 25Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Stateless model checking is a powerful method for program verification that, 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), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, 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, that replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple-to-implement algorithm, called source-DPOR. Subsequently, we enhance this algorithm with a novel mechanism, called wakeup trees, that allows the resulting algorithm, called optimal-DPOR, to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, for example, via locks. Finally, we discuss tradeoffs of the source-and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs, while the source-DPOR algorithm is at the core of a publicly available stateless model checking tool for C/pthread programs running on machines with relaxed memory models. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.

  • 7.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aiswarya, C.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Montali, Marco
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Complexity of reachability for data-aware dynamic systems2018Ingår i: Proc. 18th International Conference on Application of Concurrency to System Design, IEEE Computer Society, 2018, s. 11-20Konferensbidrag (Refereegranskat)
  • 8.
    Abdulla, Parosh Aziz
    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.
    Atig, Mohamed Faouzi
    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.
    Leonardsson, Carl
    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.
    Stateless model checking for TSO and PSO2015Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015, Springer Berlin/Heidelberg, 2015, s. 353-367Konferensbidrag (Refereegranskat)
  • 9.
    Abdulla, Parosh Aziz
    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.
    Atig, Mohamed Faouzi
    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.
    Leonardsson, Carl
    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.
    Stateless model checking for TSO and PSO2017Ingår i: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 54, nr 8, s. 789-818Artikel i tidskrift (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.
    Bouajjani, Ahmed
    Ngo, Tuan Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    A load-buffer semantics for total store ordering2018Ingår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 14, nr 1, artikel-id 9Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. 

    In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.

  • 11.
    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.

  • 12.
    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)
  • 13.
    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.
    The benefits of duality in verifying concurrent programs under TSO2016Ingår i: 27th International Conference on Concurrency Theory: CONCUR 2016, Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2016, s. 5:1-15Konferensbidrag (Refereegranskat)
    Abstract [en]

    We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes.

    In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.

  • 14.
    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)
  • 15.
    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.
    Cederberg, Jonathan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Modi, Subham
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Saini, Gaurav
    MPass: An efficient tool for the analysis of message-passing programs2015Ingår i: Formal Aspects of Component Software, Springer, 2015, s. 198-206Konferensbidrag (Refereegranskat)
  • 16.
    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
    Bui, Phi Diep
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holik, Lukas
    Rezine, Ahmed
    Rümmer, Philipp
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Trau: SMT solver for string constraints2018Ingår i: The eighteenth in a series of conferences on the theory and applications of formal methods in hardware and system verification (FMCAD 2018), 2018Konferensbidrag (Refereegranskat)
  • 17.
    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
    Bui, Phi Diep
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holık, Lukas
    Rezine, Ahmed
    Rümmer, Philipp
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Flatten and Conquer: A Framework for Efficient Analysis of String Constraints2017Ingår i: SIGPLAN notices, ISSN 0362-1340, E-ISSN 1558-1160, Vol. 52, nr 6, s. 602-617Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.

  • 18.
    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
    Holík, Lukás
    Rezine, Ahmed
    Rümmer, Philipp
    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.
    Norn: An SMT solver for string constraints2015Ingår i: Computer Aided Verification: Part I, Springer, 2015, s. 462-469Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.

  • 19.
    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.
    Ciobanu, Radu
    Mayr, Richard
    Totzke, Patrick
    Universal safety for timed Petri nets is PSPACE-complete2018Ingår i: 29th International Conference on Concurrency Theory, Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2018, s. 6:1-15Konferensbidrag (Refereegranskat)
  • 20.
    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.
    Ganjei, Zeinab
    Rezine, Ahmed
    Zhu, Yunyun
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verification of Cache Coherence Protocols wrt. Trace Filters2015Ingår i: Proc. 15th Conference on Formal Methods in Computer-Aided Design, Piscataway, NJ: IEEE , 2015, s. 9-16Konferensbidrag (Refereegranskat)
  • 21.
    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.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Leonardsson, Carl
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stateless model checking for POWER2016Ingår i: Computer Aided Verification: Part II, Springer, 2016, s. 134-156Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.

  • 22.
    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.
    Kara, Ahmet
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verification of buffered dynamic register automata2015Ingår i: Networked Systems: NETYS 2015, Springer, 2015, s. 15-31Konferensbidrag (Refereegranskat)
  • 23.
    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.
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Leonardsson, Carl
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Ros, Alberto
    Zhu, Yunyun
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Fencing programs with self-invalidation and self-downgrade2016Ingår i: Formal Techniques for Distributed Objects, Components, and Systems, Springer, 2016, s. 19-35Konferensbidrag (Refereegranskat)
  • 24.
    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.
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Leonardsson, Carl
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Ros, Alberto
    Zhu, Yunyun
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Mending fences with self-invalidation and self-downgrade2018Ingår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 14, nr 1, artikel-id 6Artikel i tidskrift (Refereegranskat)
  • 25.
    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.
    Krishna, Shankara Narayanan
    Perfect timed communication is hard2018Ingår i: Formal Modeling and Analysis of Timed Systems, Springer, 2018, s. 91-107Konferensbidrag (Refereegranskat)
  • 26.
    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.
    Krishna, Shankara Narayanan
    Vaidya, Shaan
    Verification of timed asynchronous programs2018Ingår i: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2018, Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2018, s. 8:1-16Konferensbidrag (Refereegranskat)
  • 27.
    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.
    Lång, Magnus
    Ngo, Tuan Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Precise and sound automatic fence insertion procedure under PSO2015Ingår i: Networked Systems: NETYS 2015, Springer, 2015, s. 32-47Konferensbidrag (Refereegranskat)
    Abstract [en]

    We give a sound and complete procedure for fence insertion for concurrent finite-state programs running under the PSO memory model. This model allows ''write to read'' and ''write-to-write'' relaxations corresponding to the addition of an unbounded store buffers between processors and the main memory. We introduce a novel machine model, called the Hierarchical Single-Buffer (HSB) semantics, and show that the reachability problem for a program under PSO can be reduced to the reachability problem under HSB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence insertion procedure. The procedure infers automatically a minimal set of fences that ensure correctness of the program. We have implemented a prototype and run it successfully on all standard benchmarks, together with several challenging examples.

  • 28.
    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.
    Meyer, Roland
    Salehi, Mehdi Seyed
    What's decidable about availability languages?2015Ingår i: Proc. 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science, Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2015, s. 192-205Konferensbidrag (Refereegranskat)
  • 29.
    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.
    Ngo, Tuan-Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO2015Ingår i: Programming Languages and Systems: ESOP 2015, Springer Berlin/Heidelberg, 2015, s. 308-332Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present a method for automatic fence insertion in concurrent programs running under weak memory models that provides the best known trade-off between efficiency and optimality. On the one hand, the method can efficiently handle complex aspects of program behaviors such as unbounded buffers and large numbers of processes. On the other hand, it is able to find small sets of fences needed for ensuring correctness of the program. To this end, we propose a novel notion of correctness, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving (SC) semantics. We instantiate our framework for the Total Store Ordering (TSO) memory model, and give an algorithm that reduces the fence insertion problem under TSO to the reachability problem for programs running under SC. Furthermore, we provide an abstraction scheme that substantially increases scalability to large numbers of processes. Based on our method, we have implemented a tool and run it successfully on a wide range benchmarks.

  • 30.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Univ Genoa, I-16126 Genoa, Italy..
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala Univ, Uppsala, Sweden..
    Sangnier, Arnaud
    Univ Paris Diderot, CNRS, LIAFA, Paris, France..
    Traverso, Riccardo
    FBK, Trento, Italy..
    Parameterized verification of time-sensitive models of ad hoc network protocols2016Ingår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 612, s. 1-22Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.

  • 31.
    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.

  • 32.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    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.
    Lengál, Ondrej
    Trinh, Cong Quy
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Verification of heap manipulating programs with ordered data by extended forest automata2016Ingår i: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, nr 4, s. 357-385Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.

  • 33.
    Abdulla, Parosh Aziz
    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.
    Fragment abstraction for concurrent shape analysis2018Ingår i: Programming Languages and Systems, Springer, 2018, s. 442-471Konferensbidrag (Refereegranskat)
  • 34.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sistla, A. Prasad
    Talupur, Muralidhar
    Model checking parameterized systems2018Ingår i: Handbook of Model Checking, Springer, 2018, s. 685-725Kapitel i bok, del av antologi (Refereegranskat)
  • 35.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Ciobanu, Radu
    Univ Edinburgh, Edinburgh, Midlothian, Scotland..
    Mayr, Richard
    Univ Edinburgh, Edinburgh, Midlothian, Scotland..
    Sangnier, Arnaud
    Univ Paris Diderot, CNRS, LIAFA, Sorbonne Paris Cite, Paris, France..
    Sproston, Jeremy
    Univ Turin, Turin, Italy..
    Qualitative Analysis of VASS-Induced MDPs2016Ingår i: Foundations Of Software Science And Computation Structures (FOSSACS 2016) / [ed] Jacobs, B Loding, C, 2016, s. 319-334Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almostsurely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).

  • 36.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delporte, Carole
    Univ Paris Diderot, Paris, France.
    Special Issue on NETYS'20162019Ingår i: Computing, ISSN 0010-485X, E-ISSN 1436-5057, Vol. 101, nr 1, s. 1-2Artikel i tidskrift (Övrigt vetenskapligt)
  • 37.
    Abdulla, Parosh
    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
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Brno Univ Technol, Brno, Czech Republic..
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rezine, Ahmed
    Linköping Univ, Linköping, Sweden..
    An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures2017Ingår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 19, nr 5, s. 549-563Artikel i tidskrift (Refereegranskat)
    Abstract [en]

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

  • 38.
    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.

  • 39.
    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.
    Guan, Nan
    Northeastern Univ, Shenyang, Liaoning, Peoples R China..
    Mohaqeqi, Morteza
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Wang, Yi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Towards a Tool: TIMES-Pro for Modeling, Analysis, Simulation and Implementation of Cyber-Physical Systems2017Ingår i: MODELS, ALGORITHMS, LOGICS AND TOOLS: ESSAYS DEDICATED TO KIM GULDSTRAND LARSEN ON THE OCCASION OF HIS 60TH BIRTHDAY / [ed] Aceto, L Bacci, G Bacci, G Ingolfsdottir, A Legay, A Mardare, R, SPRINGER INTERNATIONAL PUBLISHING AG , 2017, s. 623-639Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider a Cyber-Physical System (CPS) as a network of components that are either physical plants with continuous behaviors or discrete controllers. To build CPS's in a systematic manner, the TIMES-Pro tool is designed to support modeling, analysis and code generation for real-time simulation and final deployment. In this paper, we present our decisions in designing the modeling language, the tool architecture and features of TIMES-Pro, and also a case study to demonstrate its applicability.

  • 40.
    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)
  • 41.
    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, Avdelningen för datorteknik.
    Wang, Yi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Worst-Case Cause-Effect Reaction Latency in Systems with Non-Blocking Communication2019Ingår i: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE, 2019, s. 1625-1630Konferensbidrag (Refereegranskat)
    Abstract [en]

    In real-time embedded systems, a system functionality is often implemented using a data-flow chain over a set of communicating tasks. A critical non-functional requirement in such systems is to restrict the amount of time, i.e. cause-effect latency, for an input to impact its corresponding output. The problem of estimating the worst-case cause-effect latency is well-studied in the context of blocking inter-task communication. Recent research results show that non-blocking communication preserving functional semantics is critical for the model-based design of dynamically updatable systems. In this paper, we study the worst-case cause-effect reaction latency estimation problem in the context of non-blocking inter-task communication. We present a computationally efficient algorithm that tightly over-approximates the exact worst-case reaction latency in cause-effect data-flow chains.

  • 42.
    Abdullah, Jakaria
    et al.
    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.
    Synthesis of Ada code from graph-based task models2017Ingår i: Proc. 32nd ACM Symposium on Applied Computing, New York: ACM Press, 2017, s. 1467-1472Konferensbidrag (Refereegranskat)
  • 43.
    Abdullah, Syed Md Jakaria
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Lampka, Kai
    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.
    Improving performance by monitoring while maintaining worst-case guarantees2016Ingår i: Proc. 19th Conference on Design, Automation and Test in Europe, Piscataway, NJ: IEEE, 2016, s. 257-260Konferensbidrag (Refereegranskat)
  • 44. Ahlgren, Bengt
    et al.
    Hidell, Markus
    Ngai, Edith C.-H.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Internet of Things for smart cities: Interoperability and open data2016Ingår i: IEEE Internet Computing, ISSN 1089-7801, E-ISSN 1941-0131, Vol. 20, nr 6, s. 52-56Artikel i tidskrift (Refereegranskat)
  • 45.
    Akrami, Nazar
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Samhällsvetenskapliga fakulteten, Institutionen för psykologi.
    Shrestha, Amendra
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Berggren, Mathias
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Samhällsvetenskapliga fakulteten, Institutionen för psykologi.
    Kaati, Lisa
    Swedish Defense Research Agency.
    Obaidi, Milan
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Samhällsvetenskapliga fakulteten, Institutionen för psykologi.
    Cohen, Katie
    Swedish Defense Research Agency.
    Assessment of risk in written communication: Introducing the Profile Risk Assessment Tool (PRAT)2018Rapport (Övrigt vetenskapligt)
  • 46.
    Alghamdi, Fayiq
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Nylén, Aletta
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pears, Arnold
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Changing the Educational Epistemologies of Computer Science Teachers: A Case Study of the Kingdom of Saudi Arabia2018Ingår i: 2018 IEEE Frontiers in Education Conference (FIE), Piscataway, NJ: IEEE, 2018Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper explores the attitudes of Computer Sci- ence (CS) teachers in the Kingdom of Saudi Arabia (KSA) who are confronted by the Saudi Teaching Competencies Standards (STCS). The STCS is a response to a substantial need to develop both subject-specific pedagogical ability as well as teachers subject area knowledge. The Ministry of Education in the KSA is encouraging teachers to improve their practices to achieve the new quality requirements for education. This paper presents the results of an investigation of CS teachers’ views on educational belief changes in the KSA schools. The paper addresses how and why CS teachers adopt new educational beliefs in their teaching. The paper presents the results of the investigation of the CS teachers views on educational belief changes in the KSA schools and the STCS policy document guidelines. Research in the area of changing educational epistemology in teaching CS identifies six factors that influence teachers, these are personal pedagogical beliefs, peer learning, curriculum, self-directed learning, student feedback and the STCS. A mixed method study approach was adopted in this work. Content analysis has been applied to the interview transcript and thematic coding analysis to the government policy document (STCS). The results provide a valuable case study in the KSA and emphasize the weak relationship between educational epistemology change and the STCS norms. The findings show that the STCS should provide stronger guidance for CS teachers to keep changing beliefs in teaching CS. The STCS should offer supporting official resources to CS teachers to help them in changing their beliefs in regard to teaching CS.

  • 47.
    Alghamdi, Fayiq
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pears, Arnold
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Nylén, Aletta
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Computer science teachers perspectives on competencies: A case study in the Kingdom of Saudi Arabia2018Ingår i: Informatics in Schools. Fundamentals of Computer Science and Software Engineering, Springer, 2018, s. 129-140Konferensbidrag (Refereegranskat)
  • 48.
    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.

  • 49.
    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.

  • 50.
    Amanda, Nordhamn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Design and implementation of a demonstrator for a Bluetooth Low Energy based fleet service system for hand-held gardening and forestry products2016Självständigt arbete på avancerad nivå (yrkesexamen), 20 poäng / 30 hpStudentuppsats (Examensarbete)
    Abstract [en]

    Today, large companies specialized in forestry or park maintenance may own very large machine fleets consisting of hundreds of trimmers, chainsaws and brush cutters. Husqvarna Group, whose core business lies within high-end forestry and gardening products, has noticed that such companies tend to buy cheaper, low quality forestry and gardening products. The reason is thought to be that the companies lack a proper overview of the service status and utilization levels of their machines, leading to insufficient service, causing machines to break prematurely and making it hard to motivate investments in more expensive products. Hence, the companies usually adopt a consumerist approach, and buy cheaper products that are thrown away upon breaking.

    To make their products more attractive to machine park owners, Husqvarna want to explore the area of Internet of Things and equip their machines with sensing and communication capabilities. Collected data could be used to provide an overview of machine usage and service requirements to the machine parks owners, and could make it easier for machine park owners to dimension their machine fleet. In addition to this, a machine monitoring system where specific operator behavior can be tracked could enable identification of operators who consistently mistreat their machines by, for example, running the machine engine at non-optimal rotation speeds.

    In this master's thesis, a demonstrator of the working principle of a Bluetooth Low Energy based Fleet Service System is designed and implemented, complete with an evaluation of if received signal strength indicator (RSSI) is a good enough distance estimator to determine which operator operates a certain machine. 

    Experiments carried out indicate that while RSSI is not a good estimator of distance, it could be used to determine the operator in closest proximity given that operators are not allowed to work closer than within a 10 m radius of each other.

1234567 1 - 50 av 350
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