From 7d7754b75232c52c17a29da59870a70c0005093f Mon Sep 17 00:00:00 2001 From: Kyle Isom Date: Fri, 2 May 2014 13:52:23 -0700 Subject: [PATCH] Add new category, program verification. The inaugural paper in this category describes using Coq to create a formalised subset of the x86 architecture. --- program_verification/README.md | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 program_verification/README.md diff --git a/program_verification/README.md b/program_verification/README.md new file mode 100644 index 0000000..7e3318a --- /dev/null +++ b/program_verification/README.md @@ -0,0 +1,3 @@ +# Program Verification + +* [Coq: The world’s best macro assembler?](https://research.microsoft.com/en-us/um/people/nick/coqasm.pdf)