PV4 ⊧ SPEARproves a theorem about software verification conditions, formulated in bit-vectors

SPEAR is a bit-vector arithmetic theorem prover designed for proving software verification conditions

Application domain/field

• Theorem proving
• Arithmetic
• SAT solving

Type of tool

Modular theorem prover

Expected input

Format:

SPEAR MAF

Internals

• the core is a fast and simple SAT solver
• involves aggressive constant propagation