Welcome to Kestrel Technology (KT)
KT's business is to support development and maintenance of high assurance applications, in particular those with mission- and safety-critical components. Our help comes through tool-based consulting services and collaborative partnerships.
Technology based on sound, efficient and scalable mathematics enables us to analyze, transform, and verify industrial scale applications.
- We provide high assurance software property verification, both language- and application-specific.
- Policies can be formally specified, maintained separately from code, and soundly woven into an application.
- Models can be transformed correctly into forms for integration with other tools or into code.
- Vulnerability exposure and even obfuscated malware cannot escape our source code analyzers.
- Runtime properties enjoy added assurance with our technologies for in situ monitoring.
Contact us to learn more about how we can help you to achieve the benefits of mathematically sound, high assurance software with practical economics.
Breaking news
SAMATE (Software Assurance Metrics and Tool Evaluation) is a project initiated by NIST to develop standard evaluation measures and methods for software assurance [Black, P. SAMATE and evaluating static analysis tools. ADA User Journal 28 (2007), 184–188.]. The SAMATE dataset at present contains around 2000 benchmark programs in different programming languages.
The results of applying CodeHawk to SAMATE benchmarks 115–1278 are available on KT's publications page. The analysis with CodeHawk is fully automatic; the results were generated without any user intervention; and the analyzer was applied directly on the code as downloaded from the SAMATE database. The vast majority of the cases were verified as claimed by NIST. In some cases due to underspecification of input ranges, only warnings were produced. In a few remaining cases, interesting discrepancies point to the strength of CodeHawk's semantic analysis.