A Method to Deduce and Synthesize the Dafny Programs

We propose a systematic method to deduce and synthesize the Dafny programs. First, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool. Through this method, we deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems, and so on. Due to space limitation, we only illustrate the development process of Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of Dafny program developed. What’s more, we demonstrate the potential of the deductive synthesis method by developing a new local bubble Sorting program.

Certifying the synthesis of heap-manipulating programs

Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend. In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.

Method of Multilevel Adaptive Synthesis of Monitoring Object Knowledge Graphs

The paper introduces a method for adaptive deductive synthesis of state models, of complex objects, with multilevel variable structures. The method makes it possible to predict the state of objects using the data coming from them. The data from the objects are collected with sensors installed on them. Multilevel knowledge graphs (KG) are used to describe the observed objects. The new adaptive synthesis method develops previously proposed inductive and deductive synthesis methods, allowing the context to be taken into account when predicting the states of the monitored objects based on the data obtained from them. The article proposes the algorithm for the suggested method and presents its computational complexity analysis. The software system, based on the proposed method, and the algorithm for multilevel adaptive synthesis of the object models developed, are described in the article. The effectiveness of the proposed method is shown in the results from modeling the states of telecommunication networks of cable television operators.

Deductive Synthesis of Networks Hierarchical Knowledge Graphs

The article focuses on developing of a deductive synthesis method for building telecommunications networks (TN) hierarchical knowledge graphs (KG). Synthesized KGs can be used to solve search, analytical, and recommendation (forecast) problems. TNs are complex heterogeneous objects. The synthesis of knowledge graphs of such objects requires much computational resources. The proposed method provides a low complexity of the synthesis of KG of TN by taking into account their hierarchical structure. The authors propose to do synthesis by direct downward multilevel inference and reverse multilevel inference. The article analyses existing graph models of TNs and methods for their building. Detailed description of the proposed method of networks hierarchical KGs synthesis is given. In order to evaluate the deductive synthesis method, a prototype of the system is developed. The provided real-world example shows how telecommunications networks hierarchical knowledge graphs are synthesized and used in practice. Finally, conclusions are formulated, and the areas of further research are identified.

Theory Exploration Powered by Deductive Synthesis

This paper presents a symbolic method for automatic theorem generation based on deductive inference. Many software verification and reasoning tasks require proving complex logical properties; coping with this complexity is generally done by declaring and proving relevant sub-properties. This gives rise to the challenge of discovering useful sub-properties that can assist the automated proof process. This is known as the theory exploration problem, and so far, predominant solutions that emerged rely on evaluation using concrete values. This limits the applicability of these theory exploration techniques to complex programs and properties.In this work, we introduce a new symbolic technique for theory exploration, capable of (offline) generation of a library of lemmas from a base set of inductive data types and recursive definitions. Our approach introduces a new method for using abstraction to overcome the above limitations, combining it with deductive synthesis to reason about abstract values. Our implementation has shown to find more lemmas than prior art, avoiding redundant lemmas (in terms of provability), while being faster in most cases. This new abstraction-based theory exploration method is a step toward applying theory exploration to software verification and synthesis.

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities

This paper presents the main ideas behind deductive synthesis of heap-manipulating program and outlines present challenges faced by this approach as well as future opportunities for its applications.