Interactive theorem provers (ITP) enable programmers to formally verify properties of their software systems. One burden for users of ITPs is identifying the necessary helper lemmas to complete a proof, for example those that define key inductive invariants. Existing approaches to lemma synthesis for ITPs have limited, if any, support for synthesizing implications: lemmas of the form P 1 ∧ ⋅⋅⋅ ∧ P n ⇒ Q . In this paper, we propose a technique and associated tool for synthesizing useful implication lemmas. Our approach employs a form of data-driven invariant inference to explore strengthenings of the current proof state, based on sample valuations of the current goal and assumptions. We have implemented our approach in a Rocq tactic called dilemma . We demonstrate its effectiveness in synthesizing necessary helper lemmas for proofs from the Verified Functional Algorithms textbook as well as from prior benchmark suites for lemma synthesis.

Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing helper lemmas fall into two broad categories. Some approaches are goal-directed, producing lemmas specifically to help a user make progress from a given proof state, but they have limited expressiveness in terms of the lemmas that can be produced. Other approaches are highly expressive, able to generate arbitrary lemmas from a given grammar, but they are completely undirected and hence not amenable to interactive usage. In this paper, we develop an approach to lemma synthesis that is both goal-directed and expressive. The key novelty is a technique for reducing lemma synthesis to a data-driven program synthesis problem, whereby examples for synthesis are generated from the current proof state. We also describe a technique to systematically introduce new variables for lemma synthesis, as well as techniques for filtering and ranking candidate lemmas for presentation to the user. We implement these ideas in a tool called lfind, which can be run as a Coq tactic. In an evaluation on four benchmark suites, lfind produces useful lemmas in 68% of the cases where a human prover used a lemma to make progress. In these cases lfind synthesizes a lemma that either enables a fully automated proof of the original goal or that matches the human-provided lemma.

Heterogeneous computing with field-programmable gate-arrays (FPGAs) has demonstrated orders of magnitude improvement in computing efficiency for many applications. However, the use of such platforms so far is limited to a small subset of programmers with specialized hardware knowledge. High-level synthesis (HLS) tools made significant progress in raising the level of programming abstraction from hardware programming languages to C/C++, but they usually cannot compile and generate accelerators for kernel programs with pointers, memory management, and recursion, and require manual refactoring to make them HLS-compatible. Besides, experts also need to provide heavily handcrafted optimizations to improve resource efficiency, which affects the maximum operating frequency, parallelization, and power efficiency.

The widespread adoption of deep learning is often attributed to its automatic feature construction with minimal inductive bias. However, in many real-world tasks, the learned function is intended to satisfy domain-specific constraints. We focus on monotonicity constraints, which are common and require that the function's output increases with increasing values of specific input features. We develop a counterexample-guided technique to provably enforce monotonicity constraints at prediction time. Additionally, we propose a technique to use monotonicity as an inductive bias for deep learning. It works by iteratively incorporating monotonicity counterexamples in the learning process. Contrary to prior work in monotonic learning, we target general ReLU neural networks and do not further restrict the hypothesis space. We have implemented these techniques in a tool called COMET. Experiments on real-world datasets demonstrate that our approach achieves state-of-the-art results compared to existing monotonic learners, and can improve the model quality compared to those that were trained without taking monotonicity constraints into account.

Modern search techniques either cannot efficiently incorporate human feedback to refine search results or cannot express structural or semantic properties of desired code. The key insight of our interactive code search technique ALICE is that user feedback can be actively incorporated to allow users to easily express and refine search queries. We design a query language to model the structure and semantics of code as logic facts. Given a code example with user annotations, ALICE automatically extracts a logic query from code features that are tagged as important. Users can refine the search query by labeling one or more examples as desired (positive) or irrelevant (negative). ALICE then infers a new logic query that separates positive examples from negative examples via active inductive logic programming. Our comprehensive simulation experiment shows that ALICE removes a large number of false positives quickly by actively incorporating user feedback. Its search algorithm is also robust to user labeling mistakes. Our choice of leveraging both positive and negative examples and using nested program structure as an inductive bias is effective in refining search queries. Compared with an existing interactive code search technique, ALICE does not require a user to manually construct a search pattern and yet achieves comparable precision and recall with much fewer search iterations. A case study with real developers shows that ALICE is easy to use and helps express complex code patterns.

Extract Method is a widely used refactoring operation to improve method comprehension and maintenance. Much research has been done to extract codefragments within the method body to form a new method. Criteria used for identifying extractable code is usually centered around degrees of cohesiveness, coupling and length of the method. However, automatic method extraction techniques have not been highly successful, since it can be hard to concretizethe criteria. In this work, we present a novel system that learns these criteria for Extract Method refactorings from open source repositories. We extractstructural and functional features, which encode the concepts of complexity, cohesion and coupling in our learning model, and train it to extract suitablecode fragments from a given source of a method. Our tool, GEMS, recommends a ranked list of code fragments with high accuracy and greatspeed. We evaluated our approach on several open source repositories and compared it against three state-of-the-art approaches-SEMI, JExtract andJDeodorant. The results on these open-source data show the superiority of our machine-learning-based approach in terms of effectiveness. We develop GEMS asan Eclipse plugin, with the intention to support software reliability through method extraction.