Bor-Yuh E. Chang, Ph.D. - US grants

This EAGER grant explores early concepts of a new approach to computer programming. The semantic gap between what the programmer intends and what the code actually means significantly impedes efforts to improve programmer productivity, software reliability, and execution efficiency. To address the semantic gap, the project radically rethinks how to develop software. A new programming model, methodology, and system for ?gradual programming? will support the development of programs and programming language semantics in parallel. The vision advocates developing programs in a family of languages with varying semantics. Then, part of the development process involves nailing down the precise semantics of the program. A key issue involves the tradeoffs between expressiveness of a programming language and the ability to build tools capable of statically checking for programming errors. Such a vision is not without significant challenges and possible pitfalls, such as maintaining performance, and entrusting issues of programming language design to programmers. The project will study the sources of the semantic gap in the Java programming language to understand the problem better and articulate the approach more fully.

This travel grant requests funds to support graduate student travel to the Symposium on Principles of Programming Languages (POPL). This is a top conference in Computer Science for research and education in the core areas of Software and Hardware Foundations program. The funds enables students to hear the latest results in the field, meet established researchers, and build community with the next generation of researchers.

While not perfect, the depth and breadth of what today's automated analysis tools can figure out about a program is truly remarkable. Yet, despite the prevalence and cost of software defects and despite the wealth of information such automated tools could provide, program analyzers are largely ignored by today's software engineers. This situation is not due to a lack of interest from software engineers or a lack of effort in deployment from analysis experts but rather a gap in the way a tool and its user reasons about the program, which results in, for example, a difficulty in providing analysis results understandable to the user. This research confronts closing this user-tool reasoning gap.

The focus of the work is an effective approach to user-driven refinement of the analysis process. Novel techniques for generating explanations of program analysis results will be created. New approaches for trading off the exhaustiveness of compile-time verification and the simplicity of run-time checking will be developed. Together with prior work on user-centric analysis specifications, this project lays the foundation for tomorrow's tools where users and tools cooperate to reason effectively about programs. Significant potential impacts include the following: a change in the way software engineers view program analysis--replacing a magic box with a transparent reasoning assistant, improved software quality as a result of this change in view, and tools that engage students in algorithmic thinking in a hands-on manner.

As the internet and mobile devices become increasingly important
parts of our society, the need for web and mobile applications has
grown. Recent advances in software frameworks have drastically
reduced the amount of code needed to develop such applications. From a
programming languages perspective, the key enabling technology is
reflection, that is, the ability of a program to introspect and to
modify itself. Unfortunately, reflection comes at a heavy cost:
it can delay the detection of bugs, it reduces the effectiveness of
bug-finding tools, and it reduces the speed of applications. The
goal of this research project is to preserve the benefits of
reflection while eliminating the disadvantages, thereby improving the
reliability and speed of web and mobile applications.

The key observation that underlies this research is that uses of
reflection in software frameworks are governed by implicit
conventions. If those conventions could be made explicit, then
automated software tools will be able to effectively reason about
reflective code. This research will create a rich specification
language for making those conventions explicit, it will investigate
algorithms for inferring specifications from existing
application code, and it will develop tools for checking the
conformance of web-mobile applications and frameworks with respect to
specifications.

Increasingly, modern software on the web is richly extensible, accelerating its evolution and dramatically reducing the time between development and deployment. The intellectual merit of this research consists of challenging the false choice between creating software that is extensible (easy to reuse and extend) and software that is correct (meets its specifications). The new approach advanced by this work, Incremental Verification-Validation, enables programmers to bring domain-specific safely disciplines to extensible systems, by providing a framework where these disciplines are communicated both precisely and usefully, as executable code. The project's broader significance and importance consist in changing the way programmers approach building correct extensible software for the web. The research targets ECMAScript (JavaScript), enabling this research to have a direct impact on the vast number of languages and systems that create and use JavaScript. Further, the project represents a new collaboration across the University of Colorado and University of Maryland, bringing together experts across verification, incremental computing, and runtime systems. Finally, this project benefits the graduate and undergraduate teaching mission at the participating universities, as aspects of the project enriches the program analysis and programming language courses.

Incremental Verification-Validation encourages programmers to co-design their systems with executable specifications that check these systems dynamically, as they execute. Moreover, unlike typical assertions, which execute dynamically and non-incrementally, the proposed are subject to novel patterns that enhance their performance: In regressive validation, verification partially discharges some checks, dynamically rewriting the program with residual versions; in progressive verification, online verification occurs in passes that each cache and reuse work, to avoid from-scratch verification of facts that still hold from earlier passes. Finally, to avoid forcing analysis programmers to reason about incremental changes explicitly in each analysis that they create, the meta layer expresses incremental computations implicitly, using an implicitly-incremental meta language whose abstractions hide reasoning on a per-change basis.

