Formally Certified Approximate Model Counting

The integration of powerful computer-aided reasoning has scaled formal methods to meet the verification demands of modern computer systems. However, as these tools become increasingly complex and optimised, it is essential that we can trust their core reasoning algorithms and implementations.

This paper presents a new approach for certifying probabilistic systems and demonstrates it on a state-of-the-art approximate model counter, ApproxMC, developed by Professor Meel and his team.

The key contribution of this paper is its combination of theorem proving and certificate generation/checking, applied to randomised algorithms. Through fruitful collaboration, the team employed their hybrid approach to develop a comprehensive certification process for ApproxMC, covering everything from its theoretical soundness to its tool implementation. 

In the process, they showed that their certification approach adds minimal overhead to model counting and identified minor bugs in ApproxMC, which they subsequently fixed.

The team is excited to apply their certification framework to other randomised algorithms, with the potential to further enhance the trustworthiness of formal methods. They also plan to extend this work to related model counting tasks and continue improving the reliability of automated reasoning tools.

You can read the paper on Formally Certified Approximate Model Counting here.