veri-datalog/dafny/lcf/def.dfy at trace-reconstruction · secure-foundations/veri-datalog
Verified Datalog. Contribute to secure-foundations/veri-datalog development by creating an account on GitHub.
One kind of cool thing I did at CMU (with others) is mechanize verified proof checker for Datalog traces: github.com/secure-found...
Given a trace made by an untrusted solver, the Dafny code replays the trace and builds a proof tree in ghost. By construction, only valid proof trees can be created
28.05.2025 20:22 —
👍 1
🔁 0
💬 0
📌 0
The PLDI Student Research Competition's deadline is this week! We have an excellent group of expert reviewers lined up, submit/encourage your students to submit!
12.03.2025 16:11 —
👍 0
🔁 3
💬 0
📌 0
