Making public the code
Closed this issue · 7 comments
analysis (coming once Jorge gets back from maternity leave).
@ianamason Any update on this? I'm very interested in this work! I'm working a similar project as part of my master thesis (code generation and verification for NTT).
@masahi : thank you for your interest!
The reason that made us to postpone making public the code of the NTT verifier is that the original version worked on LLVM 5.0 which is quite old. It has been on my TODO list for a while to port the verifier to some more recent LLVM version (e.g., LLVM 10). I'll try to make public the code by the end of this week. If I don't have time to do it, I will give you access to the original version we used in our VSTTE'20 paper.
Is that work for you?
@caballa Thank you for the quick response. Yes, it works for me but there is no need to rush. I'm very new to verification in general and right now I'm learning about theory and tools around it.
I did try to build seahorn master branch but failed. Then I found dev10 branch which seems to be in an active development and I was able to build it. If the NTT code is going to work with dev10 branch it would be really cool.
@masahi: we have committed the implementation of the verifier. Take a look and try! It works on LLVM 11.
Sorry for the delay.
Yay Jorge! Or should I call you "The Mackerel"? See this @BrunoDutertre ?