top | item 43048812 (no title) aeneasmackenzie | 1 year 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. discuss order hn newest LiamPowell|1 year ago There'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|1 year ago Right, 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.trust-in-soft.com/
LiamPowell|1 year ago There'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|1 year ago Right, 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.trust-in-soft.com/
MaxBarraclough|1 year ago Right, 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.trust-in-soft.com/
LiamPowell|1 year ago
MaxBarraclough|1 year ago
There are also proprietary solutions that do something similar:
• https://www.eschertech.com/products/ecv.php
• https://www.trust-in-soft.com/