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 108
- Downloads 0
Study of TCP Packet Labeling to Alleviate Time-Out
Many applications (e.g., cluster based storage and Map Reduce) in modern data centers require a high fan-in, many- to-one type of data communication (known as TCP in cast), which could cause severe in cast congestion in...
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...
Impact of DDoS attack in Online Auction System and Proposed Lightweight Solution Based on Software Agent
The Denial of Service attack, in particular the Distributed Denial of Service (DDoS) attack, has become one of the key intimidations to the Internet. In general, attackers launch DDoS attacks by directing an enormous num...
Statistical Anomaly Detection Technique for Real Time Datasets
Data mining is the technique of discovering patterns among data to analyze patterns or decision making predictions. Anomaly detection is the technique of identifying occurrences that deviate immensely from the large a...
Information Extraction using Incremental Approach
Data mining is playing vital role in text extraction as now a day’s large amount of data available in scientific research, biomedical literature and web data. Data retrieval using existing approaches use sequential appro...