Browse Research and Tech Reports - Computer Science by Author "Moore, Brandon"

  • Kasampalis, Theodoros; Guth, Dwight; Moore, Brandon; Serbanuta, Traian Florin; Zhang, Yi; Filaretti, Daniele; Serbanuta, Virgil; Johnson, Ralph; Rosu, Grigore (2019-07-16)
    This paper proposes IELE, an LLVM-style language, together with a tool ecosystem for implementing and formally reasoning about smart contracts on the blockchain. IELE was designed by specifying its semantics formally in ...

    application/pdf

    application/pdfPDF (349kB)
  • Rosu, Grigore; Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon (2012-07)
    Abstract. This paper introduces *reachability logic*, a language-independent seven-rule proof system for deriving reachability properties of systems. The key ingredients of *reachability logic* are its sentences, which are ...

    application/pdf

    application/pdfPDF (358kB)
  • Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon; Serbanuta, Traian Florin; Rosu, Grigore (2013-11)
    This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (concurrent) languages, referred to as reachability logic. The proof system derives partial-correctness ...

    application/pdf

    application/pdfPDF (237kB)
  • Karmani, Rajesh Kumar; Madhusudan, P.; Moore, Brandon (2010-04-19)
    The goal of this paper is to build an annotation framework of thread contracts, called Accord to argue that a parallel program has no data-races, and build accompanying verification and testing tools. Accord annotations ...

    application/pdf

    application/pdfPDF (248kB)
  • Palmskog, Karl; Gligoric, Milos; Pena, Lucas; Moore, Brandon; Rosu, Grigore (2018-11-19)
    This report describes our effort to model and verify the Casper blockchain finality system in the Coq proof assistant. We outline the salient details on blockchain systems using Casper, describe previous verification ...

    application/pdf

    application/pdfPDF (424kB)