Mechanically verifying concurrent programs with the Boyer-Moore prover

This publication has 11 references indexed in Scilit:

• Mechanizing CSP trace theory in higher order logic
  IEEE Transactions on Software Engineering, 1990
• Microprocessor design verification
  Journal of Automated Reasoning, 1989
• A simple approach to specifying concurrent systems
  Communications of the ACM, 1989
• A mechanical proof of the Church-Rosser theorem
  Journal of the ACM, 1988
• Soundness of Hoare's logic: an automated proof using LCF
  ACM Transactions on Programming Languages and Systems, 1987
• Safety without stuttering
  Information Processing Letters, 1986
• Automatic verification of finite-state concurrent systems using temporal logic specifications
  ACM Transactions on Programming Languages and Systems, 1986
• Defining liveness
  Information Processing Letters, 1985
• Adequate proof principles for invariance and liveness properties of concurrent programs
  Science of Computer Programming, 1984
• An axiomatic basis for computer programming
  Communications of the ACM, 1969