Cargando…

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Recent experiments have shown that satisfiability of a quantified bit-vector formula coming from practical applications almost never changes after reducing all bit-widths in the formula to a small number of bits. This paper proposes a novel technique based on this observation. Roughly speaking, a gi...

Descripción completa

Detalles Bibliográficos
Autores principales: Jonáš, Martin, Strejček, Jan
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326550/
http://dx.doi.org/10.1007/978-3-030-51825-7_27