Internet of Things (IoT) marks the dawn of a technological revolution that rivals the industrial revolution. In this new era, intelligent computing becomes anticipatory, proactive, and adaptive. The next big growth in IoT systems will come from pushing Pervasive Personalized Intelligence (PPI) to the edge of the network, where latency is critical, and mobility, privacy, and context awareness are essential qualities of the application. This proposal will study the feasibility of establishing an industry university collaborative research center focused on PPI that will enable an entirely new class of intelligent applications that is predictive instead of reactive.

The proposed PPI Center will enrich the educational resources and toolsets for adding, modernizing, tuning, and suggesting intelligence in software applications for the IoT. The Colorado Site will lead activities under two thrusts: (1) Edge and Cloud Computing. Is it possible to identify and develop a small set of fundamental system-level services at the middleware layer to integrate mobile nodes, IoT devices and edge servers? (2) Programming Languages and Verification. Can new techniques be created that enable software developers to effectively create rich PPI applications that, by construction, are secure, privacy-preserving, and reliable?

With their rich array of sensors, camera, and GPS all integrated in a convenient form, IoT devices offer exciting new applications and services, never before possible on consumer devices. But these can be harnessed only if intelligence becomes a commodity. PPI will enable novel applications that will help the U.S. maintain and expand its leadership in computing. The proposed Center is committed to broadening participation in computing through, for example, summer camps focusing on programming for novices. To improve the retention of underrepresented populations, the proposed Center will work with technology associations to showcase PPI applications that help humanity.

The proposed Center on Pervasive Personalized Intelligence will be composed of Oregon State University, the University of Colorado Boulder, and industry partners. The proposed PPI Center will maintain a catalog of members, projects, meeting materials, program information, publications, data, code, and results at ppicenter.org. The website will be made available indefinitely or until the Center transitions to the next phase.

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.

Software development today is a social process, and the workflow of
programmers is increasingly centered around discussing program
revisions - that is, artifacts that document small, incremental program
changes. Meanwhile, traditional research on testing, debugging, and analyzing
programs focuses on one program version at a time, ignoring any preceding or
succeeding versions of the same software artifact. The project's novelties
are a foundational examination of program revisions and the investigation of
automated techniques that cooperatively assist software-engineering teams
with reasoning about them. The project's impacts are to enhance the way
engineering teams collaboratively evolve their software and thus enable them
to more effectively create secure and reliable software on which society
depends.

The project's core contribution is defining the notion of a "semantic
revision request" that enables treating program revisions as first-class
entities for debugging and analysis tools. A semantic view of program
revisions enables programmers to run or analyze the program revision (both
before and after a change simultaneously), not merely each of the two program
versions, as supported by today's conventional tools. By focusing on
debugging and analyzing program revisions - not their individual program
versions - the resulting tools come closer to capturing the intent of the
programmer as they develop and commit program changes. The intended broader
impact from a technical perspective is that these executable and analyzable
specifications will supplement, or even replace, informal descriptions about
how software systems evolve, by providing an unambiguous way to communicate
high-level programmer intent.

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.

Society increasingly relies on the reliability and security of software. Abstract interpretation is a well-established methodology for proving that software is free of certain classes of bugs. However, for industrial-scale software, standard abstract interpretation techniques may take hours to complete, making them difficult to integrate into modern software development practices. This project develops a framework for responsive static analysis, which retains the power of abstract interpretation while running much more quickly for common use cases. The project's novelties are new algorithms for running abstract interpretation responsively, corresponding mathematical proofs that these algorithms produce the desired, correct results, and working implementations of the algorithms. The project's impacts are greater performance and applicability of powerful abstract interpretation techniques for verifying software correctness, which in turn will yield more reliable and secure software.<br/><br/>The project builds on a recently-developed framework for demanded abstract interpretation, a demand-driven and incremental analysis approach based on reifying analysis computations and dependencies in a graph structure. Via generalizations of this approach, this project will extend the framework to handle compositional analysis, essential for efficient analysis of procedure calls, and refinement-based analysis, to enable combining analyses with varying levels of precision and scalability. This generalized framework will facilitate provable guarantees of from-scratch consistency, a crucial property for responsive analysis. The project will also implement the generalized framework and instantiate it with challenging analysis problems, addressing research challenges in making the framework practical.<br/><br/>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.