HCSS Formal Methods Education Panel

  H C S S   F O R M A L   M E T H O D S   E D U C A T I O N   P A N E L  

Moderator

Perry Alexander is the AT&T Foundation Distinguished Professor of Electrical Engineering and Computer Science and director of KU’s Information & Telecommunication Technology Center. His research interests include system-level modeling, formal verification, language semantics and trusted computing. Prior to joining KU, he was a faculty member and director of the Knowledge-Based Software Engineering Laboratory in the Department of Electrical and Computer Engineering and Computer Science at the University of Cincinnati. Alexander has been principal or co-principal investigator on more than $38 million in research projects funded by agencies such as the Defense Advanced Research Projects Agency, National Security Agency, National Science Foundation, Air Force Research Laboratory and NASA. He currently leads KU’s NSA Science of Security Lablet, the DARPA-funded KU Cyber-Assured Systems Engineering program and the Ripple University Blockchain Research Initiative gift. Alexander has published more than 120 refereed research papers and is author of “System-Level Design Using Rosetta.” He received two bachelor’s degrees, a master’s degree and a doctorate from KU, all in the areas of electrical engineering and computer science.



 

Panelists

Kevin Hamlen is the Louis A. Beecherl, Jr. Distinguished Professor in the Computer Science Department at The University of Texas at Dallas, and the Executive Director of the Cyber Security Research and Education Institute. His research applies and extends compiler theory, functional and logic programming, and automated program analysis technologies toward the development of scientifically rigorous software security systems. Over the past ten years his work has received over $20 million in federally funded research awards, including the National Science Foundation CAREER award and the Air Force Office of Scientific Research Young Investigator Award. His research on secure binary retrofitting, reactively adaptive malware, and software cyber-deception has received six best paper awards, including two CSAW Best Applied Security Paper of the Year prizes and the NSF IUCRC Technology Breakthrough award, and has been featured in thousands of news headlines worldwide, including The Economist and New Scientist. Dr. Hamlen received his Ph.D. and M.S. degrees from Cornell University, and his B.S. from Carnegie Mellon University, where his work on proof-carrying code earned the Allen Newell Award for Excellence in Undergraduate Research.

Download Presentation (You must register and request HCSS Community Membership to download the slides.)

Marijn Heule is an Associate Professor at Carnegie Mellon University and received his PhD at Delft University of Technology (2008). His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning SAT solvers and his preprocessing and proof producing techniques are used in many state-of-the-art solvers.

Pete Manolios is is a professor in the Khoury College of Computer Sciences at Northeastern University and leads the computer-aided reasoning group. What guides his research is the vision that formal methods can be used to revolutionize the design, analysis, and implementation of highly reliable, robust, and scalable systems in a variety of important application areas, including large component-based software systems, hardware systems, aerospace systems, and big data analytics. His group has been funded by DARPA, NASA, NSF, Boeing, BAE, AFRL, IBM, and SRC. Additionally, the group has developed several publicly available tools, including ACL2s, BAT, CoBaSA/Inez, 3SPIN, 3Murphi, and the Bloom Filter Calculator. Manolios is also an active consultant in the area of safety critical systems and DO-178C certification.

Download Presentation

Yan Shoshitaishvili is an assistant professor at Arizona State University, where he pursues research in automated program analysis and vulnerability identification techniques. As part of this, Yan led Shellphish's participation in the DARPA Cyber Grand Challenge, applying his research to the creation of a fully autonomous hacking system that won third place in the competition. Underpinning this system is angr, an open-source binary analysis project created by Yan (and others!) over the years. When he is not doing research, Yan is pushing the area of cybersecurity competitions into the future from his position on the Order of the Overflow, the organizers of DEF CON CTF.