A5012214843- Distributed systems and fault tolerance
- Logic, programming, and type systems
- Formal Methods in Verification
- Parallel Computing and Optimization Techniques
- Security and Verification in Computing
- Real-Time Systems Scheduling
- Advanced Data Storage Technologies
- Logic, Reasoning, and Knowledge
- Embedded Systems Design Techniques
- Software Testing and Debugging Techniques
- Cognitive Functions and Memory
- Advanced Software Engineering Methodologies
- Software Reliability and Analysis Research
- Advanced Malware Detection Techniques
- semigroups and automata theory
- Distributed and Parallel Computing Systems
- Information and Cyber Security
- Model-Driven Software Engineering Techniques
- Advanced Algebra and Logic
- Cloud Data Security Solutions
- Computability, Logic, AI Algorithms
- Cloud Computing and Resource Management
- Scientific Computing and Data Management
- Advanced Memory and Neural Computing
- Chemical Synthesis and Analysis
University of Surrey
2018-2024
Brunel University of London
2015-2018
University of London
2017
University of Sheffield
2012-2015
Queensland University of Technology
2006-2013
The University of Queensland
2005-2013
Information Technology University
2009
ARC Centre of Excellence for Engineered Quantum Systems
2006-2007
The properties of a blockchain such as immutability, provenance, and peer-executed smart contracts could bring new level security, trust, transparency to e-learning. In this paper, we introduce our proof-of-concept blockchain-based e-learning platform developed increase in assessments facilitate curriculum personalisation higher education context. Most notably, automate issue credentials. We designed it be pedagogically neutral content-neutral order showcase the benefits back-end end users...
Formal Methods (FMs) radically improve the quality of code artefacts they help to produce. They are simple, probably accessible first-year undergraduate students and certainly second-year beyond. Nevertheless, in many cases, not part a general recommendation for course curricula, i.e., taught — yet valuable. One reason this is that teaching “Formal Methods” often confused with logic theory. This article advocates what we call FM thinking : application ideas from applied informal,...
This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that is both sound and complete respect to axiomatic Batty et al. The relies on per-thread notion observability, which allows one reason about weak program in order. On top this, we develop proof calculus invariant-based reasoning, use verify version Peterson's mutual exclusion algorithm.
Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule concurrency. In this paper, we develop a new proof calculus the C11 RAR memory model (a fragment of both relaxed and release-acquire accesses) that allows all rules compound statements, including non-interference, to remain unchanged. Our method features novel assertions specifying thread-specific views on state programs. This is combined set describe how these are affected by atomic...
In this article, we propose an approach to program verification using abstract characterisation of weak memory models. Our is based on a hierarchical axiom scheme that captures the observational properties model. particular, show it possible prove correctness with respect particular scheme, and proof suffice for any model satisfies axioms. developed weakest liberal preconditions memory. This naturally extends Hoare logic Owicki-Gries reasoning by lifting (defined over read/write events)...
Journal Article Comparing Degrees of Non-Determinism in Expression Evaluation Get access Ian J. Hayes, Hayes * 1School Information Technology and Electrical Engineering, The University Queensland, Brisbane 4072, Australia *Corresponding author: Ian.Hayes@itee.uq.edu.au Search for other works by this author on: Oxford Academic Google Scholar Alan Burns, Burns 2Department Computer Science, York, York YO10 5GH, UK Brijesh Dongol, Dongol 3Department Sheffield, Sheffield S1 4DP, Cliff B. Jones...
Abstract Weak memory presents a new challenge for program verification and has resulted in the development of variety specialised logics. For C11-style models, our previous work shown that it is possible to extend Hoare logic Owicki–Gries reasoning verify correctness weak programs. The technique introduces set high-level assertions over C11 states together with basic Hoare-style axioms atomic statements (e.g. reads/writes), but retains all other standard proof obligations compound...
The Computer Science Teachers Association (CSTA) supports and promotes the teaching of computer science other computing disciplines at K-12 educational level. During this presentation we will explore issues for teachers, ...
Abstract Non-volatile memory (NVM), aka persistent memory, is a new paradigm that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design concurrent data structures, together with associated notions correctness. In this paper, we present formal proof technique for durable linearizability , which correctness criterion extends to handle crashes and recovery context ofNVM.Our proofs are based on refinement Input/Output automata (IOA)...