Requirement and Result of Verifying the Program Code
Journal Title: INTERNATIONAL JOURNAL OF COMPUTER TRENDS & TECHNOLOGY - Year 2014, Vol 9, Issue 2
Abstract
The verification of Java/C++ codes is critical, especially for special projects where human life will be at stake. A system is required that uses integrated reasoning to split each verification condition into a conjunction of simpler sub formulas, then apply a diverse collection of specialized decision procedures, first-order theorem proves, and, in the worst case, interactive theorem proverbs to prove each sub formula. There exist some commercial tools for the verification of Java/C++ code such as Jahob. However, none of the commercially available tools does a good job a finding bugs dealing with concurrency. Most of them are focusing on testing (test drivers, test cases), and, some are using more advanced techniques such as static analysis (Co verity, Klocwork, PolySpace, Code Sonar to name only a few).Techniques such as replacing complex sub formulas with stronger but simpler alternatives, exploiting structure inherently present in the verification conditions, and, when necessary, inserting verified lemmas and proof hints into the imperative source code make it possible to seamlessly integrate all of the specialized decision procedures and theorem proverbs into a single powerful integrated reasoning system. By appropriately applying multiple proof techniques to discharge different sub formulas, this reasoning system can effectively prove the complex and challenging verification conditions that arise in this context.
Authors and Affiliations
Er. Abhishek Pandey , Prof. Roshni Dubey
Keywords
Related Articles
- EP ID EP157682
- DOI -
- Views 110
- Downloads 0
A Review of Cyber Attack Classification Technique Based on Data Mining and Neural Network Approach
Cyber attack detection and classification is major challenge for web and network security. The increasing data traffic in network and web invites multiple cyber attack. The dynamic nature and large number of attribute of...
Performance Evaluation of VOIP over Multi Radio Multi channel Network
Wireless mesh network is an advanced form of wireless network. A wireless mesh network provides a better solution to problems that often arise in cellular and WLAN. Wireless mesh networks (WMNs) are receiving increasing...
A Tree of Life Approach for Multidimensional Data
With the recent exponential growth of ICT, there is explosive growth of data of varied nature. Human effort is always to efficiently store the data for the current and future usages. In the present day, we create data wi...
An Efficient Boundary Detection and Image Segmentation Method Based on Perceptual Organization
In this paper, we presents a novel method for detecting the boundaries of the object in outdoor images by using most common properties of the images such as perceptual organization laws. Here the proposed segmentation sc...
Revival of Secure Top-k Multi-Keyword over Encrypted Cloud Data
Cloud computing has recently emerged as a new platform for deploying, managing, and provisioning large-scale services through an Internet-based infrastructure. However, concerns of sensitive information on cloud potentia...