Computer systems are now widely used in our daily lives. From microwaves to vehicles, we can find computer chips providing various functionalities of the system. Defects in the design of such systems may incur devastating diasters or invaluable loss. Traditionally, experimental trials or simulation are used in detecting design flaws in systems. But these technologies can only find flaws when they find them. System developers will never know if the next trial or simulation will reveal design flaws. For critical systems such as air traffic controllers or medical devices, we would like to have more confidence in these systems. In Formal Verification Laboratory, we develop and apply formal methods to verify computer systems. Formal methods are mathematical theories that help designers develop computer systems correctly. We build design tools derived from these theories and prove system reliability mathematically. We are also interested in promoting formal verification in practical projects.
If you have any suggestions or comments, please contact web master.