Combining the benefits of static and dynamic source code analysis to deliver the most advanced & exhaustive code verification tool.
Mathematically prove C and C++ source code quality and maximize code safety and security with TrustInSoft Analyzer.
TrustInSoft Analyzer was the first in the world to meet the SATE V Ockham criteria of the NIST for exhaustivity and soundness.
TrustInSoft Analyzer identifies all bugs, meaning no false negatives. The analysis begins with no false positives, meaning each bug found is a true bug that needs to be corrected.
TrustInSoft Analyzer boosts the coverage of your tests by generalizing inputs, allowing you to test the superset of possible values for an exhaustive coverage of your code.
TrustInSoft Analyzer uses a series of formal methods to mathematically model your code, allowing you to obtain a mathematical proof that there are no bugs left once all issues detected by TrustInSoft Analyzer are corrected.
TrustInSoft Analyzer enables you to precisely visualize all variable values at every step of the execution path
Since the analyzer is following closely the program’s execution path, any detected problem happens in a real execution of the program, which means no false positives. The tool doesn’t raise any false alarms: each alarm corresponds to a real bug.
TrustInSoft Analyzer propagates values of the program at every step, and for each step, it verifies if, with these values, there is an illegal operation.
If there is an illegal operation, TrustInSoft Analyzer will always trigger an alarm, so there are never false negatives. If no alarm is raised, there is no undefined behavior left.
TrustInSoft Analyzer allows you to focus on variables involved in an alarm and track all statements affecting their values (defining the memory contents that these variables point to), and navigate back and forth along the execution path.
The analyzer helps you to find the root cause of this problem directly among these tracked statements, and ignoring all statements not involved in this problem, thus saving you time and effort.
TrustInSoft Analyzer mathematically models your program by abstracting the target platform, making it possible to simulate the behavior of your program on many hardware target platforms. The supported
platforms include ARM, X86, PPC, MIPS, and SPARC variants with the possibility to
easily add new platforms.
It helps you to detect all undefined behaviors on all hardware target platforms by easily switching the target without having the hardware close at hand.
TrustInSoft Analyzer comes with both a Graphical User Interface and a Command-Line Interface with an API to fetch all available results.
The Graphical User Interface helps you to investigate/understand problems and the Command-Line Interface allows the analyzer to be
easily integrated with any CI platform in your DevOps or DevSecOps process.
With our progressive methodology, any developer or tester can use TrustInSoft Analyzer. An analysis can be broken down into 3 steps:
Supercharging existing test suites to detect more bugs by exhaustively detecting undefined behavior on execution paths covered in the test suites.
Generalizing test suites to greatly increase the code coverage in no time.
Checking functional implementation to ensure program behaviors are compliant with their specifications
Check out this demo video of TrustInSoft Analyzer on popular open-source software Wireshark. TrustInSoft Analyzer identified a series of undefined behaviors that had been left undetected in the code for years before this analysis, which have since been corrected.
How can TrustInSoft Analyzer make a difference in your software safety and security?