The research behind Visão: how Equid became our static analyzer
Before Visão was a product, it was a research project called Equid - a language-agnostic static analysis framework built to close the gap between academic verifiers and real industrial code. Here is the paper behind our analyzer, and the ideas that carried into what we ship today.
Today, Visão is our static analysis engine - it reads source code, traces underlying defects rather than just known patterns, and scales to large multi-language codebases in high-reliability environments. But it did not start as a product. It started as a research project called Equid.
Equid was a static analysis framework designed by our founder Maxim Menshikov and presented at ICCSA 2019 (Springer LNCS, vol. 11619). The name loosely stands for "Engine for performing queries on unified intermediate representations of program and domain models." This is the story of that research - what it set out to do, how it worked, and which of its ideas live on inside Visão today.
The problem: theory that does not ship
Static analysis has a split personality. On one side sit academic tools with an exhaustive feature set - model checking, abstract interpretation, SMT solving - that rarely survive contact with a real 500,000-line codebase. On the other side sit industrial verifiers that install in minutes but treat your program as a black box and miss most of what matters.
Developing large software - especially anything tied to specialised hardware - means bugs can hide at any layer: OS core, shell, network setup, userland, even the hardware. Universal built-in detectors are rarely enough, and if the analysis does not integrate into the actual development workflow, engineers simply stop using it. That abandonment is the single biggest reason verification tools fail in practice.
Equid started from a different set of assumptions than most academic tools - assumptions grounded in what industrial code actually looks like:
Mature code is mostly debugged
Memory corruption is rare in shipped code, so exhaustive state-space exploration is often wasted effort - reserve it for the few critical components that truly need it.
The tool should assist, not replace
You cannot prove every algorithm automatically. The developer helps the tool, and contracts become a natural, machine-checkable extension of the documentation.
Contracts catch most real bugs
Function and memory-access contracts are usually enough to surface the majority of observable defects - without a PhD in formal methods to operate them.
It has to fit the workflow
Batch "night analysis", predictable load distribution and easy invocation are features, not afterthoughts. An unusable analyzer is an unused analyzer.
The pipeline, end to end
Equid processes code in stages, and the whole design is language-agnostic: the analysis is the same regardless of source language, and adding a language is cheap. The internal model was general enough to extend toward object-oriented languages - the same multi-language ambition that defines Visão now.
1. Source → Generalized Syntax Tree (GST)
Instead of binding to one compiler framework, Equid treats Clang as just one possible parser backend. Whatever the parser produces is transformed into a Generalized Syntax Tree - a unified representation that strips away syntax sugar and merges the abstract syntax trees of different languages into one shape. The GST also mines persistent relations between statements and groups them into Fragments, which makes lock-set-style concurrency analysis nearly trivial.
2. GST → Virtual Machine codes
A tree is awkward for flow-sensitive analysis, so Equid lowers it into its own intermediate representation - a compact instruction set (declare, assign, branch, check, constraint, invoke). Unlike LLVM IR and similar hardware-shaped codes, this IR can carry analyzer-specific globals and custom types without phantom variables or awkward workarounds - it describes what an expression means to the analyzer, not how a CPU would run it.
3. A Hypervisor drives Virtual Machines
A Hypervisor sits at the top and manages Virtual Machines that "execute" the VM codes - not to run the program, but to provide flow- and context-sensitivity. For flow-sensitive analysis it inlines function summaries built with Craig interpolation; for context-sensitive analysis it unrolls function bodies with enter/exit blocks. The VMs handle control flow; all the real reasoning is handed off to the solver.
4. The Multi Solver does the reasoning
This is the heart of Equid - and the reason Visão traces root causes instead of matching surface patterns. The Multi Solver combines two very different engines and lets them reinforce each other:
SMT solver (CVC4)
Turns whole functions into assertion clauses and checks the negation of the goal to verify contract violations. CVC4 was chosen for its robustness, native C++ interface and broad theory support.
Abstract interpreter
Produces an over-approximation using abstract domains (interval, polyhedral) that shrinks the SMT state space, improves precision, and can catch errors on its own - with negligible impact on analysis time.
The Multi Solver picks the most convenient interpretation per case: exact reasoning where the state space is small, over-approximation where a loop is potentially unbounded. A precise, tunable type system - built to handle endianness, ambiguous integer widths and cheap-vs-expensive conversions - keeps the memory model honest across CPU and compiler targets.
5. Semantic Storage underneath it all
Every artifact - resources, fragments, expressions, VM codes - lives in a Semantic Storage backed by MongoDB, each with a stable ID and key-value metadata. For projects that fit in RAM the database is optional; for large ones it enables a distributed technology stack, dynamic load/unload of resources, and a much smaller memory footprint. No other analyzer in the comparison used a separate semantic store like this - and it is a big part of how Visão handles large codebases today.
Contracts and detectors
Bugs are found in two complementary ways. Contracts are written in ACSL - the same annotation format used by Frama-C - and parsed straight into VM commands, giving an extremely fast first pass over user and standard-library functions. Detectors are essentially temporal-logic (LTL) formulas over the flow, and they come in a few flavours:
- GST visitors - structural checks such as duplicate operands.
- Markup manipulators - track state like "allocated" or "open handle"; a leak detector just checks that anything not passed out is freed before return.
- Sequence observers - flag bad patterns, e.g.
fclose(x)followed byread(x).
The standard library is annotated once, preloaded on startup, and a prototype that recompiled annotations to C loaded them roughly six times faster by skipping the parser entirely.
Does it actually find bugs?
On a supported subset of the Toyota ITC benchmarks, Equid detected roughly 90% of bugs in supported categories - broadly on par with Frama-C, and clearly ahead of Clang and cppcheck. It even led on categories like datalost and dataoverflow.
| Benchmark | Equid | Frama-C | Clang | cppcheck | Total |
|---|---|---|---|---|---|
| bitshift | 17 | 17 | 14 | 11 | 17 |
| bufferoverrun dyn. | 30 | 32 | 1 | 2 | 32 |
| bufferunderrun dyn. | 35 | 39 | 2 | 3 | 39 |
| datalost | 19 | 3 | — | — | 19 |
| dataoverflow | 25 | 16 | — | 9 | 25 |
| dataunderflow | 12 | 8 | — | 5 | 12 |
| littlemem_st | 11 | 11 | — | — | 11 |
| nullpointer | 15 | 16 | 13 | 12 | 17 |
| overrun_st | 47 | 54 | 2 | 21 | 54 |
| ptrsubtraction | 2 | 1 | — | — | 2 |
| underrun_st | 13 | 13 | 2 | 5 | 13 |
| uninitpointer | 10 | 16 | 11 | 5 | 16 |
| zerodivision | 16 | 16 | 13 | 8 | 16 |
Detections on the wDefects subset of the Toyota ITC benchmarks. Clang 3.9, Frama-C Silicon, cppcheck 1.76. "—" means no detection in that category.
Beyond benchmarks: real code
Synthetic benchmarks only tell part of the story. Equid was also run against a 500 KLOC operating-system management application. Getting there took domain-specific ACSL models and a declarative pointer analysis - function aliases like /feature/x/enable instead of cryptic internal names - to cope with indirect calls. Once configured, it found genuine contract violations and weaknesses no other analyzer had caught, including uninitialized structure members buried in obscure module code.
A separate experiment applied Equid's querying capability to a 500,000+ line third-party Linux kernel driver and traced the reasons behind real errors that automatic search tools had missed in that badly structured code. Modelling took effort - but the payoff was defects nothing else could reach.
From Equid to Visão
A research paper is a snapshot of a moment. Equid was honest about its limits at the time - unions were only partially supported, inter-procedural coverage was incomplete, the querying language was still maturing. But the architectural bets it made are exactly the ones that turned out to matter, and they carried directly into the product we build today:
Equid research
Generalized Syntax Tree
→ In Visão: one analysis engine across C, C++ and more, instead of a separate tool per language.
Equid research
Multi Solver (SMT + AI)
→ In Visão: tracing the underlying cause of a defect, not just matching a known bug pattern.
Equid research
Semantic Storage
→ In Visão: analysis that scales to large codebases without collapsing under its own memory footprint.
Equid research
Contracts as documentation
→ In Visão: a fast, developer-friendly path to real defects in high-reliability code.
The lesson that started with Equid has only aged well: good verification is not a choice between rigour and usability. It is about engineering both - a configurable, language-agnostic, precise analyzer that still fits the way industry actually works. That is the idea we productised as Visão.
Reference: M. Menshikov, "Equid - A Static Analysis Framework for Industrial Applications," in Computational Science and Its Applications (ICCSA 2019), Springer LNCS, vol. 11619, pp. 677-692. doi.org/10.1007/978-3-030-24289-3_50