diff --git a/talks/tan.md b/talks/tan.md new file mode 100644 index 0000000..2b89035 --- /dev/null +++ b/talks/tan.md @@ -0,0 +1,11 @@ +--- +author: "Wolfgang Ahrendt" +kind: "Short Talk (10 min. + 5 min.)" +track: "KeYmaera Track" +title: "The Last Mile in Trustworthy Automated Reasoning" +slot: 220 +length: 15 +order: 36 +--- + +This is a short talk on enhancing the trustworthiness of automated reasoning tools by building so-called certifying algorithms and corresponding proof checking workflows. I will give a demo based on SAT solving, where the generation and checking of unsatisfiability proof has become a (near) mandatory feature for all modern solvers.