Ian J. Hayes

CoRR, 2024

Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures.

[BibT_eX]

[DOI]

CoRR, 2024

Data reification in a concurrent rely-guarantee algebra.

[BibT_eX]

[DOI]

CoRR, 2024

Reasoning about distributive laws in a concurrent refinement algebra.

[BibT_eX]

[DOI]

CoRR, 2024

Restructuring a Concurrent Refinement Algebra.

[BibT_eX]

[DOI]

Nasos Evangelou-Oost

Proceedings of the Relational and Algebraic Methods in Computer Science, 2024

2023

Differential Testing of a Verification Framework for Compiler Optimizations (Case Study).

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, 2023

Using scylindric algebra to support local variables in rely/guarantee concurrency.

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE/ACM International Conference on Formal Methods in Software Engineering, 2023

Verifying Compiler Optimisations - (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2023

Trace Models of Concurrent Valuation Algebras.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2023

Verifying Term Graph Optimizations using Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

Specifying and Reasoning About Shared-Variable Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Theories of Programming and Formal Methods, 2023

Contextuality in Distributed Systems.

[BibT_eX]

[DOI]

Nasos Evangelou-Oost

Callum Bannister

Proceedings of the Relational and Algebraic Methods in Computer Science, 2023

2022

Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper).

[BibT_eX]

[DOI]

CoRR, 2022

2021

Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style.

[BibT_eX]

[DOI]

Patrick A. Meiring

CoRR, 2021

A Formal Semantics of the GraalVM Intermediate Representation.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2021

Software Specification.

[BibT_eX]

[DOI]

Steve King

Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

2020

Deriving Specifications of Control Programs for Cyber Physical Systems.

[BibT_eX]

[DOI]

Alan Burns

Comput. J., 2020

2019

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2019

Handling localisation in rely/guarantee concurrency: An algebraic approach.

[BibT_eX]

[DOI]

CoRR, 2019

Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

Cylindric Kleene Lattices for Program Construction.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018

Some Challenges of Specifying Concurrent Program Components.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 18th Refinement Workshop, 2018

Encoding fairness in a synchronous concurrent program algebra: extended version with proofs.

[BibT_eX]

[DOI]

CoRR, 2018

Type Capabilities for Object-Oriented Programming Languages.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2018

Engineering a Theory of Concurrent Programming.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2018

Encoding Fairness in a Synchronous Concurrent Program Algebra.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017

Designing a semantic model for a wide-spectrum language with concurrency.

[BibT_eX]

[DOI]

Robert J. Colvin

Formal Aspects Comput., 2017

Relational Convolution, Generalised Modalities and Incidence Algebras.

[BibT_eX]

[DOI]

CoRR, 2017

Partial Semigroups and Convolution Algebras.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

A Guide to Rely/Guarantee Thinking.

[BibT_eX]

[DOI]

Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

Capabilities for Java: Secure Access to Resources.

[BibT_eX]

[DOI]

Xi Wu

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016

Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2016

Possible values: Exploring a concept for concurrency.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2016

Generalised rely-guarantee concurrency: an algebraic foundation.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2016

Concurrent Refinement Algebra and Rely Quotients.

[BibT_eX]

[DOI]

Julian Fell

Andrius Velykis

Arch. Formal Proofs, 2016

An Algebra of Synchronous Atomic Steps.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

2015

Balancing expressiveness in formal approaches to concurrency.

[BibT_eX]

[DOI]

Robert J. Colvin

Formal Aspects Comput., 2015

2014

Deriving real-time action systems with multiple time bands using algebraic reasoning.

[BibT_eX]

[DOI]

John Derrick

Sci. Comput. Program., 2014

Reasoning about goal-directed real-time teleo-reactive programs.

[BibT_eX]

[DOI]

Peter J. Robinson

Formal Aspects Comput., 2014

Convolution, Separation and Concurrency.

[BibT_eX]

[DOI]

CoRR, 2014

Invariants, Well-Founded Statements and Real-Time Program Algebra.

[BibT_eX]

[DOI]

Proceedings of the FM 2014: Formal Methods, 2014

2013

Linking Unifying Theories of Program refinement.

[BibT_eX]

[DOI]

Steve Dunne

Sci. Comput. Program., 2013

Deriving real-time action systems in a sampling logic.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2013

Comparing Degrees of Non-Determinism in Expression Evaluation.

[BibT_eX]

[DOI]

Comput. J., 2013

Visuocode: A software development environment that supports spatial navigation and composition.

[BibT_eX]

[DOI]

Daniel R. Bradley

Proceedings of the 2013 First IEEE Working Conference on Software Visualization (VISSOFT), 2013

Path-Sensitive Data Flow Analysis Simplified.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Safety-Critical Systems, 2013

2012

Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic.

[BibT_eX]

[DOI]

John Derrick

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Deriving Real-Time Action Systems Controllers from Multiscale System Specifications.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 9th International Conference, 2012

Integrated Operational Semantics: Small-Step, Big-Step and Multi-step.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

