Formal analysis is an invaluable tool for software engineers, yet state-of-the-art formal analysis techniques suffer from well-known scalability
limitations. Furthermore, creating accurate formal specifications can be a difficult and time-consuming task. These challenges conspire to limit the adoption of formal methods in the practice of software design, as real-world systems are both too large and too dynamic for analysis with state-of-the-art techniques. This presentation highlights new techniques which improve the scalability of applying formal analysis to real-world, dynamic software systems and explores avenues for future research in understanding how real-world software teams interact when developing software systems. Ultimately, improved scalability and understanding of developer behavior
will allow researchers to develop tools and techniques to enable large-scale, real-world application of formal methods through all phases of the software development lifecycle, including software architecture and design.
Clay Stevens is a Ph.D. candidate in computer science at the University of Nebraska-Lincoln, with an emphasis in software engineering. Prior to starting his Ph.D., Clay spent more than 13 years in industry as a professional software engineer and architect. His research aims are to scientifically study how software engineers and architects work in practice and to improve the scalability of rigorous formal analysis tools to enable their use on large-scale, real-world problems.