6 ms·
Compcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.
by aeneasmackenzie 2y ago
Compcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.
- LiamPowell 2y agoThere's also Frama-C, but having used both Frama-C and SPARK I can say I'd pick SPARK any day. Having a rich type system and not having to work with pointers makes proving a program so much easier.
- MaxBarraclough 2y agoRight, Frama-C can formally prove properties of C code. There are also proprietary solutions that do something similar: • https://www.eschertech.com/products/ecv.php https://www.eschertech.com/products/ecv.php • https://www.trust-in-soft.com/ https://www.trust-in-soft.com/