Designing abstract transformers for program-analysis tools is a challenging task. In the past, bugs have been discovered in such transformers, showing the difficulty of designing such transformers manually, and providing motivation for automated techniques. Recently, Kalita et al. showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) \({\mathcal{L}}\) (i.e., “ \({\mathcal{L}}\) -transformers”). Their technique creates provably sound and maximally precise \({\mathcal{L}}\) -transformers for an abstract domain \( A \) —i.e., given specifications of a concrete operation op , DSL \({\mathcal{L}}\) , and abstract domain \( A \) , it finds a best abstract \({\mathcal{L}}\) -transformer for op in \( A \) . However, we found that the algorithm of Kalita et al. does not succeed when applied to reduced-product domains: The need to synthesize transformers for all of the domains simultaneously blows up the search space. Because reduced-product domains are an important device for improving the precision of abstract interpretation, in this article, we propose an algorithm to synthesize reduced \({\mathcal{L}}\) -transformers \(\langle{f}^{\sharp\textsf{R}}_{1},{f}^{\sharp\textsf{R}}_{2},\dots,{f}^{\sharp \textsf{R}}_{n}\rangle\) for a product domain \(A_{1}\times A_{2}\times\dots\times A_{n}\) , using multiple DSLs: \({\mathcal{L}}\) \(=\langle{\mathcal{L}}_{1},{\mathcal{L}}_{2},\ldots,{\mathcal{L}}_{n}\rangle\) . Synthesis of reduced-product transformers is quite challenging: First, the synthesis task has to tackle an increased “feature set” because each component transformer now has access to the abstract inputs from all component domains in the product. Second, to ensure that the product transformer is maximally precise, the synthesis task needs to arrange for the component transformers to cooperate with each other. We implemented our algorithm in a tool, Amurth2 , and used it to synthesize abstract transformers for two product domains—SAFE and JSAI—available within the SAFE str framework for JavaScript program analysis. For four of the six operations supported by SAFE str , Amurth2 synthesizes more precise abstract transformers than the manually written ones available in SAFE str .

What-Comes-Next (WCN) puzzles challenge us to identify the next figure that "logically follows" a provided sequence of figures. WCN puzzles are a favorite of interviewers and examiners---there is hardly any aptitude test that misses WCN puzzles. In this work, we propose to automatically synthesize WCN puzzles. The key insight to our methodology is that generation of WCN problems can be posed as a program synthesis problem. We design a small yet expressive language, PuzzlerLang, to capture solutions to WCN puzzles. PuzzlerLang is expressive enough to explain almost all human generated WCN puzzles that we collected, and yet, small enough to allow synthesis in a reasonable time. To ensure that the generated puzzles are appealing to humans, we infer a machine learning model to approximate the appeal factor of given WCN puzzle to humans. We use this model within our puzzle synthesizer as an optimization function to generate highly appealing and correct-by-construction WCN puzzles. We implemented our ideas in a tool, PuzzleGen; we found that PuzzleGen is fast, clocking an average time of about 3.4s per puzzle. Further, statistical tests over the responses from a user-study supported that the PuzzleGen generated puzzles were indistinguishable from puzzles created by humans.

Program analysis, verification and testing are important topics in programming languages and software engineering. They aim to produce engineers who are not only capable of empirically evaluating but, also formally reasoning on the correctness of software systems. We propose a specialized framework, Chiron, designed to teach graduate-level courses on these topics. Chiron has a small code base for easy understanding, uses a unified intermediate representation across all its analysis modules, maintains a modular architecture for plugging in new algorithms and uses a “fun” programming language to provide a gamified experience. Currently, it packages a dataflow analysis engine for driving compiler optimizations, an abstract interpretation engine for verification, a symbolic execution engine, a fuzzer and an evolutionary test generator for program testing, and a spectrum based statistical bug localization module. Within Chiron, program analysis tasks are posed in an unconventional setting (as adventures of a turtle) to provide a gamified experience; the accompanying animations (showing the movements of the turtle) allow the student to understand the underlying concepts better, and the detailed logs allow the teaching assistants in their grading activities. Chiron has been used in two offerings of a graduate level course on program analysis, verification and testing. In response to our survey questionnaire, all the students unanimously held the opinion that Chiron was extremely helpful in aiding their learning, and recommended its use in similar courses.

This paper addresses the problem of creating abstract transformers automatically. The method we present automates the construction of static analyzers in a fashion similar to the way yacc automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides specifications of (i) the concrete semantics of a given operation op , (ii) the abstract domain A to be used by the analyzer, and (iii) the semantics of a domain-specific language L in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for op in abstract domain A , expressed in L (an “ L -transformer for op over A ”). Moreover, the abstract transformer obtained is a most-precise L -transformer for op over A ; that is, there is no other L -transformer for op over A that is strictly more precise. We implemented our method in a tool called AMURTH. We used AMURTH to create sets of replacement abstract transformers for those used in two existing analyzers, and obtained essentially identical performance. However, when we compared the existing transformers with the transformers obtained using AMURTH, we discovered that four of the existing transformers were unsound, which demonstrates the risk of using manually created transformers.

Programming environments for sequential programs provide strong debugging support. However, concurrent programs, especially under relaxed memory models, lack powerful interactive debugging tools. In this work, we present Gambit, an interactive debugging environment that uses gdb to run a concrete debugging session on a concurrent program, while employing a symbolic execution on the program trace in the background simultaneously. The symbolic execution is analysed by a theorem prover to answer queries from the programmer on possible scenarios resulting from alternate thread interleavings or due to reorderings on other relaxed memory models.

Path‐based equivalence checkers (PBECs) have been successfully applied for verification of programmes from diverse domains and from various stages of high‐level synthesis. In the case of non‐equivalence, PBEC provides very little information which is not sufficient for further investigation of the two programmes being compared by some human expert. In this work, the authors show how a counter‐trace ( cTrace ) can be generated in the case of non‐equivalence reported by the PBEC. Using this cTrace , they also present a procedure to find suitable initialisation values for input variables which reveal the non‐equivalence (i.e. counter‐example) by using off‐the‐shelf satisfiability modulo theories (SMT) solvers. To aid the human expert, they also show that how they can visualise this cTrace in the control and data‐flow graph of the programmes using the graph visualisation software – Graphviz. This counter‐example and visual representation of the corresponding cTrace will be helpful in debugging the root cause of the non‐equivalence. The experimental results are encouraging.