Browse Research and Tech Reports - Computer Science by Title

  • Nelson, Samuel C.; Kravets, Robin (2010-05-21)
    Effectively utilizing groups in delay tolerant networks (DTNs) can both improve the throughput of unicast routing protocols and open the door for a wide range of paradigms, such as anycast and multicast. Unfortunately, in ...

    application/pdf

    application/pdfPDF (173kB)
  • Meseguer, José (2018-09-16)
    Cloud computing systems are complex distributed systems whose design is challenging for two main reasons: (1) since they are distributed systems, a correct design is very hard to achieve by testing alone; and (2) cloud ...

    application/pdf

    application/pdfPDF (212kB)
  • Meredith, Patrick; Katelman, Michael; Meseguer, José; Rosu, Grigore (2010-07)
    This paper describes a formal executable semantics for the Verilog hardware description language. The goal of our formalization is to provide a concise and mathematically rigorous reference augmenting the prose of ...

    application/pdf

    application/pdfPDF (279kB)
  • 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)
  • Tominaga, Kazuto (2004-03)
    The field of studies on complex systems is becoming one of the most active research areas in computer science. Among those systems, there is a type of system that has the following characteristics: comprising a large number ...

    application/pdf

    application/pdfPDF (170kB)
  • 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)
  • Meredith, Patrick O'Neil; Hills, Mark; Rosu, Grigore (2007-07)
    This paper presents a formal definition of Scheme (based on the informal definition given in the R5RS report R5RS. The definition is purely equational, so it can be regarded as an algebraic denotational specification with ...

    application/pdf

    application/pdfPDF (234kB)
  • Ellison, Chucky M.; Rosu, Grigore (2011-11-22)
    This paper describes an executable formal semantics of C expressed using a formalism based on term rewriting. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully ...

    application/pdf

    application/pdfPDF (591kB)
  • Saxena, Manasvi; Chen, Xiaohong; Rodrigues, Nishant; Rosu, Grigore (2020)
    Hybrid Automata (HA) form the backbone of modeling systems with both discrete and continuous components. However, the semantics of HA are usually described loosely using Labeled Transition Systems (LTS), and reasoning ...

    application/pdf

    application/pdfPDF (369kB)
  • Garrido, Alejandra; Meseguer, José (2006-05)
    There is an extensive literature about refactorings of object-oriented programs, and many refactoring tools for the Java programming language. However, except for a few studies, in practice it is difficult to find precise ...

    application/pdf

    application/pdfPDF (172kB)
  • Salverda, Pierre M.; Zilles, Craig (2003-12)
    MSSP is a new execution paradigm that achieves high performance by removing correctness constraints from the critical path. A collection of concurrently executing slave processors, which are not on the critical path, check ...

    application/pdf

    application/pdfPDF (376kB)
  • Meseguer, José; Olveczky, Peter C. (2010-09-13)
    Many Distributed Real-Time Systems (DRTS), such as integrated modular avionics systems and distributed control systems in motor vehicles, are made up of a collection of components communicating asynchronously among ...

    application/pdf

    application/pdfPDF (1MB)
  • Jose Meseguer and Peter Olveczky (2009-11-12)
    Due to physical requirements, what in essence and at a higher level of abstraction is a logically synchronous real-time system has to be often realized as a distributed, asynchronous system. Getting asynchronous real-time ...

    application/pdf

    application/pdfPDF (360kB)
  • Iqbal, Shamsi T. (2008-07)
    Interruptions in the workplace are becoming increasingly prevalent due to the proliferation of proactive behavior within communication applications and collaborative practices. Interruptions caused by notifications from ...

    application/pdf

    application/pdfPDF (6MB)
  • Iqbal, Shamsi T. (2008-07)
    Interruptions in the workplace are becoming increasingly prevalent due to the proliferation of proactive behavior within communication applications and collaborative practices. Interruptions caused by notifications from ...

    application/pdf

    application/pdfPDF (6MB)
  • Chang, Tony Y.; Chilson, Neil A.; Bailey, Brian P. (2004-09)
    Knowledge about user task execution can help systems better reason about when to interrupt users. To enable recognition and forecasting of task execution, we develop a novel framework for specifying and monitoring user ...

    application/pdf

    application/pdfPDF (128kB)
  • Bailey, Brian P.; Adamczyk, Piotr D.; Chang, Tony Y.; Chilson, Neil A. (2005-04)
    Interrupting users engaged in tasks typically has negative effects on their task completion time, error rate, and affective state. Empirical research has shown that these negative effects can be mitigated by deferring ...

    application/pdf

    application/pdfPDF (275kB)