HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler.

Sascha Böhme Michal Moskal Wolfram Schulte Burkhart Wolff

Published in: J. Autom. Reason. (2010)

Keyphrases

back end
user friendly
theorem prover
theorem proving
data management
data types
programming language
building blocks
general purpose
formal methods
model checking
first order logic
publish subscribe
version control
inference rules
user interaction
databases
data repositories