Sort by: Order: Results:

Now showing items 1-5 of 5

  • Applying Formal Verification to an Open-Source Real-Time Operating System 

    Butterfield, Andrew (Springer Nature Switzerland, 2023)
    This paper describes work done using formal methods to verify parts of the RTEMS real-time operating system, as part of an activity sponsored by the European Space Agency to qualify multi-core processors for spaceflight. ...
  • Circus2CSP: A tool for model-checking circus using FDR 

    Butterfield, Andrew; Gomes, Artur Oliveira (2019)
    In this paper, we introduce Circus2CSP, a tool that automatically translates Circus into 𝐶𝑆𝑃𝑀, with an implementation based on a published manual translation scheme. This scheme includes new and modified translation ...
  • The Inner and Outer Algebras of Unified Concurrency 

    Butterfield, Andrew (2019)
    Algebras have always played a critical role in Unifying Theories of Programming, especially in their role in providing the "laws" of programming. The algebraic laws form a triad with two other forms, namely operational ...
  • Saoithín: A Theorem Prover for UTP 

    BUTTERFIELD, ANDREW (Springer, 2010)
    Saoithín is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and “programs as ...
  • Towards a model-checker for circus 

    Butterfield, Andrew; Gomes, Artur Oliveira (2019)
    Among several approaches aiming at the correctness of systems, model-checking is one technique to formally assess system models regarding their desired/undesired behavioural properties. We aim at model-checking the Open ...