Software Property Assurance

Mission risk mitigation requires that key system properties hold. For large, complex applications this is a challenging objective. Time and cost can stand in the way of improvements. For development the response has typically been to rely on best practices, and for verfication to test to the limits of the budget.

Formal methods have been repeatedly considered for high assurance, but until now their successful use has encountered severe problems for scaling beyond small applications. Consequently, there is an industry-wide skeptical attitude toward their practicality. KT can demonstrate for you that property assurance on existing code -- even for systems with users in the loop -- can reduce or eliminate conventional testing through customized, mathematically-based static analyzers. Where you must still test, we can show you how to make best use of your testing budget.

For high assurance in software verification, we can help you to ensure that your application:

  • satifies defined properties
  • is not vulnerable to defined classes of security threats
  • meets your current policy requirements
  • is safely monitored at runtime

We offer an approach tailored for each application, bringing to bear technologies that have been developed and refined over decades by world leaders in each specialty.