| Faculty: | Gianfranco Ciardo | Professor |
| Students: | Galen Mecham | MS |
| Min Wan | PhD | |
| Jinqing (Andy) Yu | PhD | |
| Alumni: | Ming-Ying Chung | PhD (2007, University of California at Riverside) |
| Anwar Adi | MS (2006, University of California at Riverside) | |
| John Anderson | MS (2006, University of California at Riverside) | |
| Teddy Matinde | MS (2006, University of California at Riverside) | |
| Piyush Satapathi | MS (2006, University of California at Riverside) | |
| Honomount Rawat | MS (2005, University of California at Riverside) | |
| Paul L. Grieco | MS (2003, William and Mary) | |
| Robert M. Marmorstein | MS (2003, William and Mary) | |
| Radu I. Siminiceanu | PhD (2003, William and Mary) | |
| Robert L. Jones, III | PhD (2002, William and Mary) | |
| Arun S. Mangalam | MS (2000, William and Mary) | |
| Andrew S. Miner | PhD (2000, William and Mary) |
Both logic system verification and stochastic performance and reliability analysis of systems have strong theoretical underpinnings. However, the two have been traditionally relegated to separate research areas in computer science, the former focusing on logic and discrete algorithms (with ``yes-no'' answers), the latter focusing on exact or approximate numerical methods (with answers consistiting of probabilities, timings, and distributions).
In the last few years, though, there has been a convergence of research in these two areas, due to the realization that data structures used in one area can benefit the other and that, by merging the goals of the two areas, a more integrated approach to system analysis can be derived.
In our group, we have been focussing on symbolic, or implicit, techniques for the encoding of large discrete state spaces and transition relations (on the logic side) and large Markov chains (on the stochastic side).
Our tool, SMART (Stochastic Model checking Analyzer for Reliability and Timing) is the product of many years of research and implementation by current and past members of our group.