ANSI-C Software Components for Automated Proof Search

Developing a proof engine with industrial performance and capacity is a risky and costly venture. At best, it requires a team of computer science PhD’s and years of R&D, at worst the venture fails to deliver. Our commercially packaged Prover Plug-In® proof engines enable software tool vendors to, instead of starting from scratch license a proven commercial off-the-shelf component. This means that the cost, performance and capacity is known up front, and the risk of failure is eliminated.

The Prover Plug-In products are intended for developers and suppliers of various system design and verification tools, for instance those used in electronic design, complex IC and systems on a chip, critical control software, embedded systems, and design and specification tools for languages such as TTCN, UML, and SDL, to name a few.

Integration

The Prover Plug-In products target verification software suppliers. They can be used to power verification tools for systems specified using languages like PiSPEC, Verilog, C, Simulink, Statemate, SCADE and UML, to name a few.

A mature and industry-proven solution

Prover Plug-In solves industrial problems faster and using less computer memory than the competition. Further, Prover Plug-In enjoys close to 20 years of R&D and industrial experience and includes patented proof methods. In addition, Prover Technology offers top quality support and maintenance.

Analysis Capabilities and Modeling Language

Prover Plug-In can be used to perform bounded and unbounded model checking, combinational and sequential equivalence checking, and test generation. The engines support modeling of sequential systems using imperative and declarative formalisms and a wide variety of data types including arrays, booleans, integers and reals.