| Publisher | Microsoft | ||
|---|---|---|---|
| Format | 349.8KB PDF | Date added | 16 Jan 2007 |
| Topics | Object-Oriented, Programming Languages | ||
| Downloads | 106 | ||
This paper describes the program-verifier component of a verifying compiler for a core multi-threaded object-oriented language. The verifier takes as input a program written in the source language and generates, via a translation into an intermediate verification language, a set of verification conditions. The verification conditions are first-order logical formulas whose validity implies the correctness of the program. The formulas can be analyzed automatically by a Satisfiability-Modulo-Theory (SMT) solver. The paper defines the source language and intermediate language, the translation from the former into the latter, and the generation of verification conditions from the latter. The paper also builds a methodology for writing and verifying single- and multi-threaded code with object invariants, and encodes the methodology into the intermediate-language program.
Did you find this white paper useful?
24 out of 50 users found this white paper useful
Related white papers
Business Rules for Object-Oriented Projects
Managers and developers adopt object-oriented techniques, not for the benefits of the new technology, but for protection against the weaknesses of the old technology. They are usually seeking refuge from...
The Scoop on the New CCNA and CCNP Specializations
There has been a lot of interest among students lately on the details surrounding the CCNA specializations and their relationship with the corresponding CCNP specializations. These specializations were introduced in...
Leveraging the Model Driven Development and Software Product Line Engineering Synergy for Success
This report focuses on one of these integrations, the Rational Rhapsody/BigLever Software Gears Bridge. The Rational Rhapsody/Gears Bridge extends the abstraction, comprehension and communication benefits provided by model-driven development (MDD)...
Systems and Software Product Line Engineering with SysML, UML and the Rational Rhapsody/ Gears Bridge
One of the great challenges and opportunities in systems and software delivery today is Product Line Engineering - creating, evolving and maintaining a portfolio of closely related products with variations...
A Better Alternative: An Improved Approach to Facilities Management
Real estate is typically the second largest corporate expense after personnel, so why do so many organizations remain unchanged in the way they manage their facilities? Shouldn't they, and you,...
Model-Driven Development for the C Developer
C replaced assembler as the preferred language for embedded programming over ten years ago and with it came a huge increase in productivity. Today, Model Driven Development and UML offer...
Object Oriented Data Modeling for Data Warehousing
All are familiar with the growth rate of the public Web. Regardless of the metric used to measure its growth attached networks, servers, users or pages the growth rate continues...
