Randal Bryant - US grants

This research is on symbolic simulation as a basis for formally verifying complex IC designs. Symbolic simulation differs from classical simulation in that during simulator operation the user can set inputs not only to 0 or 1 but also to Boolean variables. The research exploits existing simulation technology by taking a behavioral approach to circuit verification. In this, the verifier applies logic simulation to compute the circuit's response to a series of stimuli chosen to detect all possible design errors. Research tasks include: selecting a set of simulation patterns which can defeat a malicious adversary attempting to foil the verifier; determining structures and algorithms, based on binary decision diagrams, for manipulating Boolean formulas; and investigating the use of the simulation system as an aid to debugging and design.

Binary Decision Diagrams (BDD's) have found widespread use in synthesis, formal verification and testing of digital circuits. This success in the EDA research area has spawned research efforts on a number of fronts, including theoretical studies of algorithms and complexity, applications to such areas as artificial intelligence and logic programming, and extensions beyond Boolean functions to represent matrices, Markov systems, and multi-variate polynomials. This workshop (February 13-17, 1995) is the first ever held specifically on this important technology.

The research seeks to extend the effective use of binary decision diagrams (BDDs), which have already proved an effective method for symbolically representing and manipulating Boolean functions. A number of researchers worldwide have found novel applications of BDDs to such areas as synthesis, formal verification, and testing of digital circuits. Extensions to allow more compact forms and to represent the behavior of arithmetic circuits have improved the performance and extended the range BDDs, leading to a broader class of those diagrams. The U.S. and German group collaborating in this effort have had a synergistic relationship, with each group building on the work of the other. This new effort will enable a more formal collaboration between the two groups.

Algorithms on graphical structures play a central role in both communications technology and formal verification. Minimal trellises are graphical representations of error-correcting codes that have emerged as a unifying framework for understanding and manipulating codes of all types. Ordered binary decision diagrams and their variants are graph-based data structures for representing Boolean functions that have found widespread use in formal verification for a range of problems, including circuit checking, logic synthesis and test generation. This project builds on the close correspondence that has recently been established between the code trellis and binary decision diagram, and investigates the transfer of ideas between these previously disparate fields. The fundamental challenge that confronts both uses of graphical methods is the same: devise techniques to combat the exponential blowup in the size of the graph. The research is interdisciplinary, and can be expected to have a broad range of application, both within coding and verification, as well as to such areas as artificial intelligence, database search, and combinatorial optimization.

This research project is developing a new generation of formal verification tools that can be integrated into design environments for the complex, high-assurance embedded and autonomous systems of today and of the future. Such systems are increasingly distributed, complex, and dynamic; they must operate with a high degree of autonomy and survivability in diverse and unpredictable environments. This project will focus on the development of new verification methods and tools to provide a rigorous means for checking the integrity and correctness of designs for these systems before they are deployed. The project has two broad research thrusts:

1. Verifying System Integrity. System integrity refers to correctness with respect to the interactions among the distributed software and hardware components. Systems must satisfy synchronization, resource, and real-time constraints imposed by the implementation architecture and application requirements. This project will extend automated verification methods that have been successful in hardware and protocol applications to their use with embedded and autonomous systems.
2. Modeling the Environment. Embedded and autonomous systems must interact in complex ways with physical systems and adverse environments. It is thus essential to capture correctly and effectively the continuous dynamics, feedback loops, and unpredictable features of the environment in the models used for formal verification. This project will draw on recent developments in hybrid system verification to integrate continuous state dynamics with discrete-state models used in formal verification.

This project develops and evaluates a system for assessing proofs in undergraduate mathematics and computer science classes via peer evaluation. It approaches the problem as an instance of human computation, using computer technology to harness the collective capability of large numbers of people to do useful work. This requires breaking down the task of assessing a proof to make it possible for multiple, nonexpert people to contribute to the assessment. It requires instituting mechanisms to ensure the quality, uniformity, and integrity of the assessment process. The work builds on previous experience with a prototype system that had been used for two years in computer science and mathematics courses that targeted handling large classes using teams of undergraduate graders. Experience indicated the feasibility of the basic strategy, while this project works to ensure the quality of the assessments and of the learning experience for the assessors. In addition, this project takes initial steps toward an assessment system that can scale to support web-scale courses.

This work creates structured frameworks in which to analyze proofs, so that assessment can be decomposed into a number of tasks, suitable for nonexperts. It explores ways to maximize the learning experience students gain by critically evaluating each other's proofs. It creates a platform for performing quantitative experiments on the most effective methods for teaching students how to read and evaluate proofs.

The goal of the Carnegie Mellon University (CMU) I-Corps Site, led by the campus-wide Carnegie Mellon Center for Innovation and Entrepreneurship (CIE), is to implement a systematic and replicable agile startup methodology, focused on customer discovery and product adaptation.

The CMU I-Corps Site leverages Carnegie Mellon's strengths and past successes in fusing technology with entrepreneurship. Their Site utilizes CMU's network of internal and external contacts to train entrepreneurial faculty and student teams working in STEM fields. CMU's curricular model is based on the i6 Agile Innovation System and is consistent with the I-Corps Curriculum. It includes four elements: workshops, mentoring, funding for projects and customer discovery, and incubator space.

The objectives of the CMU Site are to:
1) capitalize on CMU's culture of innovation by expanding programs to nurture entrepreneurial ventures and transition university research to the market;
2) train individuals to understand basic motivations, processes, practices, and challenges of innovation and entrepreneurship;
3) hone individuals' entrepreneurial practices and skills;
4) collaborate with industry, entrepreneurs, and the business community in the region and nation.

