USC Center for Software Engineering Presents

Los Angeles

Software Process Improvement Network


Wednesday, Dec. 1, 5:30 P.M. to 8:30 P.M.


"Formal Methods Used in for Practical Software Verification"


Speaker:  Robert T. Bauer, IBM


In the formal methods community, software verification means to prove that a given software system is correct with respect to its specification.  Engineers and managers in software Quality Assurance (QA) and Quality Engineering (QE) have a different problem:  Increasingly complex software that needs to be "tested" in ever decreasing amounts of time.  Even if you prove that some software system is correct (with respect to its specification), you still need to test the software system.  This does not mean that the techniques of formal methods are "orthogonal" with those used by QA/QE teams.  It means that QA/QE teams will be more effective if they understand the ideas and limitations of formal methods.  QA/QE teams can incorporate many of the concepts and even the techniques themselves within the test environment.


While many practices of formal methods are quite mathematical and complicated, the techniques themselves are quite simple.  This talk gives a high-level overview of these techniques and shows how they apply at a very practical level to the problems faced by QA/QE teams.


Robert T. Bauer has over 15 years of industry experience.  He has worked in research labs and in real-world business application development.  At Quantum Dynamics' Advanced Experimental Research Laboratory, Robert developed the real-time kernel for NASA's Cryogenic Orbital Depot Satellite.  At PDS, he developed inventory, order processing, shipping and customer service applications to support a full-service fulfillment center.  At 1776, Robert developed fault-tolerant disk array software and at NCR, he developed a wide-variety of software to support large-scale testing of the Teradata database.  His Parallel Test Environment (PTE) is now the standard testing environment at NCR and is used at the 5 Teradata development centers.  He began working in formal methods at NCR and continued that work at Levetate where he worked on the semantics of a behavioral specification language and developed a theorem prover for automated formal verification.  Robert is now with IBM where he spends most of his time working on design pattern software and on formal methods related work.


Robert is well-known in the software quality community for his contributions to software testing.  Robert developed a testing strategy called Customer-Based Testing.  This strategy combines software reliability engineering, automatic test case generation, and usage coverage to minimize the risk of expensive failures and maximize assurance of base functionality.  Robert introduced Early Regression Testing.  At NCR, early regression testing moved 70% of the problems discovered at system test to feature/unit testing.  Robert has undergraduate degrees in Electrical and Industrial Engineering and a graduate degree in Computer Science. 


*** Recheck the web site before the meeting ***

Location:  University of Southern California - Information Sciences Institute

11th Floor Conference Room, 4676 Admiralty Way, Marina Del Rey, CA  90292-6601

Map and directions at | Directions


5:30 to 6:00  Networking

7:00 to 7:30  Networking

6:00 to 7:00  Presentation

7:30 to 8:30  Presentation cont’d


No reservations needed.  Free parking in nearby structure, bring ticket to meeting for validation.

For additional information: or