Courses Developed and Taught by Prof. Janusz Laski  
STAD, OU - Prof. J. Laski & P. Luczycki
Procomp, OU - Prof. J. Laski & W. Szermer & W.F. Stanley
 
Swat, Softools Inc.,
 
Short Introduction to VDM-Tools
 
Short Introduction to Spark Systems
 
back to courses

     

CSE 438/538


VERIFICATION

 		     
  

 OF COMPUTER 

 		  
     

 PROGRAMS 


Instructor: Prof. Janusz Laski

Course Outline.
The objective of the course is to introduce students to language-independent
systematic methods of program verification, analysis, testing and debugging.
The course consists of three main parts: Static Program Analysis, Dynamic
Program Analysis and Formal Software Verification, the first two representing
software engineering approach to software Quality Assessment. Most of the
course consists of lectures by the instructor and discussions of the assignments.

There are two exams (midterm and final) and five to six assignments during
the course. The following software tools are used in the course: SPARK,
a Safety Critical subset of Ada (Static Analysis, Formal verification)
and STAD 1.0, a System for Testing And Debugging developed at OU (static
analysis and testing). The former is installed in the EDS Software Testing
and Verification Laboratory (101 SEB) while the latter can be installed on your
personal computers. If the class is small, a presentation to the class can be
required in lieu of one assignment.

Text: There is no single text that covers all topics in the course.
Therefore, a course pack material has been compiled and is available in the
Bookstore. Although the pack looks somewhat formidable, only parts of the
enclosed papers are actually used. However, you are welcome to consult
the following books:

  1. John Barnes, “High Integrity Ada, The SPARK Approach,”
    Addison-Wesley 1997. This text deals with some aspects of
    static analysis and practical verification methods for safety
    critical software.
  2. Boris Beizer, "Software Testing Techniques," Van Nostrand, 1990.
    This (huge) text covers main issues in software testing, albeit in a
    too loose form.

Topics (tentative, might change depending on class size and progress made)
  • Static Program Analysis
    • Information Flow Relations
    • Program flowgraphs
    • Call graphs
    • Control and data flow anomalies
    • Dependencies
    • Program slicing
  • Dynamic Program Analysis
    • Black-Box and Structural Testing
    • Coverage monitors
    • Test case synthesis
    • Regression testing
    • Slicing
  • Formal Verification
    • Specification
    • Program correctness
    • Inductive assertions
    • Proofs


    Prerequisites: CSE 262, APM 263, Major Standing.

    To see a sample of typical assignments, see CSE438/538.ASSIGNMENTS.