Run your code forall inputs

Try Symbolica and see what you find

What is Symbolica?

Symbolica is a symbolic code executor hosted as a 'CI-like' service. We run your code, but instead of feeding it concrete inputs like 1 or "Hello World", we feed it symbols (variables) that represent all of the possible inputs to your program. This allows us to explore all the code paths at the same time, which allows us to do all kinds of interesting things, such as:

  • check if two different programs are logically equivalent
  • find out if any inputs lead to buffer overflows
  • detect inputs that cause undefined behaviour

Logical Equivalence Checking

Symbolica can be used to check if two programs are logically equivalent. By mapping every possible input of your program to its corresponding output, we can determine whether forall inputs two different implementations produce exactly the same outputs.

Find Buffer Overflows

Because we search your program's entire input space, we can find out if any of those inputs might lead to a buffer overflow. Symbolica helps you verify that your code is free from such security vulnerabilities.

Detect Undefined Behaviour

We analyse your code at the LLVM IR level, so we can tell if any part of your program might call instructions with undefined behaviour.

Try it now

You can play with Symbolica right now, for free, on our Playground.

Join the private alpha

We're currently only allowing a small number of early adopters to experiment with the full version of Symbolica.

If you want to be amongst the first to get access, then sign-up for our private alpha today using the form below.

Run it on every commit

From the outset we've designed Symbolica to integrate seamlessly into a DevOps pipeline, so that you can do powerful verification of your code each time you build it.

All you have to do is add a simple declarative script to your repo to tell Symbolica how to analyse your code.

We Open Source

The core of our symbolic executor is open source on GitHub. So if you need to, you can dig deeper and see exactly how it's processing your code.
Symbolica GitHub repo stats