ITHACA, NY–July 9, 2013–GrammaTech, Inc., a leading software developer specializing in software assurance tools and cybersecurity solutions, today announced that the company has received an award from NASA to prototype a specification editing and discovery tool (SPEEDY) for C/C++ code analysis.
Packaged as a plug-in to the Eclipse integrated development environment (IDE), the tool will assist software developers in modular formal verification tasks. SPEEDY will provide automated suggestions of specifications for given contexts, with user interface features aiding developers in generating, editing and checking specifications.
“SPEEDY will essentially be able to look over your shoulder, using machine-checkable specifications to automate sound verification and warn you if something isn’t right,” explained Tim Teitelbaum, GrammaTech’s CEO. “The user interface features, and underlying automation in SPEEDY, will facilitate the use of formal methods by all software developers, improving efficiency and accuracy of development teams.”
SPEEDY will support the needs of NASA’s software-development teams and Independent Verification and Validation (IV&V) groups. The tool will be able to assist NASA personnel in evaluating the safety and robustness properties of software in production or under review, including embedded next-generation avionics and space software. The tool will also serve as a natural companion to the heuristic bug-finding and style-checking tools GrammaTech has completed for NASA’s Jet Propulsion Laboratory (JPL) in the past.
About GrammaTech and CodeSonar:
GrammaTech’s static analysis tools are used worldwide by Fortune 500 companies, educational institutions, startups and government agencies. The staff includes 15 PhD experts in static analysis and a superb engineering team, all focused on creating the most innovative and in-depth analysis algorithms. The company’s flagship product, CodeSonar, is a sophisticated static analysis tool that performs a whole-program, interprocedural analysis on C/C++, Java and binary code, identifying complex programming bugs that can result in serious reliability or security problems. More information about CodeSonar can be found on our website at http://www.grammatech.com/codesonar.
