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.
