2 ms·

SPARK has been used for a microkernel (Muen), crypto primitives (Skein) that caught error in C version, and DNS server (Ironsides). Might be worth mentioning in

SPARK has been used for a microkernel (Muen), crypto primitives (Skein) that caught error in C version, and DNS server (Ironsides). Might be worth mentioning in these so people can see practical work. Far as floating point, I might take your word for it on how hard it is but what's your take on work like Gappa? https://www.lri.fr/~melquion/doc/14-smt12-expose.pdf https://www.lri.fr/~melquion/doc/14-smt12-expose.pdf Think such methods can be expanded to handle more of it like SPARK does runtime errors? Or it will stay really hard?

touisteur 9y ago
I'd read about gappa in here : https://hal.inria.fr/hal-01534533/document https://hal.inria.fr/hal-01534533/document and then https://hal.archives-ouvertes.fr/hal-01522770/document https://hal.archives-ouvertes.fr/hal-01522770/document . Seems they're building on the work done with gappa. My guess (bystander and user of the tech) is that it'll stay hard for 5-10 years (slow progress of research projects, lots of lead bullets, and far more cores on our dev machines...). If you're motivated and are ready for semi-automated proof you can probably use lemmas (pre-proven properties) in Spark but if you can't find your lemmas in the Spark toolset, then good luck with Coq or Isabelle. Some encouraging stuff is going on in the FP static analysis world though, with projects like herbie (based on sampling only IIRC), the Tocatta lab, and I've heard some good things about numalis (start-up). Edit: seems Gappa can be integrated through why3, and seems they did some work on collabaration with alt-ergo so it seems it should be usable through Spark. Something to check in the next release :-D.