Computer science colloquia: Andy Miner
| Date/Time: | Thursday, 08 Nov 2012 at 3:40 pm |
|---|---|
| Location: | B29 Atanasoff Hall |
| Cost: | Free |
| Phone: | 515-294-6516 |
| Channel: | College of Liberal Arts and Sciences |
| Categories: | Lectures |
| Actions: | Download iCal/vCal | Email Reminder |
Today's applications increasingly rely on multi-threaded and
multi-process solutions, especially in communication networks. But designing algorithms with multiple concurrent processes, that work correctly, is difficult. Model checking is an important tool that can help algorithm designers discover race conditions, deadlocks or other undesirable behaviors. The main challenge of this approach is that a real system to be analyzed will often produce a model that is too large for model checking tools to handle. This talk gives a brief overview of research areas in model checking. Also discussed are some methods that address the size problem, with an emphasis on "symbolic" approaches, which utilize a clever data structure called decision diagrams.