Formal proof producing decision procedures

Опубликовано 7 сентября 2016, 17:58

Automated decision procedures nowadays play a crucial role in the verification process of real life code. The breakthrough introduced by SAT and then SMT solvers make them very widely use to help developers prove assertions about the correctness of their code. Yet these tools, especially in the case of SMT solvers, often give little explanation about their answer, which can become an obstacle when certifying critical code. In this talk I will describe how formal proof assistants can help in that case, which approaches are already available for this task, and the challenges this problem raises for proof assistants.