Formal Methods Research at Carnegie Mellon University
Research in formal methods is concerned with the development and use of mathematically-based languages, techniques, and tools to support the specification and verification of software and hardware systems.
group photo

A couple of informal poses.

Faculty
Randal Bryant Formal verification of microprocessors, arithmetic circuit verification, symbolic manipulation of boolean and other discrete functions.
Edmund Clarke Model checking, real-time systems, hybrid systems, SMV, Verus.
David Garlan Software architecture, formal specification, software development environments, ABLE, ACME, Wright.
Jeannette Wing Specification languages, design and protocol analysis, programming languages, distributed systems, security, survivable systems.
Visitors
Michael Loui
Graduate Students
Sergey Berezin
Sagar Chaki
Pankajkumar Chauhan
Yirng-An Chen
Alex Groce
Anubhav Gupta
Rune Jensen
Rob O'Callahan
Manish Pandey
Sanjit Seshia
Oleg Sheyner
Joao Sousa
Bridget Spitznagel
Projects
Model Checking Finite state machine analysis. Hardware and protocol verification.
Information Assurance Survivability analysis of systems.
Wright A formal architectural description language.
Related Carnegie Mellon Projects
Composable Systems: Software engineering.
POP Group: Semantics of programming languages.
TinkerTeach: Educational infrastructure.
Local Activity
Sending to the email alias formal-methods@cs.cmu.edu reaches all current Carnegie Mellon faculty, visitors, postdocs, and students listed above.

Formal Methods: State of the Art and Future Directions, Edmund M. Clarke and Jeannette M. Wing, report by the Working Group on Formal Methods for the ACM Workshop on Strategic Directions in Computing Research, ACM Computing Surveys, December 1996. Also CMU-CS-96-178.

Worldwide Formal Methods Activity
Oxford University's Formal Methods home page.

previous next csd home Maintained by Jeannette Wing (wing@cs.cmu.edu)