23 citations · 68 across the 22 of their papers we have counts for
Showing 2016Show all
2 papers · 1 filter
cs.LO2016
Efficient verification of imperative programs using auto2
Bohua Zhan
Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search me…
cs.LO2016★ 10 cited
AUTO2, a saturation-based heuristic prover for higher-order logic
Bohua Zhan
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core…