Developing a Numerical Algorithm with CIVL Model Checking in the Loop

Youngjun Lee, Anshu Dubey, Jan Hückelheim

Verifying a numerical algorithm in a large scientific simulation framework is challenging: the framework is too big to model-check, and the unit tests exercise only sampled inputs.…