In praise of algebra

DOI10.1007/s00165-012-0249-0zbMath1259.68030MaRDI QIDQ1941861

Stephan van Staden, C. A. R. Hoare

Publication date: 22 March 2013

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-012-0249-0

zbMATH Keywords

refinement; concurrency; algebra

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

Denotational semantics and its algebraic derivation for an event-driven system-level language, A UTP approach for rTiMo, A process calculus BigrTiMo of mobile systems and its formal semantics, On the relation between concurrent separation logic and concurrent Kleene algebra, Constructing the Views Framework, Towards a Modeling Language for Cyber-Physical Systems, Laws of Programming for References

Uses Software

• Isabelle/HOL
• Sledgehammer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Concurrent Kleene algebra and its foundations
• Graphical models of separation logic
• A calculus of communicating systems
• Proving total correctness of nondeterministic programs in infinitary logic
• A completeness theorem for Kleene algebras and the algebra of regular events
• Isabelle/HOL. A proof assistant for higher-order logic
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• On Locality and the Exchange Law for Concurrent Processes
• Concurrent Kleene Algebra
• Laws of programming
• The specification statement
• CONCUR 2004 - Concurrency Theory
• An axiomatic basis for computer programming
• Sledgehammer: Judgement Day