We love formal methods
We specify, model and verify code and designs using formal logic.
Properties can be anything you can specify in logic. It can range
over a function, or an entire program.
We check those properties against concrete inputs (runtime
verification) and symbolic inputs (formal verification), and
explore all possible behaviors of the code, to give you the
highest possible assurance.
Our approach is based on the K Semantic Framework.
Our approach is based on the K Semantic Framework.
