Systems Analysis & Verification

Projects

Currently, we have the following projects:

• ConSave: Analysis and verification for concurrent systems and programs
• F-Soft: Software verification platform for sequential programs
• Tessa: Techniques for Embedded System and Software Assurance
• VeriSol: Symbolic model checking platform (SAT-based, SMT-based)

ConSave

We have developed many techniques for component-level verification in hardware (VeriSol project) and sequential software programs (F-Soft project). However, these methods do not always scale up to the system-level. Furthermore, with the growth of multi-core processing and concurrent programming in many key computing segments, there is a great need to develop effective verification technology for concurrent programs. The ConSave project attempts to fill these gaps. It is essential to combine formal methods with other techniques for verification of such systems, with the overall aims of reducing their development costs and improving designer/developer productivity. Our research focuses on:

• Methods for handling concurrency: These include concurrent dataflow analyses, model checking, testing and dynamic execution.
• Methods for system-level verification: These include compositional verification methods that exploit design modularity, and semi-formal techniques that improve test coverage.
• Applications: We plan to investigate challenging applications, and develop multiple tool flows based on a common platform for various analyses.

F-Soft

F-Soft is a platform for verifying source code programs. It can check C programs for runtime errors such as pointer access violations, buffer overflow, memory leaks, standard library API usage and other user-defined properties. It can be used to check programs globally, or it can be used as an annotation checker for checking user written contracts. We have successfully analyzed large benchmark examples to find previously unknown bugs using F-Soft [1]. An in-house product based on F-Soft, called VARVEL, is currently in use at NEC.

Overall, F-Soft provides a cooperative, staged framework of various static analyses and model checking techniques, where the size and complexity of the model and the number of properties are successively reduced across the stages. This enables efficient use of complex analyses when needed for higher precision. We believe this is essential for handling large programs with hundreds of (automatically instrumented) properties.

A more thorough explanation of F-Soft can be found here.

Tessa

The Tessa project targets system analysis and verification for model-based design flows in embedded, real-time, and cyber-physical domains. These systems will be designed for greater autonomy, efficiency, functionality, reliability, and safety requirements than systems today. Typical examples include avionics and automotive domains. As part of this project, we are working on extending the F-Soft framework to better handle software common in these domains, such as source code that heavily relies on floating-point or fixed-point numbers. We also target popular model-based design flows by providing tools to systematically analyze the models for property verification or test coverage improvements.

VeriSol

This project includes efficient and scalable model checking techniques at the Boolean level (bounded and unbounded model checking, abstraction-refinement, efficient memory modeling), high performance constraint solvers (SAT solvers, SMT solvers) and verification techniques at higher levels of design abstraction (high-level BMC, polyhedral-based model checking). It supports hardware verification by providing a front-end for Verilog designs. It is also used for software verification, by providing the model checking back-end for the F-Soft platform.

VeriSol is available commercially as a C-level property checker in CyberWorkBench (CWB), a System LSI Design Environment, developed and provided by NEC System Technologies, Ltd.