Formally verify that software or firmware programs fulfill their specifications.
Formally verify that a hardware design fulfills its specifications.
Formally verify that programs written in different languages (even across the hardware/software boundary) are equivalent.
Improve the assurance of software using symbolic testing.
Provide libraries for symbolic formula representation and solver interaction.
Analyze binaries in a variety of formats and for a host of different Instruction Set Architectures.
Perform binary analysis and rewriting for a variety of purposes.
Automatically generate model-based tests for a software, firmware, or hardware system.
Specify a systems architectures at a high level leveraging Natural Language Processing technology.
Create or generate a new model or an implementation from a semi-formal or formal model or implementation by adding extra information, typically turning a denotational property into an operational computation, and guarantee that the new, refined model behaves identically to the previous, abstract model.
Extract formal models---including behavioral and architectural models---from source code and binaries, and guarantee that all properties of the abstract model hold for the more concrete model or implementation.
Define a pair of functions, an abstraction function L: I->M and concretization function C: M->I, such that they form a refinement relation over some property P (roughly, P(c(l(i)))=P(i)) between their pair of types M and I.
Specify and formally refine a semi-formal architecture.
Specify and reason about product lines of hardware, firmware, and/or software systems.
Reason about products derived from product lines, particularly automatically generated CPUs and SoCs.
Reason about non-behavioral properties of models or implementations, such as security proofs of cryptographic algorithms and protocols, safety and progress properties of concurrent or distributed systems, information leakage properties of embedded systems and hardware designs.
Make feature selections in a feature model in order to specify the subset of products from a product line that are of interest.
Configure a feature model until no open choices exist, thereby creating a fully configured feature model that specifies a single product.