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 112
- Downloads 0
A Novel Routing Protocol for Providing Anonymity in MANET
Mobile Ad Hoc Networks (MANETs) using anonymous routing protocols hidden node identity and external routes having anonymity protection. Anonymous routing protocols use either hop-by-by hop encryption or redundant traffic...
Securing ATM Using Graphical Password Authentication Scheme
In our day to day life ATMs are widely used and have brought so much relief to the financial world. Various problems were solved with the advent of these machines ranging from keeping the banking hall free of traffic wit...
Cluster Based Secure Data Broadcast of CLAODV Protocol for MANET
Ad-hoc Networks are using multicast protocol to broadcast the messages. Multicast authentication in ad-hoc networks are very challenging based on below mentioned multiple factors such as nodes have limited computing, ban...
A Novel Encryption and Extended Dynamic Histogram Shifting Modulation for Reversible Data Hiding in Encrypted Image
Recently, progressive interest is paid to reversible data hiding (RDH) in encrypted images, since it preserves the original cover can be recovered without any loss after embedded data is extracted to protect the con?den...
Hardware and Software Interface for Luminescence Measurements
This Paper deal with the hardware and software interface for the Luminescence measurements Luminescence is one of the oldest know phenomenon, but its systematic study started only between eighteenth and nineteenth centur...