3 entries tagged with #ProofInUse
GNATprove Tips and Tricks: Bitwise OperationsThe ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was trying its best to translate those into equivalent operations on integers. It is now using native theory of smt-solvers when available resulting in much better support, and guaranteeing state of the art handling of bitwise operations. We present some examples in this post.
by Lena Comar
ProofInUse is coming!
For lovers of verification tools and critical system (we know you're out there!), we are very excited to present ProofInUse!