bounded model checking using satisfiability modulo theories

this project is part of a bigger project, namely the eureka project at artificial intelligence laboratory.

C bounded model checking (cbmc) is one of the leading approaches to automatic software analysis. The key idea is to

  • build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property, and
  • use state-of-the-art sat solvers to check the resulting formulae for satisfiability.
in this project we propose a generalisation of the cbmc approach based on an encoding into richer (but still decidable) theories than propositional logic. our approach may lead to considerably more compact formulae than those obtained with cbmc. we have built a prototype implementation of our technique that uses a satisfiability modulo theories (SMT) solver to solve the resulting formulae. computer experiments indicate that our approach compares favourably with and on some significant problems outperforms cbmc.

for more details, please go to the papers section of the eureka project web page.

Experiments

you may want to take a look at the benchmark programs that we used for our experiments.

download our benchmarks1 and benchmarks2.
Back to the main page
this website is maintained by jacopo mantovani. Last updated: Dec 19, 2005