Towards an Algebra for Real-Time Programs.

[BibT_eX]

[DOI]

Proceedings of the Relational and Algebraic Methods in Computer Science, 2012

2011

A semantics for Behavior Trees using CSP with specification commands.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2011

Structural operational semantics through context-dependent behaviour.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2011

Approximating Idealised Real-Time Specifications Using Time Bands.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Model-Driven Web Form Validation with UML and OCL.

[BibT_eX]

[DOI]

Proceedings of the Current Trends in Web Engineering, 2011

2010

A timeband framework for modelling real-time systems.

[BibT_eX]

[DOI]

Alan Burns

Real Time Syst., 2010

Integrating Requirements: The Behavior Tree Philosophy.

[BibT_eX]

[DOI]

Kirsten Winter

Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, 2010

Unifying Theories of Programming That Distinguish Nontermination and Abort.

[BibT_eX]

[DOI]

Steve Dunne

Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

Compositional Action System Derivation Using Enforced Properties.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

Invariants and Well-Foundedness in Program Algebra.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2010

2009

Dynamically Detecting Faults via Integrity Constraints.

[BibT_eX]

[DOI]

Proceedings of the Methods, 2009

CSP with Hierarchical State.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation.

[BibT_eX]

[DOI]

Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009

2008

Calculating modules in contextual logic program refinement.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2008

Algebraic reasoning for probabilistic action systems and while-loops.

[BibT_eX]

[DOI]

Acta Informatica, 2008

Reasoning about Loops in Total and General Correctness.

[BibT_eX]

[DOI]

Steve Dunne

Andy Galloway

Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

Towards reasoning about teleo-reactive programs for robust real-time systems.

[BibT_eX]

[DOI]

Proceedings of the SERENE 2008, 2008

Probabilistic Choice in Refinement Algebra.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

2007

Procedures and parameters in the real-time program refinement calculus.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2007

Deriving Specifications for Systems That Are Connected to the Physical World.

[BibT_eX]

[DOI]

Michael A. Jackson

Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006

Termination of Real-Time Programs: Definitely, Definitely Not, or Maybe.

[BibT_eX]

[DOI]

Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

Continuous Action System Refinement.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 8th International Conference, 2006

Reasoning Algebraically About Probabilistic Loops.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2006

2005

A theory for execution-time derivation in real-time programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Integration of generic program analysis tools into a software development environment.

[BibT_eX]

[DOI]

Erica Glynn

Anthony MacDonald

Proceedings of the Computer Science 2005, 2005

2004

Developing Logic Programs from Specifications Using Stepwise Refinement.

[BibT_eX]

[DOI]

Proceedings of the Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, 2004

An Environment for Building a System out of its Requirements.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 2004

Towards Platform-Independent Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the 15th Australian Software Engineering Conference (ASWEC 2004), 2004

2003

Linear Approximation of Execution-Time Constraints.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2003

Formal Semantics for Program Paths.

[BibT_eX]

[DOI]

Proceedings of the Computing: the Australasian Theory Symposiumm, 2003

Reasoning about Deadlines in Concurrent Real-Time Programs.

[BibT_eX]

[DOI]

Sibylle Peuker

Proceedings of the 17th International Parallel and Distributed Processing Symposium (IPDPS 2003), 2003

Programs as Paths: An Approach to Timing Constraint Analysis.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2003

Determining the Specification of a Control System from That of Its Environment.

[BibT_eX]

[DOI]

Michael A. Jackson

Proceedings of the FME 2003: Formal Methods, 2003

2002

A refinement calculus for logic programs.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2002

Reasoning about real-time repetitions: terminating and nonterminating.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2002

An Introduction to Real-Time Object-Z.

[BibT_eX]

[DOI]

Graeme Smith

Formal Aspects Comput., 2002

Don't Care Non-determinism in Logic Program Refinement.

[BibT_eX]

[DOI]

Proceedings of the Computing: the Australasian Theory Symposium, 2002

Reasoning about Timeouts.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 6th International Conference, 2002

Refinement of Higher-Order Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Tranformation, 2002

Towards a Refinement Calculus for Concurrent Real-Time Programs.

[BibT_eX]

[DOI]

Sibylle Peuker

Proceedings of the Formal Methods and Software Engineering, 2002

Refining Object-Oriented Invariants and Dynamic Constraints.

[BibT_eX]

[DOI]

Jamie Shield

Proceedings of the 9th Asia-Pacific Software Engineering Conference (APSEC 2002), 2002

The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming.

[BibT_eX]

[DOI]

Proceedings of the Applications and Theory of Petri Nets 2002, 2002

Translating Refined Logic Programs to Mercury.

[BibT_eX]

[DOI]

Proceedings of the Computer Science 2002, 2002

2001

Using Theory Interpretation to Mechanise the Reals in a Theorem Prover.

[BibT_eX]

[DOI]

Jamie Shield

David A. Carrington

Proceedings of the Computing: The Australasian Theory Symposium, 2001

Semantic characterisation of dead control-flow paths.

