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, On algebra of program correctness and incorrectness, 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