Towards a mostly-automated prover for bit-vector arithmetic

We present work in progress on the development of EasyBV, a specialized theorem prover for fixed-size bit-vector arith- metic.

Detalhes bibliográficos
Autor principal: Abal, Iago (author)
Outros Autores: Pinto, Jorge Sousa (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2013
Assuntos:
Software/program verification
Deduction and theorem proving
Bit-vectors
SMT
Rewriting
theorem proving
Texto completo:http://hdl.handle.net/1822/26412
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/26412
Descrição
Resumo:We present work in progress on the development of EasyBV, a specialized theorem prover for fixed-size bit-vector arith- metic.

Registos relacionados