[BibT_eX]

[DOI]

IEE Proc. Softw., 2001

A sequential real-time refinement calculus.

[BibT_eX]

[DOI]

Acta Informatica, 2001

Refinement Calculus for Logic Programming in Isabelle/HOL.

[BibT_eX]

[DOI]

David Hemer

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

2000

Reasoning about Non-terminating Loops Using Deadline Commands.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 5th International Conference, 2000

A Technique for Modular Logic Program Refinement.

[BibT_eX]

[DOI]

Proceedings of the Logic Based Program Synthesis and Transformation, 2000

Modular Logic Program Refinement.

[BibT_eX]

Proceedings of the Extended Abstracts of the 10th International Workshop on Logic-based Program Synthesis and Transformation, 2000

Structuring Real-Time Object-Z Specifications.

[BibT_eX]

[DOI]

Graeme Smith

Proceedings of the Integrated Formal Methods, Second International Conference, 2000

Real-Time Program Refinement Using Auxiliary Variables.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2000

Reasoning about real-time programs using idle-invariant assertions.

[BibT_eX]

[DOI]

Proceedings of the 7th Asia-Pacific Software Engineering Conference (APSEC 2000), 2000

Refining Logic Programs Using Types.

[BibT_eX]

[DOI]

Proceedings of the 23rd Australasian Computer Science Conference (ACSC 2000), 31 January, 2000

1999

The deadline command.

[BibT_eX]

[DOI]

Geoffrey Watson

IEE Proc. Softw., 1999

Towards Real-Time Object-Z.

[BibT_eX]

[DOI]

Graeme Smith

Proceedings of the Integrated Formal Methods, 1999

1998

Expressive Power of Specification Languages.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1998

A Program Refinement Tool.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1998

Deadlines are termination.

[BibT_eX]

Proceedings of the Programming Concepts and Methods, 1998

A Set-Theoretic Model for Real-Time Specification and Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 1998

Defining Differentiation and Integration in Z.

[BibT_eX]

[DOI]

Brendan P. Mahony

Proceedings of the Second IEEE International Conference on Formal Engineering Methods, 1998

1997

Supporting Contexts in Program Refinement.

[BibT_eX]

[DOI]

Ray Nickson

Sci. Comput. Program., 1997

1996

Supporting Module Reuse in Refinement.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1996

Refining Specifications to Logic Programs.

[BibT_eX]

[DOI]

R. G. Nickson

Proceedings of the Logic Programming Synthesis and Transformation, 1996

Integrating Real-Time Scheduling Theory and Program Refinement.

[BibT_eX]

[DOI]

Proceedings of the FME '96: Industrial Benefit and Advances in Formal Methods, 1996

1995

Specification by Interface Separation.

[BibT_eX]

[DOI]

Jeff W. Sanders

Formal Aspects Comput., 1995

Using Units of Measurement in Formal Specifications.

[BibT_eX]

[DOI]

Brendan P. Mahony

Formal Aspects Comput., 1995

A Formal Semantics for a Language with Type Extension.

[BibT_eX]

[DOI]

Peter Bancroft

Proceedings of the ZUM '95: The Z Formal Specification Notation, 1995

Are Formal Methods Relevant?

[BibT_eX]

[DOI]

Proceedings of the 2nd Asia-Pacific Software Engineering Conference (APSEC '95), 1995

1994

Understanding the differences between VDM and Z.

[BibT_eX]

[DOI]

John E. Nicholls

ACM SIGSOFT Softw. Eng. Notes, 1994

1993

Deriving Modular Designs from Formal Specifications.

[BibT_eX]

[DOI]

Proceedings of the First ACM SIGSOFT Symposium on Foundations of Software Engineering, 1993

1992

A Case-Study in Timed Refinement: A Mine Pump.

[BibT_eX]

[DOI]

Brendan P. Mahony

IEEE Trans. Software Eng., 1992

VDM and Z: A Comparative Case Study.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1992

Multi-Relations in Z.

[BibT_eX]

[DOI]

Acta Informatica, 1992

Towards Libraries for Z.

[BibT_eX]

[DOI]

Luke Wildman

Proceedings of the Z User Workshop, London, UK, 14-15 December 1992, Proceedings, 1992

1990

Interpretations of Z Schema Operations.

[BibT_eX]

Proceedings of the Z User Workshop, 1990

1989

A Generalisation of Bags in Z.

[BibT_eX]

[DOI]

Proceedings of the Fourth Annual Z User Meeting, Oxford, UK, December 15, 1989, 1989

Signalling System No.7, The Network Layer.

[BibT_eX]

M. Mowbray

Gordon A. Rose

Proceedings of the Protocol Specification, 1989

1987

Laws of Programming.

[BibT_eX]

[DOI]

Commun. ACM, 1987

1986

Specification Directed Module Testing.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1986

1985

Applying Formal Specification to Software Development in Industry.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1985

1978

Some remarks on "Ambiguous Machine Architecture".

[BibT_eX]

[DOI]