Memory leakage and security are persistent problems experienced by software systems written in the C/C++ programming languages. Whilst finding latent errors that are missed by conventional testing through static analysis has a high return on investment, this type of testing is prone to false negatives; that is, flagging potential vulnerabilities where in fact none exist. The cost of proving these false negatives renders many verification tools impractical.
To speed up the proving rate and increase accuracy we partnered with software verification firm Monoidics’ (since subsumed by Facebook). We integrated the Solve Engine with their static analysis system in place of its internal prover and were thus able to encode assertions and translate them between multiple formats. By exposing these assertions to previously inaccessible solvers we were able to reduce the number of false negatives and identify vulnerabilities more quickly.
reduction in false negatives against common benchmark
fewer false negatives against leading technology
previously unknown errors identified in GZIP and OpenSSH code
1000X faster cable network planning
We created a way to plan fibre round a town in seconds – more than a thousand times faster than the existing approach.Learn more
Mobile cells optimally placed
We placed mobile network infrastructure to maximise coverage whilst minimising equipment costs.Learn more
20% more efficient staff schedules
We reengineered staff rotas for a global entertainment group based on predicted footfall and employee preferences.Learn more
Thank you for contacting us, we will come back to you as soon as possible