More Like this

1. Semantics-guided synthesis

   https://doi.org/10.1145/3434311  

   Kim, Jinwoo; Hu, Qinheping; D'Antoni, Loris; Reps, Thomas (January 2021, Proceedings of the ACM on Programming Languages)

   This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuS framework, we develop an algorithm for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, our approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space. We implemented the technique in a tool called MESSY, and applied it to SyGuS problems (i.e., over expressions), synthesis problems over an imperative programming language, and synthesis problems over regular expressions. 

   more » « less
2. PyFoReL: A Domain-Specific Language for Formal Requirements in Temporal Logic

   https://doi.org/10.1109/RE54965.2022.00037  

   Anderson, Jacob; Hekmatnejad, Mohammad; Fainekos, Georgios (August 2022, 2022 IEEE 30th International Requirements Engineering Conference (RE))

   Temporal Logic (TL) bridges the gap between natural language and formal reasoning in the field of complex systems verification. However, in order to leverage the expressivity entailed by TL, the syntax and semantics must first be understood—a large task in itself. This significant knowledge gap leads to several issues: (1) the likelihood of adopting a TL-based verification method is decreased, and (2) the chance of poorly written and inaccurate requirements is increased. In this ongoing work, we present the Pythonic Formal Requirements Language (PyFoReL) tool: a Domain-Specific Language inspired by the programming language Python to simplify the elicitation of TL-based requirements for engineers and non-experts. 

   more » « less
3. Transformation of TOCL Temporal Properties into OCL

   Al Lail, Mustafa; Rosales, Antonio; Cardenas, Hector; Hamann, Lars; Perez, Alfredo (October 2022, MODELS'22: ACM / IEEE 25th International Conference on Model Driven Engineering Languages and Systems Workshops)

   Specifying and verifying the temporal properties of UML-based systems can be challenging. Although there exist some extensions of OCL to support the specification of temporal properties in UML-based notations, most of the approaches depend on using non-UML formal formalisms such as LTL, CTL, and CTL* while transforming the under-development UML models into non-UML model checking frameworks for verification. This approach introduces complexities and relies on techniques and tools that are not within the UML spectrum. In this paper, we show how TOCL (one OCL extension for temporal properties specification) can be transformed into OCL for verification purposes. Towards this end, we created a formal EBNF grammar for TOCL, based on which a parser and a MOF metamodel were generated for the language. Additionally, to facilitate the analysis of the TOCL properties, we formally defined transformation rules from TOCL metamodel to OCL metamodel using QVT. Finally, we validated the implementations of the transformation rules using USE. 

   more » « less
4. Data flow refinement type inference

   https://doi.org/10.1145/3434300  

   Pavlinovic, Zvonimir; Su, Yusen; Wies, Thomas (January 2021, Proceedings of the ACM on Programming Languages)

   Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of constrained Horn clauses extracted from typing derivations. An example is Liquid type inference, which solves the extracted constraints using predicate abstraction. However, the reduction to constraint solving in itself already signifies an abstraction of the program semantics that affects the precision of the overall static analysis. To better understand this issue, we study the type inference problem in its entirety through the lens of abstract interpretation. We propose a new refinement type system that is parametric with the choice of the abstract domain of type refinements as well as the degree to which it tracks context-sensitive control flow information. We then derive an accompanying parametric inference algorithm as an abstract interpretation of a novel data flow semantics of functional programs. We further show that the type system is sound and complete with respect to the constructed abstract semantics. Our theoretical development reveals the key abstraction steps inherent in refinement type inference algorithms. The trade-off between precision and efficiency of these abstraction steps is controlled by the parameters of the type system. Existing refinement type systems and their respective inference algorithms, such as Liquid types, are captured by concrete parameter instantiations. We have implemented our framework in a prototype tool and evaluated it for a range of new parameter instantiations (e.g., using octagons and polyhedra for expressing type refinements). The tool compares favorably against other existing tools. Our evaluation indicates that our approach can be used to systematically construct new refinement type inference algorithms that are both robust and precise. 

   more » « less
5. Lightweight multi-language syntax transformation with parser parser combinators

   https://doi.org/10.1145/3314221.3314589  

   van Tonder, Rijnard; Le Goues, Claire (July 2019, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation)

   Automatically transforming programs is hard, yet critical for automated program refactoring, rewriting, and repair. Multi-language syntax transformation is especially hard due to heterogeneous representations in syntax, parse trees, and abstract syntax trees (ASTs). Our insight is that the problem can be decomposed such that (1) a common grammar expresses the central context-free language (CFL) properties shared by many contemporary languages and (2) open extension points in the grammar allow customizing syntax (e.g., for balanced delimiters) and hooks in smaller parsers to handle language-specific syntax (e.g., for comments). Our key contribution operationalizes this decomposition using a Parser Parser combinator (PPC), a mechanism that generates parsers for matching syntactic fragments in source code by parsing declarative user-supplied templates. This allows our approach to detach from translating input programs to any particular abstract syntax tree representation, and lifts syntax rewriting to a modularly-defined parsing problem. A notable effect is that we skirt the complexity and burden of defining additional translation layers between concrete user input templates and an underlying abstract syntax representation. We demonstrate that these ideas admit efficient and declarative rewrite templates across 12 languages, and validate effectiveness of our approach by producing correct and desirable lightweight transformations on popular real-world projects (over 50 syntactic changes produced by our approach have been merged into 40+). Our declarative rewrite patterns require an order of magnitude less code compared to analog implementations in existing, language-specific tools. 

   more » « less