Formal verification methods for OOPS 
Author Message
 Formal verification methods for OOPS

Here is a summary of the responses I got for my formal verifications
request in comp.lang.eiffel a little while ago plus a few other "useful

        Gary T. Leavens. Verifying object-oriented programs that
        use subtypes.  Technical Report 439, MIT, Laboratory for
        Computer Science, February 1989.

   This is a development by the University of Queensland's Computer Science
   Department.  It is a set of extensions to the Z specification language
   to allow for specifications of object-oriented programs and systems.  The
   main paper at present is:

        D.Carrington, D.Duke, R.Duke, P.King, G.Rose and G.Smith.
        Object-Z: An object-oriented extension to Z.  In Formal
        Description Techniques (FORTE'89).  North Holland, 1990.

   So far, work with Object-Z has mainly been from a specification rather
   than verification standpoint, but Roger Duke at the e-mail address
   above can tell you more about it.

3. Pierre America and Frank de Boer, now at the Eindhoven University of
   Technology, have developed formal proof systems for two object-oriented
   languages, a sequential and a parallel one. They use a kind of Hoare logic,
   where the language in which the assertions are written has been specially
   devised to deal with arbitrary pointer structures. Both systems have been
   proved to be sound and complete. Publications are on their way, but anyone
   who is interested can get the reports; just send your (ordinary mail)
   address to:

        Pierre America
        Philips Research Laboratories
        P.O. Box 80.000
        5600 JA Eindhoven
        The Netherlands

   Note: I have contacted Pierre, but haven't received any replies yet.


My honours project itself will not be available till the end of the year,
but I will endeavour to see that everyone who wants a copy gets one.
It is being modelled within "Functional Logic" and "Functional Set Theory",
which are local developments here at the University of Queensland.  My aim
is to add extra definitions and theories to deal with object-oriented
concepts.  Two of the introductory Technical Reports dealing with these
subjects are shown below:

        J.Staples, P.Robinson and D.Hazel, A Functional Logic for
        Higher Level Reasoning About Computation.  Tech. Rept No. 141,
        Key Centre for Software Technology, Dept. of Comp. Sci.,
        University of Queensland, December 1989.

        P.Henman and J.Staples, Introduction to Functional Set Theory,
        Tech. Rept No. 144, Key Centre for Software Technology, Dept. of
        Comp. Sci., University of Queensland, February 1990.

To find out more about these topics, contact John Staples:

If anyone has anything to add to the list above, pertaining to verification
of object-oriented programs, then contact me at the e-mail address below and
I will maintain a summary and post it regularly if there is a lot of demand.


||  Rhys Weatherley             |  University of Queensland,  ||


Wed, 18 Nov 1992 12:29:56 GMT  
 [ 1 post ] 

 Relevant Pages 

1. Formal methods for verification of OOPS

2. Formal verificatinon methods for OOPS

3. BACUP meeting: Formal Verification, Physical Verification; SourceLink

4. BACUP meeting: Formal Verification, Physical Verification; SourceLink

5. Functional programming languages & formal verification

6. IBM/Israel: Open Positions in Functional Formal Verification

7. Scientific puzzle of formal circuit verification at next week's DAC

8. Formal verification of one-hot state machine.

9. Formal Verification

10. Formal verification

11. Formal verification and Static Timing

12. Advertisement: EDA Jobs (Formal Verification)


Powered by phpBB® Forum Software