Timeline for Proof Carrying LLVM?
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 2, 2018 at 21:22 | answer | added | Jules | timeline score: 3 | |
| Sep 21, 2017 at 4:49 | history | tweeted | twitter.com/StackCompSci/status/910727562153906176 | ||
| Nov 11, 2015 at 23:29 | comment | added | Pseudonym♦ | Just a suggestion, but you might want to consider a simpler language like Berkeley Packet Filter. | |
| Nov 11, 2015 at 20:08 | comment | added | Jason Kleban |
I'm only considering this now, but I guess that while LLVM is capable of strong type safety mechanisms, a compiler like clang for languages like c which are not enforced as type safe, the resulting LLVM cannot take advantage of those type safe mechanisms either (falling back to some idea of unsafe)? Is a property of type-safety not enough to guarantee memory safety? Rust understands memory safety. So perhaps LLVM lacks a native understanding of the safety property it would need to then emit a proof of that safety property?
|
|
| Nov 11, 2015 at 19:48 | comment | added | D.W.♦ | I still think you need to clarify what the source language is. Your citation talks about Java. Doing PCC when the source language is Java is very different than when the source language is C; the latter raises a host of issues not present in Java. Also, there are reasons why you'd want to start from the source language, not from LLVM bitcode. Is an answer that explains those issues and reasons the kind of thing you'd count as a satisfactory answer? | |
| Nov 11, 2015 at 18:52 | history | edited | Jason Kleban | CC BY-SA 3.0 |
added 2399 characters in body
|
| Nov 11, 2015 at 18:18 | comment | added | D.W.♦ | Finally, I think it would help to clarify exactly what you're asking about: Extending a C compiler to generate proofs of memory safety as it translates from C to LLVM bitcode? Something else? It's not clear where you expect LLVM to come into it or what task you're hoping about, so some edits to clarify this might help. | |
| Nov 11, 2015 at 18:15 | history | edited | D.W.♦ | CC BY-SA 3.0 |
Avoid making assumptions that it is impossible today.
|
| Nov 11, 2015 at 18:14 | comment | added | D.W.♦ | PCC for what properties? Memory safety? Do you have a citation/reference for your statement about practicality? What research have you done? Have you tried doing some searching on Google Scholar to find the state-of-the-art in PCC, and to see if you can find any research papers that implement PCC for LLVM? | |
| Nov 11, 2015 at 15:00 | comment | added | Raphael | While the concepts involved are certainly CS territory, I'm not sure if a question that aims at one specific language is ontopic here. I'll let the community decide. | |
| Nov 11, 2015 at 15:00 | history | edited | Raphael |
edited tags
|
|
| Nov 11, 2015 at 14:36 | history | asked | Jason Kleban | CC BY-SA 3.0 |