Browse Dept. of Computer Science by Subject "Model Checking"

  • Liu, Si; Ölveczky, Peter; Zhang, Min; Wang, Qi; Meseguer, José (2019)
    Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated ...

    application/pdf

    application/pdfPDF (317kB)
  • Tasharofi, Samira (2014-01-16)
    The actor model is a model of concurrent programming that consists of concurrent entities called actors. Actors communicate using asynchronous messages, and depending on the order in which they receive messages, they may ...

    application/pdf

    application/pdfPDF (925kB)
  • Liu, Si; Olveczky, Peter C.; Meseguer, José (2017)
    Mobile ad hoc networks (MANETs) are increasingly popular and deployed in a wide range of environments. However, it is challenging to formally analyze a MANET, both because there are few reasonably accurate formal models ...

    application/pdf

    application/pdfPDF (945kB)
  • Liu, Si; Olveczky, Peter C.; Rahman, Muntasir Raihan; Ganhotra, Jatin; Gupta, Indranil; Meseguer, José (2016)
    To cope with ever-increasing data sets, distributed data stores partition their data across servers. However, real-world systems usually do not provide useful transactional semantics for operations accessing multiple ...

    application/pdf

    application/pdfPDF (444kB)
  • Liu, Si; Olveczky, Peter C.; Meseguer, José (2015)
    The modeling and analysis of mobile ad hoc networks MANETs pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectionality can interact in unforeseen ...

    application/pdf

    application/pdfPDF (988kB)
  • Liu, Si; Olveczky, Peter C.; Meseguer, José (2016)
    Modeling and analyzing Mobile Ad-hoc Networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectional wireless communication ...

    application/pdf

    application/pdfPDF (2MB)
  • Liu, Si; Olveczky, Peter C.; Wang, Qi; Meseguer, José (2018)
    Walter is a distributed partially replicated data store providing Parallel Snapshot Isolation (PSI), an important consistency property that offers attractive performance while ensuring adequate guarantees for certain kinds ...

    application/pdf

    application/pdfPDF (361kB)
  • Kini, Dileep; Viswanathan, Mahesh (2015)
    LTL\GU is a fragment of linear temporal logic (LTL), where negations appear only on propositions, and formulas are built using the temporal operators X (next), F (eventually), G (always), and U (until, with the restriction ...

    application/pdf

    application/pdfPDF (368kB)
  • Korthikanti, Vijay Anand; Viswanathan, Mahesh; Kwon, YoungMin; Agha, Gul A. (2010)
    We consider Markov Decision Processes (MDPs) as transformers on probability distributions, where with respect to a scheduler that resolves nondeterminism, the MDP can be seen as exhibiting a behavior that is a sequence of ...

    application/pdf

    application/pdfPDF (404kB)