The Power of Definitions for Model Counting and Sampling

30/09/2022

Speaker

Mate Soos

Abstract

Model counting and sampling are important areas of formal methods that can help users reason about probabilities, automatically generate test cases, or verify neural networks. As in many areas of computer science, preprocessing the input problem can significantly lower the execution cost of most algorithms. In this talk, we present our independent support computation technique, Arjun, that acts as a preprocessor for model counting and sampling tools, significantly improving their performance.

Bio

Mate Soos got his PhD from INRIA, France in 2009, and has since been conducting research on formal methods, along with working in industry. Within the scope of his research, he has been working on SAT and SMT solving, model counting, and uniform sampling. Recently, he has been focusing his research on probabilistic methods such the approximate model counting tool ApproxMC, and the uniform-like sampler CMSGen.