Scalable and precise program analysis at NEC
Gogul Balakrishnan, Malay Ganai, Aarti Gupta, Franjo Ivančić, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang · 2010
NEC Labs engages in foundational as well as applied research in the areas of verification and analysis of software and embedded systems. We have developed several tools and frameworks for scalable and precise analysis of programs, some of which are now used within the company on large software projects. This extended abstract highlights their main features and provides pointers to published papers with more details. I. F-SOFT F-Soft is a platform for verifying source code programs [3], [4]. 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 assertions. It can be used to check programs globally, or as an annotation checker to check user-written contracts. We have successfully analyzed large benchmark examples to find previously unknown bugs