Program verification using HOL-UNITY

This publication has 12 references indexed in Scilit:

• Recursive Boolean Functions In HOL
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2005
• Mechanical verification of concurrent systems with TLA
  Published by Springer Nature ,1993
• 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
• A predicate transformer approach to semantics of parallel programs
  Published by Association for Computing Machinery (ACM) ,1989
• Parallel Program Design
  Published by Springer Nature ,1989
• HOL: A Proof Generating System for Higher-Order Logic
  Published by Springer Nature ,1988
• Deciding Combinations of Theories
  Journal of the ACM, 1984
• Proving Liveness Properties of Concurrent Programs
  ACM Transactions on Programming Languages and Systems, 1982
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940