Re:LLM4Decompile: Decompiling Binary Code with LLM
by thfuran on Sunday March 17, 2024 @11:16AM
(#39734994)
Good luck formally proving Linux.
[ Parent
| on HN ]
Re:LLM4Decompile: Decompiling Binary Code with LLM
by layer8 on Sunday March 17, 2024 @11:17AM
(#39735003)
The goal is to prove that the source code matches the machine code, not to prove that the code implements some intended higher-level semantics. This has nothing to do with formally proving the correctness of the Linux kernel.