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 117
- Downloads 0
Vertical Clustering of 3D Elliptical Helical Data
This research proposes an effective vertical clustering strategy of 3D data in an elliptical helical shape based on 2D geometry. The clustering object is an elliptical cross-sectioned metal pipe which is been bended in t...
Implementation of an Efficient RBAC Technique of Cloud Computing in .Net Environment
Cloud Computing is flourishing day by day and it will continue in developing phase until computers and internet era is in existence. While dealing with cloud computing, a number of security and traffic related issues are...
An Effective Method of Eye Detection Using Segmentation and Projection
Face detection and eye detection has long been the subject of interest in practical implementation of image processing and vision. Moreover the exact pupil detection of eye is the cream of research as the basic step of r...
Optimizing Resource Allocation in IAAS Clouds
Cloud computing is a phenomenon which bestows new model of computing. It has various service modes. The service model which provides on-demand access to computing resources is known as infrastructure-as-a-service (IaaS)....
OSI Reference Model: An Overview
A reference model is a conceptual blueprint of how communication should take place. It addresses all the process required for effective communication and divides these processes into logical grouping called layers. When...