Great work by the LANGSEC crowd. My recent interest in parsers was those verified for correctness or security. So, they have security and a certain amount of correctness. A great next step would be combining it with work on formal verification of parsers or generators (see below). On top of that, ensure the subset could generate SPARK and/or CompCert-compatible C code to automate much of the rest of the problem. TRX…
Thanks! Those are all excellent papers. I am actually looking into formally verifying Hammer using Frama-C, but haven't gotten too far yet.
Smart move. It's a good default far as work vs results tradeoff. I'll try to keep your project in mind when I review my collection of verification papers in case I see any little-known, C verification methods that might help.