A modular coding of UNITY in COQ

This publication has 8 references indexed in Scilit:

• A proof environment for concurrent programs
  Published by Springer Nature ,2005
• On the logic of UNITY
  Theoretical Computer Science, 1995
• Extensions of the UNITY Methodology
  Published by Springer Nature ,1995
• Program verification using HOL-UNITY
  Published by Springer Nature ,1994
• Eliminating the substitution axiom from UNITY logic
  Formal Aspects of Computing, 1991
• Mechanically verifying concurrent programs with the Boyer-Moore prover
  IEEE Transactions on Software Engineering, 1990
• The calculus of constructions
  Information and Computation, 1988
• The formal specification and design of a distributed electronic funds-transfer system
  IEEE Transactions on Computers, 1988