skip to main content
Department of Computer Science University of Colorado Boulder
cu: home | engineering | mycuinfo | about | cu a-z | search cu | contact cu cs: about | calendar | directory | catalog | schedules | mobile | contact cs
home · events · colloquia · 1998-1999 · 

Colloquium - Chan

ECCR 265

Symbolic Model Checking for Large Software Specifications: Case Studies, Optimization, and Extension
University of Washington

Despite its tremendous success in locating bugs in hardware circuits, symbolic model checking has rarely been applied to software. The prevalent view is that the symbolic representations used in model checking, such as binary decision diagrams (BDDs), cannot capture the complexity inherent in most software systems. Contrary to this belief, I will present some results and experience in applying the technique to the statecharts specifications of two industrial software systems: a collision-avoidance system used on most commercial aircraft and an electrical power distribution system on Boeing 777.

Using symbolic model checking, I have discovered subtle but important errors not found in prior verification efforts. Although the final results are encouraging, initially many of the analyses were infeasible because of the huge BDDs generated. I have developed intuition about some factors that can cause BDD blowup, and based on the insights, devised optimization techniques to improve the efficiency of the analyses by orders of magnitude. These optimizations have made feasible certain analyses that were previously intractable. Another limitation of the existing techniques was the inability to handle complicated arithmetic. To attack the problem, I have extended the conventional model-checking algorithm by coupling BDDs with a constraint-satisfaction engine.

Hosted by Kenneth Anderson.
Refreshments will be served immediately following the talk in ECOT 831.

The Department holds colloquia throughout the Fall and Spring semesters. These colloquia, open to the public, are typically held on Thursday afternoons, but sometimes occur at other times as well. If you would like to receive email notification of upcoming colloquia, subscribe to our Colloquia Mailing List. If you would like to schedule a colloquium, see Colloquium Scheduling.

Sign language interpreters are available upon request. Please contact Stephanie Morris at least five days prior to the colloquium.

See also:
Department of Computer Science
College of Engineering and Applied Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
Send email to

Engineering Center Office Tower
ECOT 717
FAX +1-303-492-2844
XHTML 1.0/CSS2 ©2012 Regents of the University of Colorado
Privacy · Legal · Trademarks
May 5, 2012 (13:29)