The HOL-Voss system: Model-checking inside a general-purpose theorem-prover

This publication has 4 references indexed in Scilit:

• Linking BDD-based symbolic evaluation to interactive theorem-proving
  Published by Association for Computing Machinery (ACM) ,1993
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
  IEEE Transactions on Computers, 1991
• STATEMATE: a working environment for the development of complex reactive systems
  IEEE Transactions on Software Engineering, 1990
• Correctness Properties of the Viper Block Model: The Second Level
  Published by Springer Nature ,1989