andrewbutterfield
Academic, interested in formal semantics and verification, functional programming.
Trinity College Dublin
Pinned Repositories
ab-rtems
Realtime SMP Kernel, networking, file-systems, drivers, BSPs, samples, and testsuite.
ccs2csp
Prototype automation for translating between CCS-like and CSP-like process algebras
CCSPivsCSP
CS4098-2017
CSVprocessing
Avoidance of the need to do yak-shaving with Excel
manual-spin2tests
Small example of using Promela/SPIN to generate tests for the RTEMS operating system.
readmetest
reasonEq
RTEMS-SMP-Formal
Contains formal methods material developed for RTEMS SMP with support from ESA, and subsequent additions by student projects
UTP2
GUI-driven equational reasoning theorem prover for Unifying Theories of Programming
andrewbutterfield's Repositories
andrewbutterfield/reasonEq
andrewbutterfield/RTEMS-SMP-Formal
Contains formal methods material developed for RTEMS SMP with support from ESA, and subsequent additions by student projects
andrewbutterfield/manual-spin2tests
Small example of using Promela/SPIN to generate tests for the RTEMS operating system.
andrewbutterfield/readmetest
andrewbutterfield/ccs2csp
Prototype automation for translating between CCS-like and CSP-like process algebras
andrewbutterfield/CS4098-2017
andrewbutterfield/UTP2
GUI-driven equational reasoning theorem prover for Unifying Theories of Programming
andrewbutterfield/ab-rtems
Realtime SMP Kernel, networking, file-systems, drivers, BSPs, samples, and testsuite.
andrewbutterfield/CCSPivsCSP
andrewbutterfield/CSVprocessing
Avoidance of the need to do yak-shaving with Excel
andrewbutterfield/Forvis_RISCV-ISA-Spec
Formal specification of RISC-V Instruction Set
andrewbutterfield/FSM-check
Generic way to check if some sequence is accepted by a given finite state-machine
andrewbutterfield/hextract
Pulls out code in \begin{haskell} .. \end{haskell} from Latex documents
andrewbutterfield/literateStack
A template for using Literate Haskell (LaTeX based) with stack.
andrewbutterfield/nicesymbols
Some useful Unicode (UTF_8) and ANSI ESCapade trickery for Haskell Strings
andrewbutterfield/proglogcalc
A Programmable Logic Calculator
andrewbutterfield/reasonH
Equational reasoning for Haskell Programs
andrewbutterfield/rtems-central
Contains a partial specification of RTEMS and tools to work with the specification
andrewbutterfield/rtems-docs
Project documentation.
andrewbutterfield/smcgen
andrewbutterfield/utp-calculator
andrewbutterfield/UTPViews
A unifying theory of views
andrewbutterfield/visualize-cbn
andrewbutterfield/xv6-cs2016-3d4
xv6 OS