As an active and contributing member of the formal methods community the National Science and Technology Council's Special Cyber Operations Research and Engineering Subcommittee would like to invite you to attend a one-day meeting to discuss successes and barriers, opportunities and challenges, in the (accelerating) use of formal methods in cyber systems. This one-day meeting will convene a by-name group of experts to discuss technical areas to include formal methods logics, tools, and ecosystems, as well as to consider more broadly their related evaluation and use. Ultimately the meeting discussions and summary reporting is meant to encourage understanding of how the formal methods community might achieve the use of this critical technology at scale.
We recognize that there are multiple dimensions of scale that we will need to address. These include, for example: (1) the range of properties and qualities that are modeled and reasoned about, such as relating to security, safety, performance, fault tolerance, real-time, etc., (2) complexity and the size of systems and their supply chains, including issues related to composability (3) efficiency of FM-related modeling, tooling, and engineering practices, including integration into mainstream tooling and practices, (4) ability to rapidly co-evolve systems and associated evidence, (5) ease of use for non-expert developers and evaluators.
We are also interested in addressing the different dimensions of experience that we can share. Discussion of these experiences can help ground our conversation, and help us understand cross-cutting considerations such as commonalities in technical foundations, and challenges relating to adoption into practice and tooling. Some kinds of experiences we can share include: (1) applications to specific major systems in government and industry, (2) tour-de-force results, such as proofs of significant mathematical results or reasoning about modern processors, (3) the advancement of formal methods ecosystems surrounding the various provers and stacks, (4) integration of more limited capabilities into broader communities of practice, such as has been happening in major tech firms.
As a participant in this meeting we would ask that you submit, in advance of the meeting, a short abstract summarizing your position on the theme of achieving formal methods at scale.
Attendance at the one-day meeting is by invitation only and limited because of time and space constraints. We will convene on the morning of September 25th, 2019 at SRI Rosslyn. To accept our non-transferrable invitation, please register by June 12th with the code provided in the invitation email. Limited travel support is available for non-government participants.
A separate one-day meeting will be held on the West Coast on October 9. If you are unable to attend the East Coast meeting but are available for the West Coast meeting please email the organizers. We will do our best to accommodate your request.
If you have any questions, please contact the organizers: FMatScale@cps-vo.org
Meeting Sponsor
Brad Martin
Co-Chairs
Patrick Lincoln, SRI International
William Scherlis, Carnegie Mellon University
Patrick Lincoln, Ph.D., is director of the Computer Science Laboratory at SRI International. He is also the executive director of SRI's program for the Department of Homeland Security’s Cyber Security Research and Development Center and director of the SRI Center for Computational Biology. Lincoln leads research in the fields of formal methods, computer security and privacy, computational biology, scalable distributed systems, and nanoelectronics.
He has led multidisciplinary groups conducting high-impact research projects in symbolic systems biology, scalable anomaly detection, exquisitely sensitive biosensor systems, strategic reasoning and game theory, and privacy-preserving data sharing. He has published dozens of influential papers, holds several patents, has served on scientific advisory boards for private and publicly held companies, nonprofits, and government agencies and departments.
Lincoln holds a Ph.D. in computer science from Stanford University and a B.Sc. in computer science from MIT. He has previously held positions at MCC, Los Alamos National Laboratory, and ETA Systems.
Lincoln was named an SRI Fellow in 2005.
William L. Scherlis is a Professor of Computer Science and director of CMU's Institute for Software Research (ISR), one of seven academic departments in the School of Computer Science (SCS). ISR research and educational programs relate to software development, cybersecurity, privacy engineering, Internet of Things, network analysis, mobility, systems assurance, and other topics. ISR is home to two PhD programs and three professional Masters programs. Scherlis founded the PhD Program in Software Engineering in 1999 and directed it for more than a decade. During 2012 and early 2013 he was the Acting CTO for the Software Engineering Institute, a Department of Defense FFRDC at CMU.
Scherlis joined the Carnegie Mellon faculty after completing an A.B. magna cum laude at Harvard University in applied mathematics, a year in the Department of Artificial Intelligence at the University of Edinburgh (Scotland) as a John Knox Fellow, and a Ph.D. in computer science at Stanford University (Zohar Manna advisor). His research relates to software assurance, cybersecurity, software analysis, and assured safe concurrency. His team has developed analysis tools based on techniques to verify safe concurrency, information flow, and other properties that tend to defy conventional testing and heuristic analysis. He has led several large research projects including the National Security Agency Science of Security Lablet at CMU since its inception in 2011 and, previously, the Carnegie Mellon / NASA High Dependability Computing Project (HDCP).
Scherlis has testified before Congress on federal software sustainment, on computing technology and innovation, and on roles for a Federal CIO. He interrupted his career at CMU to serve at Defense Advanced Research Projects Agency (DARPA) for more than six years, departing in 1993 as a federal senior executive. At DARPA his responsibilities related to research and strategy in software technology, computer security, information infrastructure, and other topics. He participated in the initiation of the high performance computing and communications (HPCC) program (now NITRD) and in defining the concept for CERT-like security organizations, hundreds of which now operate in more than 90 countries world-wide.
Scherlis has led multiple national studies including the National Research Council (NRC) study committee that produced the report Critical Code: Software Producibility for Defense in 2010. He served multiple terms as a member of the DARPA Information Science and Technology Study Group (ISAT). He has been an advisor to major technology firms, defense companies, and venture investors, and is a co-founder of Panopto, a CMU spin-off. He has served as program chair for a number of technical conferences including the ACM Foundations of Software Engineering (FSE) Symposium and the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM).
He is a Fellow of the IEEE and a Lifetime National Associate of the National Academy of Sciences.