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 98
- Downloads 0
RW-Homeomorphism in Topological Spaces
A bijection f:(X,)→(Y, σ) is called regular weakly homeomorphism if f and f[sup]-1[/sup] are rw-continuous. Also we introduce new class of maps namely rw-homeomorphism. This class of maps is closed under composition of...
A Survey of an Adaptive Weighted Spatio-Temporal Pyramid Matching For Video Retrieval
Recently, in the field of video analysis and retrieval Human action recognition in video is an important research and challenging topic. An efficient video retrieval is needed to search most similar and relevant video co...
Cluster Head Election and Multi Hop Using Fuzzy Logic for Wireless Sensor Network
A wireless sensor network (WSN) consists of such spatially distributed autonomous sensors(a device that is generally able to perform its task without being connected to the interrogation unit) to monitor physical or envi...
A Survey of Machine Learning Algorithm in Network Traffic Classification
Network Traffic Classification is an emerging research area and now a day the research is widely used in various activities such as intrusion detection system and for security purpose. Many of the protocols and proposed...
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...