3 ms·
You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com
by tom_mellior 9y ago
You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com/ http://frama-c.com/), or SPARK Ada (https://www.adacore.com/download https://www.adacore.com/download). There has been quite a lot of work in imperative languages that might inspire you.
Low-level pointers make everything very very annoying, though.
- thethirdone 9y ago> You might want to look into things like the KeY verifier for Java (https://www.key-project.org/ https://www.key-project.org/), Frama-C for C (http://frama-c.com/ http://frama-c.com/), or SPARK Ada (https://www.adacore.com/download https://www.adacore.com/download). I am aware of SPARK. KeY and Frama-C are new to me though. Thanks for mentioning them. > Low-level pointers make everything very very annoying, though. Definitely.