uu.seUppsala universitets publikationer
Ändra sökning
Avgränsa sökresultatet
1234567 51 - 100 av 838
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.
  • 51. Armstrong, Alasdair
    et al.
    Struth, Georg
    Weber, Tjark
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Kleene Algebra2013Ingår i: Archive of Formal Proofs, ISSN 2150-914xArtikel i tidskrift (Refereegranskat)
  • 52. Armstrong, Alasdair
    et al.
    Struth, Georg
    Weber, Tjark
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL2013Ingår i: Interactive Theorem Proving: ITP 2013, Springer Berlin/Heidelberg, 2013, s. 197-212Konferensbidrag (Refereegranskat)
    Abstract [en]

    Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while-programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.

  • 53. Armstrong, Alasdair
    et al.
    Struth, Georg
    Weber, Tjark
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Programming and automating mathematics in the Tarski-Kleene hierarchy2014Ingår i: Journal of Logical and Algebraic Methods in Programming, ISSN 2352-2208, Vol. 83, nr 2, s. 87-102Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how models can be programmed, including sets of traces and paths, languages, binary relations, max-plus and min-plus algebras, matrices, formal power series. For relation algebras we discuss primarily proof automation in a comprehensive library and present an advanced formalisation example. 

  • 54.
    Aronis, Stavros
    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.
    Effective Techniques for Stateless Model Checking2018Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    Stateless model checking is a technique for testing and verifying concurrent programs, based on exploring the different ways in which operations executed by the processes of a concurrent program can be scheduled. The goal of the technique is to expose all behaviours that can be a result of scheduling non-determinism. As the number of possible schedulings is huge, however, techniques that reduce the number of schedulings that must be explored to achieve verification have been developed. Dynamic partial order reduction (DPOR) is a prominent such technique.

    This dissertation presents a number of improvements to dynamic partial order reduction that significantly increase the effectiveness of stateless model checking. Central among these improvements are the Source and Optimal DPOR algorithms (and the theoretical framework behind them) and a technique that allows the observability of the interference of operations to be used in dynamic partial order reduction. Each of these techniques can exponentially decrease the number of schedulings that need to be explored to verify a concurrent program. The dissertation also presents a simple bounding technique that is compatible with DPOR algorithms and effective for finding bugs in concurrent programs, if the number of schedulings is too big to make full verification possible in a reasonable amount of time, even when the improved algorithms are used.

    All improvements have been implemented in Concuerror, a tool for applying stateless model checking to Erlang programs. In order to increase the effectiveness of the tool, the interference of the high-level operations of the Erlang/OTP implementation is examined, classified and precisely characterized. Aspects of the implementation of the tool are also described. Finally, a use case is presented, showing how Concuerror was used to find bugs and verify key correctness properties in repair techniques for the CORFU chain replication protocol.

    Delarbeten
    1. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
    Öppna denna publikation i ny flik eller fönster >>Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
    2017 (Engelska)Ingår i: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 64, nr 4, artikel-id 25Artikel i tidskrift (Refereegranskat) Published
    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.

    Ort, förlag, år, upplaga, sidor
    Association for Computing Machinery (ACM), 2017
    Nationell ämneskategori
    Programvaruteknik
    Identifikatorer
    urn:nbn:se:uu:diva-331842 (URN)10.1145/3073408 (DOI)000410615900002 ()
    Projekt
    UPMARCRELEASE
    Forskningsfinansiär
    EU, FP7, Sjunde ramprogrammet, 287510Vetenskapsrådet
    Tillgänglig från: 2017-10-18 Skapad: 2017-10-18 Senast uppdaterad: 2018-01-13Bibliografiskt granskad
    2. The shared-memory interferences of Erlang/OTP built-ins
    Öppna denna publikation i ny flik eller fönster >>The shared-memory interferences of Erlang/OTP built-ins
    2017 (Engelska)Ingår i: Proceedings Of The 16Th Acm Sigplan International Workshop On Erlang (Erlang '17) / [ed] Chechina, N.; Fritchie, SL., New York: Association for Computing Machinery (ACM), 2017, s. 43-54Konferensbidrag, Publicerat paper (Refereegranskat)
    Abstract [en]

    Erlang is a concurrent functional language based on the actor modelof concurrency. In the purest form of this model, actors are realizedby processes that do not share memory and communicate witheach other exclusively via message passing. Erlang comes quiteclose to this model, as message passing is the primary form of interprocesscommunication and each process has its own memoryarea that is managed by the process itself. For this reason, Erlangis often referred to as implementing “shared nothing” concurrency.Although this is a convenient abstraction, in reality Erlang’s mainimplementation, the Erlang/OTP system, comes with a large numberof built-in operations that access memory which is shared byprocesses. In this paper, we categorize these built-ins, and characterizethe interferences between them that can result in observabledifferences of program behaviour when these built-ins are usedin a concurrent setting. The paper is complemented by a publiclyavailable suite of more than one hundred small Erlang programsthat demonstrate the racing behaviour of these built-ins.

    Ort, förlag, år, upplaga, sidor
    New York: Association for Computing Machinery (ACM), 2017
    Nyckelord
    Actors, BEAM, Concuerror, Erlang, Scheduling nondeterminism
    Nationell ämneskategori
    Programvaruteknik
    Identifikatorer
    urn:nbn:se:uu:diva-331840 (URN)10.1145/3123569.3123573 (DOI)000426922100005 ()978-1-4503-5179-9 (ISBN)
    Konferens
    16th ACM SIGPLAN International Workshop on Erlang (Erlang), Sep 08, 2017 , Oxford, England.
    Projekt
    UPMARC
    Forskningsfinansiär
    Vetenskapsrådet
    Tillgänglig från: 2017-10-18 Skapad: 2017-10-18 Senast uppdaterad: 2018-07-03Bibliografiskt granskad
    3. Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
    Öppna denna publikation i ny flik eller fönster >>Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
    2017 (Engelska)Konferensbidrag, Publicerat paper (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.

    Ort, förlag, år, upplaga, sidor
    Cham: Springer, 2017
    Serie
    Lecture Notes in Computer Science ; 10510
    Nationell ämneskategori
    Datorsystem Programvaruteknik
    Identifikatorer
    urn:nbn:se:uu:diva-331836 (URN)10.1007/978-3-319-66845-1_15 (DOI)978-3-319-66844-4 (ISBN)978-3-319-66845-1 (ISBN)
    Konferens
    Integrated Formal Methods. IFM 2017
    Projekt
    UPMARC
    Tillgänglig från: 2017-10-18 Skapad: 2017-10-18 Senast uppdaterad: 2018-01-13Bibliografiskt granskad
    4. Optimal dynamic partial order reduction with observers
    Öppna denna publikation i ny flik eller fönster >>Optimal dynamic partial order reduction with observers
    2018 (Engelska)Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2018, Vol. 10806, s. 229-248Konferensbidrag, Publicerat paper (Refereegranskat)
    Abstract [en]

    Dynamic partial order reduction (DPOR) algorithms are used in stateless model checking (SMC) to combat the combinatorial explosion in the number of schedulings that need to be explored to guarantee soundness. The most effective of them, the Optimal DPOR algorithm, is optimal in the sense that it explores only one scheduling per Mazurkiewicz trace. In this paper, we enhance DPOR with the notion of observability, which makes dependencies between operations conditional on the existence of future operations, called observers. Observers naturally lead to a lazy construction of dependencies. This requires significant changes in the core of POR algorithms (and Optimal DPOR in particular), but also makes the resulting algorithm, Optimal DPOR with Observers, super-optimal in the sense that it explores exponentially less schedulings than Mazurkiewicz traces in some cases. We argue that observers come naturally in many concurrency models, and demonstrate the performance benefits that Optimal DPOR with Observers achieves in both an SMC tool for shared memory concurrency and a tool for concurrency via message passing, using both synthetic and actual programs as benchmarks.

    Ort, förlag, år, upplaga, sidor
    Springer, 2018
    Serie
    Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10806
    Nationell ämneskategori
    Datavetenskap (datalogi)
    Identifikatorer
    urn:nbn:se:uu:diva-333508 (URN)10.1007/978-3-319-89963-3 _ 14 (DOI)000445822600014 ()978-3-319-89962-6 (ISBN)978-3-319-89963-3 (ISBN)
    Konferens
    TACAS 2018, April 14–20, Thessaloniki, Greece.
    Projekt
    UPMARC
    Forskningsfinansiär
    Vetenskapsrådet
    Tillgänglig från: 2018-04-14 Skapad: 2017-11-21 Senast uppdaterad: 2019-01-07Bibliografiskt granskad
  • 55.
    Aronis, Stavros
    et al.
    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.
    Lång, Magnus
    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 reduction with observers2018Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2018, Vol. 10806, s. 229-248Konferensbidrag (Refereegranskat)
    Abstract [en]

    Dynamic partial order reduction (DPOR) algorithms are used in stateless model checking (SMC) to combat the combinatorial explosion in the number of schedulings that need to be explored to guarantee soundness. The most effective of them, the Optimal DPOR algorithm, is optimal in the sense that it explores only one scheduling per Mazurkiewicz trace. In this paper, we enhance DPOR with the notion of observability, which makes dependencies between operations conditional on the existence of future operations, called observers. Observers naturally lead to a lazy construction of dependencies. This requires significant changes in the core of POR algorithms (and Optimal DPOR in particular), but also makes the resulting algorithm, Optimal DPOR with Observers, super-optimal in the sense that it explores exponentially less schedulings than Mazurkiewicz traces in some cases. We argue that observers come naturally in many concurrency models, and demonstrate the performance benefits that Optimal DPOR with Observers achieves in both an SMC tool for shared memory concurrency and a tool for concurrency via message passing, using both synthetic and actual programs as benchmarks.

  • 56.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Papaspyrou, Nikolaos
    Roukounaki, Katerina
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Tsiouris, Yiannis
    Venetis, Ioannis E.
    A scalability benchmark suite for Erlang/OTP2012Ingår i: Proc. 11th ACM SIGPLAN Workshop on Erlang, New York: ACM Press, 2012, s. 33-42Konferensbidrag (Refereegranskat)
    Abstract [en]

    Programming language implementers rely heavily on benchmarking for measuring and understanding performance of algorithms, architectural designs, and trade-offs between alternative implementations of compilers, runtime systems, and virtual machine components. Given this fact, it seems a bit ironic that it is often more difficult to come up with a good benchmark suite than a good implementation of a programming language.

    This paper presents the main aspects of the design and the current status of bencherl, a publicly available scalability benchmark suite for applications written in Erlang. In contrast to other benchmark suites, which are usually designed to report a particular performance point, our benchmark suite aims to assess scalability, i.e., help developers to study a set of performance points that show how an application's performance changes when additional resources (e.g., CPU cores, schedulers, etc.) are added. We describe the scalability dimensions that the suite aims to examine and present its infrastructure and current set of benchmarks. We also report some limited set of performance results in order to show the capabilities of our suite.

  • 57.
    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.
    On using Erlang for parallelization: Experience from parallelizing Dialyzer2013Ingår i: Trends in Functional Programming, Springer Berlin/Heidelberg, 2013, s. 295-310Konferensbidrag (Refereegranskat)
  • 58.
    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.
    The shared-memory interferences of Erlang/OTP built-ins2017Ingår i: Proceedings Of The 16Th Acm Sigplan International Workshop On Erlang (Erlang '17) / [ed] Chechina, N.; Fritchie, SL., New York: Association for Computing Machinery (ACM), 2017, s. 43-54Konferensbidrag (Refereegranskat)
    Abstract [en]

    Erlang is a concurrent functional language based on the actor modelof concurrency. In the purest form of this model, actors are realizedby processes that do not share memory and communicate witheach other exclusively via message passing. Erlang comes quiteclose to this model, as message passing is the primary form of interprocesscommunication and each process has its own memoryarea that is managed by the process itself. For this reason, Erlangis often referred to as implementing “shared nothing” concurrency.Although this is a convenient abstraction, in reality Erlang’s mainimplementation, the Erlang/OTP system, comes with a large numberof built-in operations that access memory which is shared byprocesses. In this paper, we categorize these built-ins, and characterizethe interferences between them that can result in observabledifferences of program behaviour when these built-ins are usedin a concurrent setting. The paper is complemented by a publiclyavailable suite of more than one hundred small Erlang programsthat demonstrate the racing behaviour of these built-ins.

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

  • 60.
    Asai, Kenichi
    et al.
    Ochanomizu Univ, Tokyo 112, Japan..
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. NTUA, Athens, Greece..
    Selected and extended papers from Partial Evaluation and Program Manipulation 2015 (PEPM ' 15)2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 137, s. 1-1Artikel i tidskrift (Övrigt vetenskapligt)
  • 61.
    Ashcroft, Michael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    An Introduction To Bayesian Networks in Systems and Control2012Konferensbidrag (Refereegranskat)
  • 62.
    Ashcroft, Michael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Bayesian Networks in Business Analytics2012Ingår i: 2012 FEDERATED CONFERENCE ON COMPUTER SCIENCE AND INFORMATION SYSTEMS (FEDCSIS), 2012, s. 955-961Konferensbidrag (Refereegranskat)
  • 63.
    Ashcroft, Michael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Performing Decision-Theoretic Inference in Bayesian Network Ensemble Models2013Ingår i: Twelfth Scandinavian Conference on Artificial Intelligence / [ed] Jaeger, M; Nielsen, TD; Viappiani, P, 2013, Vol. 257, s. 25-34Konferensbidrag (Refereegranskat)
    Abstract [en]

    The purpose of this paper is to present a simple extension to an existing inference algorithm on influence diagrams (i.e. decision theoretic extensions to Bayesian networks) that permits these algorithms to be applied to ensemble models. The extension, though simple, is important because of the power and robustness that such ensemble models provide [1]. This paper is intended principally as a 'recipe' that can be used even by those unfamiliar with the algorithms extended. Accordingly, I present the algorithms that the original contribution builds upon in full, though references are given to less concise renditions. Those familiar with these algorithms are invited to skip the elucidation. The consequence is a useful paper with more background and less original input than usual.

  • 64.
    Ashcroft, Michael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Using Bayesian networks in business analytics: Overview and short case study2012Ingår i: Business Informatics, ISSN 1507-3858, Vol. 3, nr 25Artikel i tidskrift (Refereegranskat)
  • 65.
    Ashcroft, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Fisher, Ali
    Univ Vienna, VORTEX, Vienna, Austria.
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Omer, Enghin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Prucha, Nico
    Kings Coll London, ICSR, London, England.
    Detecting jihadist messages on twitter2015Ingår i: Proc. 5th European Intelligence and Security Informatics Conference, IEEE Computer Society, 2015, s. 161-164Konferensbidrag (Refereegranskat)
    Abstract [en]

    Jihadist groups such as ISIS are spreading online propaganda using various forms of social media such as Twitter and YouTube. One of the most common approaches to stop these groups is to suspend accounts that spread propaganda when they are discovered. This approach requires that human analysts manually read and analyze an enormous amount of information on social media. In this work we make a first attempt to automatically detect messages released by jihadist groups on Twitter. We use a machine learning approach that classifies a tweet as containing material that is supporting jihadists groups or not. Even tough our results are preliminary and more tests needs to be carried out we believe that results indicate that an automated approach to aid analysts in their work with detecting radical content on social media is a promising way forward. It should be noted that an automatic approach to detect radical content should only be used as a support tool for human analysts in their work.

  • 66.
    Ashcroft, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Johansson, Fredrik
    Swedish Def Res Agcy FOI, Stockholm, Sweden..
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Swedish Def Res Agcy FOI, Stockholm, Sweden..
    Shrestha, Amendra
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Multi-domain alias matching using machine learning2016Ingår i: Proc. 3rd European Network Intelligence Conference, IEEE, 2016, s. 77-84Konferensbidrag (Refereegranskat)
    Abstract [en]

    We describe a methodology for linking aliases belonging to the same individual based on a user's writing style (stylometric features extracted from the user generated content) and her time patterns (time-based features extracted from the publishing times of the user generated content). While most previous research on social media identity linkage relies on matching usernames, our methodology can also be used for users who actively try to choose dissimilar usernames when creating their aliases. In our experiments on a discussion forum dataset and a Twitter dataset, we evaluate the performance of three different classifiers. We use the best classifier (AdaBoost) to evaluate how well it works on different datasets using different features. Experiments show that combining stylometric and time based features yield good results on our synthetic datasets and a small-scale evaluation on real-world blog data confirm these results, yielding a precision over 95%. The use of emotion-related and Twitter-related features yield no significant impact on the results.

  • 67.
    Ashcroft, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. FOI, Stockholm, Sweden.
    Meyer, Maxime
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    A step towards detecting online grooming: Identifying adults pretending to be children2015Ingår i: Proc. 5th European Intelligence and Security Informatics Conference, IEEE Computer Society, 2015, s. 98-104Konferensbidrag (Refereegranskat)
    Abstract [en]

    Online grooming is a major problem in todays society where more and more time is spent online. To become friends and establish a relationship with their young victims in online communities, groomers often pretend to be children. In this paper we describe an approach that can be used to detect if an adult is pretending to be a child in a chat room conversation. The approach involves a two step process wherein authors are first classified as being children or adults, and then each child is being examined and false children distinguished from genuine children. Our results show that even if it is hard to separate ordinary adults from children in chat logs it is possible to distinguish real children from adults pretending to be children with a high accuracy. In this paper we will discuss the accuracy of the methods proposed, as well as the features that were important in their success. We believe that this work is an important step towards automated analysis of chat room conversation to detect and possible attempts of grooming. Our approach where we use text analysis to distinguish adults who are pretending to be children from actual children could be used to inform children about the true age of the person that they are communicating. This would be a step towards making the Internet more secure for young children and eliminate grooming.

  • 68.
    Ashcroft, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Meyer, Maxime
    Are You Really a Child?: A Machine Learning Approach To Protect Children from Online Grooming2015Ingår i: Proc. National Symposium on Technology and Methodology for Security and Crisis Management: TAMSEC 2015, 2015Konferensbidrag (Refereegranskat)
    Abstract [en]

    Online grooming and sexual abuse of children is a major threat towards the security of todays society where more and more time is spent online. To become friends and establish a relationship with their young victims in online communities, groomers often pretend to be children. In this work we describe an approach that can be used to detect if an adult is pretending to be a child in a chat room conversation. Our results show that even if it is hard to separate ordinary adults from children in chat logs it is possible to distinguish real children from adults pretending to be children with a high accuracy.

  • 69.
    Ashcroft, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Magnani, Matteo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Vega, Davide
    Univ Bologna, Bologna, Italy..
    Montesi, Danilo
    Univ Bologna, Bologna, Italy..
    Rossi, Luca
    IT Univ Copenhagen, Copenhagen, Denmark..
    Multilayer Analysis of Online Illicit Marketplaces2016Ingår i: 2016 European Intelligence And Security Informatics Conference (EISIC) / [ed] Brynielsson, J Johansson, F, IEEE , 2016, s. 199-199Konferensbidrag (Refereegranskat)
  • 70. Atzmueller, Martin
    et al.
    Gaito, Sabrina
    Interdonato, Roberto
    Kanawati, Rushed
    Largeron, Christine
    Magnani, Matteo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sala, Alessandra
    International Workshop on Mining Attributed Networks (MATNET 2018) Chairs’ Welcome2018Övrigt (Övrigt vetenskapligt)
  • 71.
    Axelson, Roland
    et al.
    Department of Computer Science, University of Munich.
    Lange, Martin
    Department of Computer Science, University of Munich.
    Somla, Rafal
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    The Complexity of Model Checking Higher-order Fixpoint Logic2007Ingår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 3, nr 2:7, s. 1-33Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the modal μ-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of programs that are not expressible in the modal μ-calculus. This paper provides complexity results for its model checking problem. In particular we consider those fragments of HFL built by using only types of bounded order k and arity m. We establish k-fold exponential time completeness for model checking each such fragment. For the upper bound we use fixpoint elimination to obtain reachability games that are singly-exponential in the size of the formula and k-fold exponential in the size of the underlying transition system. These games can be solved in deterministic linear time. As a simple consequence, we obtain an exponential time upper bound on the expression complexity of each such fragment. The lower bound is established by a reduction from the word problem for alternating (k-1)-fold exponential space bounded Turing Machines. Since there are fixed machines of that type whose word problems are already hard with respect to k-fold exponential time, we obtain, as a corollary, k-fold exponential time completeness for the data complexity of our fragments of HFL, provided m exceeds 3. This also yields a hierarchy result in expressive power.

  • 72.
    Badiozamany, Sobhan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Distributed multi-query optimization of continuous clustering queries2014Ingår i: Proc. VLDB 2014 PhD Workshop, 2014Konferensbidrag (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.

  • 73.
    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
  • 74.
    Badiozamany, Sobhan
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Melander, Lars
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Truong, Thanh
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Xu, Cheng
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Risch, Tore
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Grand challenge: Implementation by frequently emitting parallel windows and user-defined aggregate functions2013Ingår i: Proc. 7th ACM International Conference on Distributed Event-Based Systems, New York: ACM Press, 2013, s. 325-330Konferensbidrag (Refereegranskat)
  • 75.
    Badiozamany, Sobhan
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Orsborn, Kjell
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Risch, Tore
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Framework for real-time clustering over sliding windows2016Ingår i: Proc. 28th International Conference on Scientific and Statistical Database Management, New York: ACM Press, 2016, s. 1-13, artikel-id 19Konferensbidrag (Refereegranskat)
  • 76.
    Badiozamany, Sobhan
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Risch, Tore
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Scalable ordered indexing of streaming data2012Ingår i: 3rd International Workshop on Accelerating Data Management Systems using Modern Processor and Storage Architectures, 2012, s. 11-Konferensbidrag (Refereegranskat)
  • 77. Balck, Kenneth
    et al.
    Grinchtein, Olga
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Model-based protocol log generation for testing a telecommunication test harness using CLP2014Ingår i: Proc. 17th Conference on Design, Automation and Test in Europe, Piscataway, NJ: IEEE , 2014Konferensbidrag (Refereegranskat)
  • 78. Balck, Kenneth
    et al.
    Grinchtein, Olga
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Model-based protocol log generation for testing a telecommunication test harness using CLP2014Ingår i: 2014 DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION (DATE), 2014Konferensbidrag (Refereegranskat)
    Abstract [en]

    Within telecommunications development it is vital to have frameworks and systems to replay complicated scenarios on equipment under test, often there are not enough available scenarios. In this paper we study the problem of testing a test harness, which replays scenarios and analyses protocol logs for the Public Warning System service, which is a part of the Long Term Evolution (LTE) 4G standard. Protocol logs are sequences of messages with timestamps; and are generated by different mobile network entities. In our case study we focus on user equipment protocol logs. In order to test the test harness we require that logs have both incorrect and correct behaviour. It is easy to collect logs from real system runs, but these logs do not show much variation in the behaviour of system under test. We present an approach where we use constraint logic programming (CLP) for both modelling and test generation, where each test case is a protocol log. In this case study, we uncovered previously unknown faults in the test harness.

  • 79.
    Baldamus, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    A Fully Abstract Encoding of the pi-Calculus with Data Terms2005Ingår i: Proceedings of ICALP 2005 / [ed] Luís Caires; Guiseppe F. Italiano; Luís Monteiro; Catuscia Palamidessi; Moti Yung, Berlin: Springer , 2005, s. 1202-1213Konferensbidrag (Refereegranskat)
    Abstract [en]

    The π-calculus with data terms (πT) extends the pure π-calculus by data constructors and destructors and allows data to be transmitted between agents. It has long been known how to encode such data types in π, but until now it has been open how to make the encoding fully abstract, meaning that two encodings (in π) are semantically equivalent precisely when the original πT agents are semantically equivalent. We present a new type of encoding and prove it to be fully abstract with respect to may-testing equivalence. To our knowledge this is the first result of its kind, for any calculus enriched with data terms. It has particular importance when representing security properties since attackers can be regarded as may-test observers. Full abstraction proves that it does not matter whether such observers are formulated in π or πT, both are equally expressive in this respect. The technical new idea consists of achieving full abstraction by encoding data as table entries rather than active processes, and using a firewalled central integrity manager to ensure data security.

  • 80.
    Baldamus, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Spi Calculus Translated to pi-Calculus Preserving May-Testing2003Rapport (Övrigt vetenskapligt)
    Abstract [en]

    We present a concise and natural encoding of the spi-calculus into the more basic pi-calculus and establish its correctness with respect to a formal notion of testing. This is particularly relevant for security protocols modelled in spi since the tests can be viewed as adversaries. The translation has been implemented in a prototype tool. As a consequence, protocols can be described in the spi calculus and analysed with the emerging flora of tools already available for pi. The translation also entails a more detailed operational understanding of spi since high level constructs like encryption are encoded in a well known lower level. The formal correctness proof is nontrivial and interesting in its own; so called context bisimulations and new techniques for compositionality make the proof simpler and more concise.

  • 81.
    Baldamus, Michael
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Spi Calculus Translated to pi-Calculus Preserving May-Tests2004Ingår i: Proceedings of LICS 2004: Logic in Computer Science, Los Alamitos, Calif: IEEE Computer Society, 2004, s. 22-31Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present a concise and natural encoding of the spi-calculus into the more basic pi-calculus and establish its correctness with respect to a formal notion of testing. This is particularly relevant for security protocols modelled in spi since the tests can be viewed as adversaries. The translation has been implemented in a prototype tool. As a consequence, protocols can be described in the spi calculus and analysed with the emerging flora of tools already available for pi. The translation also entails a more detailed operational understanding of spi since high level constructs like encryption are encoded in a well known lower level. The formal correctness proof is nontrivial and interesting in its own; so called context bisimulations and new techniques for compositionality make the proof simpler and more concise.

  • 82.
    Baltopoulos, Ioannis G.
    et al.
    University of Cambridge.
    Borgström, Johannes
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Gordon, Andrew D.
    Microsoft Research, Cambridge.
    Maintaining Database Integrity with Refinement Types2011Ingår i: ECOOP 2011 – Object-Oriented Programming / [ed] Mezini, Mira, Berlin: Springer-Verlag , 2011, s. 484-509Konferensbidrag (Refereegranskat)
    Abstract [en]

    Taking advantage of recent advances in automated theorem proving, we present a new method for determining whether database transactions preserve integrity constraints. We consider check constraints and referential-integrity constraints—extracted from SQL table declarations—and application-level in- variants expressed as formulas of first-order logic. Our motivation is to use static analysis of database transactions at development time, to catch bugs early, or during deployment, to allow only integrity-preserving stored procedures to be accepted. We work in the setting of a functional multi-tier language, where functional code is compiled to SQL that queries and updates a relational database. We use refinement types to track constraints on data and the underlying database. Our analysis uses a refinement-type checker, which relies on recent highly efficient SMT algorithms to check proof obligations. Our method is based on a list-processing semantics for an SQL fragment within the functional language, and is illustrated by a series of examples. 

  • 83. Bartocci, Ezio
    et al.
    Beyer, Dirk
    Black, Paul E.
    Fedyukovich, Grigory
    Garavel, Hubert
    Hartmanns, Arnd
    Huisman, Marieke
    Kordon, Fabrice
    Nagele, Julian
    Sighireanu, Mihaela
    Steffen, Bernhard
    Suda, Martin
    Sutcliffe, Geoff
    Weber, Tjark
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Yamada, Akihisa
    TOOLympics 2019: An overview of competitions in formal methods2019Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: 25 years of TACAS, Part III, Springer, 2019, s. 3-24Konferensbidrag (Refereegranskat)
  • 84. Bartoletti, Massimo
    et al.
    Bocchi, LauraHenrio, LudovicKnight, SophiaUppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Proc. 10th Interaction and Concurrency Experience2017Proceedings (redaktörskap) (Refereegranskat)
  • 85. Bartoletti, Massimo
    et al.
    Henrio, LudovicKnight, SophiaUppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.Torres Vieira, Hugo
    Proc. 9th Interaction and Concurrency Experience2016Proceedings (redaktörskap) (Refereegranskat)
  • 86.
    Bartoletti, Massimo
    et al.
    Univ Cagliari, Cagliari, Italy.
    Henrio, Ludovic
    Univ Cote Azur, CNRS, I3S, Nice, France.
    Knight, Sophia
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Vieira, Hugo Torres
    IMT Sch Adv Studies Lucca, Lucca, Italy.
    Preface for the special issue on Interaction and Concurrency Experience 20162018Ingår i: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 98, s. 26-26Artikel i tidskrift (Övrigt vetenskapligt)
  • 87. Basin, David
    et al.
    Deville, Yves
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Hamfelt, Andreas
    Humanistisk-samhällsvetenskapliga vetenskapsområdet, Samhällsvetenskapliga fakulteten, Institutionen för informationsvetenskap. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Fischer Nilsson, Jorgen
    Synthesis of Programs in Computational Logic2004Ingår i: Program Development in Computational Logic, Springer-Verlag , 2004, s. 30-65Kapitel i bok, del av antologi (Refereegranskat)
  • 88. Beldiceanu, Nicolas
    et al.
    Carlsson, Mats
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Francisco Rodríguez, María Andreína
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Linking prefixes and suffixes for constraints encoded using automata with accumulators2014Ingår i: Principles and Practice of Constraint Programming: CP 2014, Springer, 2014, s. 142-157Konferensbidrag (Refereegranskat)
  • 89. Beldiceanu, Nicolas
    et al.
    Carlsson, Mats
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Lorca, Xavier
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Petit, Thierry
    Prud'homme, Charles
    A modelling pearl with sortedness constraints2015Ingår i: Global Conference on Artificial Intelligence: GCAI 2015, Manchester, UK: Cool Press , 2015, s. 27-41Konferensbidrag (Refereegranskat)
  • 90. Beldiceanu, Nicolas
    et al.
    Carlsson, Mats
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    On matrices, automata, and double counting2010Ingår i: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Berlin: Springer-Verlag , 2010, s. 10-24Konferensbidrag (Refereegranskat)
  • 91. Beldiceanu, Nicolas
    et al.
    Carlsson, Mats
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    On matrices, automata, and double counting in constraint programming2013Ingår i: Constraints, ISSN 1383-7133, E-ISSN 1572-9354, Vol. 18, nr 1, s. 108-140Artikel i tidskrift (Refereegranskat)
  • 92. Beldiceanu, Nicolas
    et al.
    Carlsson, Mats
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    On the reification of global constraints2013Ingår i: Constraints, ISSN 1383-7133, E-ISSN 1572-9354, Vol. 18, nr 1, s. 1-6Artikel i tidskrift (Refereegranskat)
  • 93. Beldiceanu, Nicolas
    et al.
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Biologiska sektionen, Institutionen för cell- och molekylärbiologi, Centrum för bioinformatik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Lorca, Xavier
    Combining tree partitioning, precedence, and incomparability constraints2008Ingår i: Constraints, ISSN 1383-7133, E-ISSN 1572-9354, Vol. 13, nr 4, s. 459-489Artikel i tidskrift (Refereegranskat)
  • 94. Beldiceanu, Nicolas
    et al.
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. CSD.
    Lorca, Xavier
    Combining Tree Partitioning, Precedence, Incomparability, and Degree Constraints, with an Application to Phylogenetic and Ordered-Path Problems2006Rapport (Övrigt vetenskapligt)
  • 95. Beldiceanu, Nicolas
    et al.
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. CSD.
    Lorca, Xavier
    Partitionnement de graphes par des arbres sous contraintes de degré2006Ingår i: Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC'06), 2006Konferensbidrag (Refereegranskat)
  • 96. Beldiceanu, Nicolas
    et al.
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Centrum för bioinformatik. Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Lorca, Xavier
    The tree constraint2005Ingår i: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems: Second International Conference, CPAIOR 2005, Proceedings, 2005, s. 64-78Konferensbidrag (Refereegranskat)
  • 97. Beldiceanu, Nicolas
    et al.
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Monette, Jean-Noël
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Simonis, Helmut
    Toward sustainable development in constraint programming2014Ingår i: Constraints, ISSN 1383-7133, E-ISSN 1572-9354, Vol. 19, nr 2, s. 139-149Artikel i tidskrift (Refereegranskat)
  • 98. Beldiceanu, Nicolas
    et al.
    Flener, Pierre
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pearson, Justin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Van Hentenryck, Pascal
    Propagating regular counting constraints2014Ingår i: Proc. 28th AAAI Conference on Artificial Intelligence: Volume 4, Palo Alto, CA: AAAI Press, 2014, s. 2616-2622Konferensbidrag (Refereegranskat)
  • 99.
    Bengtson, Jesper
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Bhargavan, Karthikeyan
    Fournet, Cédric
    Gordon, Andrew D.
    Maffeis, Sergio
    Refinement types for secure implementations2011Ingår i: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 33, nr 2, s. 8:1-45Artikel i tidskrift (Refereegranskat)
  • 100.
    Bengtson, Jesper
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Johansson, Magnus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Psi-calculi: a framework for mobile processes with nominal data and logic2011Ingår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 7, nr 1, s. 11-Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The framework of psi-calculi extends the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Psi-calculi can capture the same phenomena as other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions.

    We provide ample comparisons to related calculi and discuss a few significant applications. Our labelled operational semantics and definition of bisimulation is straightforward, without a  structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic properties of psi-calculi, all of which have been checked in the interactive theorem prover Isabelle. Expressiveness of psi-calculi significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.

1234567 51 - 100 av 838
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