by David Hauzar SPARK 16: Generating Counterexamples for Failed ProofsWhile the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory. #Formal Verification #SPARK
by Clément Fumex 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. #Formal Verification #SPARK
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! #SPARK #ProofInUse