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 88
- Downloads 0
Aligning Cloud Computing Security with Business Strategy
These days, the technological growth in the IT sector is rapid. Cloud computing is also one of the new technologies that have both benefits and limitations. This paper gives an overview of how cloud computing can be help...
A survey on Human Computer Interaction Mechanism Using Finger Tracking
Human Computer Interaction (HCI) is a field in which developer makes a user friendly system. User can interact with a computer system without using any conventional peripheral devices. Marker is used to recognize hand mo...
Deriving the Probability with Machine Learning and Efficient Duplicate Detection in Hierarchical Objects
Duplicate detection is the major important task in the data mining, in order to find duplicate in the original data as well as data object. It exactly identifies whether the given data is duplicates or not. Real world du...
Improved Discretization Based Decision Tree for Continuous Attributes
The majority of the Machine Learning and Data Mining applications can easily be applicable only on discrete features. However, data in solid world are sometimes continuous by nature. Even for algorithms that will directl...
A Survey on Mobility Management Protocols for Improving Handover Performance
The wireless and mobile communication systems have enormous growth in recent years because many people use mobile devices for acquiring different services like browsing, multimedia applications and file sharing etc. Mobi...