Dept. of Computer Science

 

The Department of Computer Science is recognized throughout the world as a leader in education and research. The department and its graduates have long been at the forefront of modern computing beginning with the ILLIAC in 1952, and continuing with the creation of Mosaic, the first graphic web browser, through the most recent Internet era.

Browse Sub-communities

Browse Collections of Items

Recent AdditionsRSS feed

  • Matching Logic Explained 
    Chen, Xiaohong; Lucanu, Dorel; Rosu, Grigore (2020-07)
    Matching logic was recently proposed as a unifying logic for specifying and reasoning about static structure and dynamic behavior of programs. In matching logic, patterns and specifications are used to uniformly represent ...

    application/pdf

    application/pdfPDF (868kB)
  • Initial Algebra Semantics in Matching Logic 
    Chen, Xiaohong; Lucanu, Dorel; Rosu, Grigore (2020-07)
    Matching logic is a unifying foundational logic for defining formal programming language semantics, which adopts a minimalist design with few primitive constructs that are enough to express all properties within a variety ...

    application/pdf

    application/pdfPDF (808kB)
  • Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification 
    Meseguer, Jose; Skeirik, Stephen (2020-07-16)
    We present an inductive inference system for proving validity of formulas in the initial algebra T[E] of an order-sorted equational theory E with 17 inference rules, where only 6 of them require user interaction, ...

    application/pdf

    application/pdfPDF (244kB)
  • End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract 
    Park, Daejun; Zhang, Yi; Rosu, Grigore (2020)
    We report our experience in the formal verification of the deposit smart contract, whose correctness is critical for the security of Ethereum 2.0, a new Proof-of-Stake protocol for the Ethereum blockchain. The deposit ...

    application/pdf

    application/pdfPDF (762kB)
  • Formal semantics of hybrid automata 
    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)

Community Statistics