Popili’s advanced formal verification allows you to find errors in your software automatically during development and fix them prior to integration. Need to make software changes? Let Popili tell you which dependencies are impacted and whether any errors have been introduced.
Do your ports or components have any runtime errors? For example, are there any accidental array out-of-bounds or overflows in your code, obscure corner cases where one of your functions is trying to read or load an invalid value, or scenarios where a state invariant is violated?
Does each component interact correctly with other components it depends upon in accordance with their ports? For example, are there any scenarios where your software makes function calls on other parts of the system which can’t handle them, or receives signals that it can’t handle?
Are your ports and components well-formed? For example, have you accidentally built a nondeterministic implementation, or built an implementation that, under certain circumstances, can become unresponsive to calls from other parts of the system?
Do your components implement their ports correctly? For example, are there any scenarios where your implementation sends signals that are prohibited by its specification, fails to implement functions that its specification says it must, or fails to guarantee that an action will eventually occur?
That’s why we built our own bespoke verification engine, Cosmos – designed and optimised for event-driven software. It’s why our verification approach is compositional – you can decompose your systems into collections of subsystems, and build and verify each one independently. So you’ll be safe in the knowledge that they’ll work together correctly when integrated.
It’s also why we provide a powerful cloud verification service – to not only increase processing speed, but also provide caching for your results. That way, any member of your team can get them without having to rerun the verification.