The CMU program will recruit teams from: existing entrepreneurial activities, course projects, college liaisons, and an open call. Underrepresented groups will be especially encouraged to apply. Teams will be encouraged to avail themselves of enrichment opportunities such as funding avenues, venture competitions, and business events. Each team will have an Entrepreneurial Lead, an Academic Lead, and a Mentor.

The assessment plan focuses on ascertaining the most effective components of an agile university entrepreneurship training program. Teams' milestones and customer contacts will be tracked. Formative assessment using tools such as pre-, mid-, and post-program surveys will inform the CMU program evolution.

Of particular merit is this proposed Site's agile and adaptable customer-based training program, components of which have been shown to be successful in programs such as the i6 Agile Innovation System and the I-Corps Curriculum/Lean Launch Pad. Combining these components -- and then distilling through assessment and evaluation which of them are especially effective at spurring creativity, resourcefulness, independence, and connectivity -- will further entrepreneurial knowledge and education. The program will also teach entrepreneurial students and faculty how to create their own ecosystem by engaging in customer discovery and network building.

The CMU I-Corps Site plans to move university research out of the lab more efficiently and effectively. Expediting the movement of academic innovation to the commercial sector allows new, often government-funded, university discoveries and inventions to reach the public sector earlier spawning new endeavors and economic growth. All sectors of society and areas of inquiry -- healthcare, energy, sustainability, global communication, for example, can see benefits. In addition, making earlier decisions about viability of commercial outcomes is beneficial as it can more effectively utilize critical resources --time, energy, talent, and funds. In addition, a successful Site will likely impact the Pittsburgh, Steel Valley, and Allegheny Valley communities.

There is a growing need for techniques to detect security vulnerabilities in hardware and at the hardware-software interface. Such vulnerabilities arise from the use of untrusted supply chains for processors and system-on-chip components and from the scope for malicious agents to subvert a system by exploiting hardware defects arising from design errors, incomplete specifications, or maliciously inserted blocks. This project addresses the problem by developing foundational techniques and tools for formal and semi-formal specification and verification of security properties of hardware.

This project addresses gaps in the current specification and verification processes for hardware designs. Given a design and a (possibly informal) specification, the approach first identifies signals that correspond to high-integrity or confidential parts of the design, such as privileged mode flags or secret keys. The approach uses this information to perform critical signal analysis, specification generation, security-aware specification analysis, and test characterization and augmentation. These steps are iterated until a suitable level of security assurance is attained. The methods build upon formal computational engines for Boolean reasoning, symbolic simulation, and model checking. The project is evaluated using case studies based on processor cores and non-processor blocks, where each case study includes both offensive and defensive components. Tangible results will include theories, threat models, software tools, benchmarks, and case studies. Results from the project are incorporated into courses and textbooks written by the PIs to teach students how to design systems with a security mindset.

Due to the pandemic and the resulting uncertain circumstances, academic institutions are facing major hiring disruptions. This leaves the computing research community at risk of losing yet another class of young researchers who cannot afford to wait out the current disruption and thus may leave the research career path permanently. It is not a stretch to anticipate that the loss of this workforce in the research pipeline will have long-lasting downstream effects on computing innovation and impact. The Computing Innovation Fellows (CIFellows) Program addresses these issues by providing funding for two-year postdoctoral positions for recent PhD graduates in computer information science and engineering to provide a career-enhancing bridge experience that will give them the opportunity to remain in the academic research community and retain a cohort of early career professionals in areas under the umbrella of NSF CISE.

With funding by the National Science Foundation, the CIFellows 2021 program will offer two-year postdoctoral opportunities in computing, with cohort activities to support career development and community building. This program is open to researchers whose work falls under the National Science Foundation Computing and Information Science and Engineering Directorate and who have completed or plan to complete their PhD between 1/1/20 - 12/31/21. Applicants will work with a mentor from a US academic institution for their postdoc.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.