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 106
- Downloads 0
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...
Load-Balancing Multipath Switching System with Flow Slice
Load balancing plays a pivotal role in core routers as they need to handle multiple requests at a time. To achieve load balancing Multipath Switching Systems (MPS) are widely used. One of the challenging issues in buildi...
Classification of Diabetes Mellitus using Modified Particle Swarm Optimization and Least Squares Support Vector Machine
Diabetes Mellitus is a major health problem all over the world. Many classification algorithms have been applied for its diagnoses and treatment. In this paper, a hybrid algorithm of Modified-Particle Swarm Optimization...
Efficient Optimal Algorithm of Task Scheduling in Cloud Computing Environment
Cloud computing is an emerging technology in distributed computing which facilitates pay per model as per user demand and requirement. Cloud consist of a collection of virtual machine which includes both computational an...
Improved 3-Dimensional Security in Cloud Computing
Cloud computing is a trending technology in the field of Information Technology as it allows sharing of resources over a network. The reason Cloud computing gained traction so rapidly was because of its performance, avai...