Showing 1–39 of 39 results for author: D'Antoni, L

The SemGuS Toolkit

Authors: Keith J. C. Johnson, Andrew Reynolds, Thomas Reps, Loris D'Antoni

Abstract: Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solve… ▽ More Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solvers, and presents an evaluation of the baseline enumerative solvers. △ Less

Submitted 3 June, 2024; originally announced June 2024.

Grammar-Aligned Decoding

Authors: Kanghee Park, Jiayu Wang, Taylor Berg-Kirkpatrick, Nadia Polikarpova, Loris D'Antoni

Abstract: Large Language Models (LLMs) struggle with reliably generating highly structured outputs, such as program code, mathematical formulas, or well-formed markup. Constrained decoding approaches mitigate this problem by greedily restricting what tokens an LLM can output at each step to guarantee that the output matches a given constraint. Specifically, in grammar-constrained decoding (GCD), the LLM's o… ▽ More Large Language Models (LLMs) struggle with reliably generating highly structured outputs, such as program code, mathematical formulas, or well-formed markup. Constrained decoding approaches mitigate this problem by greedily restricting what tokens an LLM can output at each step to guarantee that the output matches a given constraint. Specifically, in grammar-constrained decoding (GCD), the LLM's output must follow a given grammar. In this paper we demonstrate that GCD techniques (and in general constrained decoding techniques) can distort the LLM's distribution, leading to outputs that are grammatical but appear with likelihoods that are not proportional to the ones given by the LLM, and so ultimately are low-quality. We call the problem of aligning sampling with a grammar constraint, grammar-aligned decoding (GAD), and propose adaptive sampling with approximate expected futures (ASAp), a decoding algorithm that guarantees the output to be grammatical while provably producing outputs that match the conditional probability of the LLM's distribution conditioned on the given grammar constraint. Our algorithm uses prior sample outputs to soundly overapproximate the future grammaticality of different output prefixes. Our evaluation on code generation and structured NLP tasks shows how ASAp often produces outputs with higher likelihood (according to the LLM's distribution) than existing GCD techniques, while still enforcing the desired grammatical constraints. △ Less

Submitted 31 May, 2024; originally announced May 2024.

A One-Layer Decoder-Only Transformer is a Two-Layer RNN: With an Application to Certified Robustness

Authors: Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni

Abstract: This paper reveals a key insight that a one-layer decoder-only Transformer is equivalent to a two-layer Recurrent Neural Network (RNN). Building on this insight, we propose ARC-Tran, a novel approach for verifying the robustness of decoder-only Transformers against arbitrary perturbation spaces. Compared to ARC-Tran, current robustness verification techniques are limited either to specific and len… ▽ More This paper reveals a key insight that a one-layer decoder-only Transformer is equivalent to a two-layer Recurrent Neural Network (RNN). Building on this insight, we propose ARC-Tran, a novel approach for verifying the robustness of decoder-only Transformers against arbitrary perturbation spaces. Compared to ARC-Tran, current robustness verification techniques are limited either to specific and length-preserving perturbations like word substitutions or to recursive models like LSTMs. ARC-Tran addresses these limitations by meticulously managing position encoding to prevent mismatches and by utilizing our key insight to achieve precise and scalable verification. Our evaluation shows that ARC-Tran (1) trains models more robust to arbitrary perturbation spaces than those produced by existing techniques and (2) shows high certification accuracy of the resulting models. △ Less

Submitted 27 May, 2024; originally announced May 2024.

Verified Training for Counterfactual Explanation Robustness under Data Shift

Authors: Anna P. Meyer, Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni

Abstract: Counterfactual explanations (CEs) enhance the interpretability of machine learning models by describing what changes to an input are necessary to change its prediction to a desired class. These explanations are commonly used to guide users' actions, e.g., by describing how a user whose loan application was denied can be approved for a loan in the future. Existing approaches generate CEs by focusin… ▽ More Counterfactual explanations (CEs) enhance the interpretability of machine learning models by describing what changes to an input are necessary to change its prediction to a desired class. These explanations are commonly used to guide users' actions, e.g., by describing how a user whose loan application was denied can be approved for a loan in the future. Existing approaches generate CEs by focusing on a single, fixed model, and do not provide any formal guarantees on the CEs' future validity. When models are updated periodically to account for data shift, if the generated CEs are not robust to the shifts, users' actions may no longer have the desired impacts on their predictions. This paper introduces VeriTraCER, an approach that jointly trains a classifier and an explainer to explicitly consider the robustness of the generated CEs to small model shifts. VeriTraCER optimizes over a carefully designed loss function that ensures the verifiable robustness of CEs to local model updates, thus providing deterministic guarantees to CE validity. Our empirical evaluation demonstrates that VeriTraCER generates CEs that (1) are verifiably robust to small model updates and (2) display competitive robustness to state-of-the-art approaches in handling empirical model updates including random initialization, leave-one-out, and distribution shifts. △ Less

Submitted 6 March, 2024; originally announced March 2024.

Comments: 16 pages, 2 figures. Accepted at DMLR workshop at ICLR 2024

Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of Programs

Authors: Shaan Nagy, **woo Kim, Loris D'Antoni, Thomas Reps

Abstract: Unrealizability logic (UL) was proposed by Kim et al. as the first Hoare-style proof system for proving properties that hold for an infinite set of programs (defined by a regular tree grammar). The goal of our work is to automate reasoning and proof generation for UL. A key ingredient in UL is the notion of nonterminal summaries-inductive facts that characterize recursive nonterminals in the gramm… ▽ More Unrealizability logic (UL) was proposed by Kim et al. as the first Hoare-style proof system for proving properties that hold for an infinite set of programs (defined by a regular tree grammar). The goal of our work is to automate reasoning and proof generation for UL. A key ingredient in UL is the notion of nonterminal summaries-inductive facts that characterize recursive nonterminals in the grammar that defines the set of programs. They are analogous to procedure summaries in Hoare logic. The goal of automating UL led us to reformulate the inference rules-in particular, introducing a unified rule for nonterminal summaries, called the rule of adaptation, which draws inspiration from how procedure summaries are handled in Hoare logic. In the same way that verification conditions can be used to synthesize loop invariants for Hoare logic proofs, our reformulation of UL reduces the problem of synthesizing a nonterminal summary to a Syntax-Guided Synthesis problem. We implement Wuldo, the first checker and synthesizer for UL. Wuldo can express proofs beyond the reach of existing tools, including proofs that establish how infinitely many programs behave on infinitely many inputs, and in some cases Wuldo can even synthesize the needed nonterminal summaries. △ Less

Submitted 24 January, 2024; originally announced January 2024.

Comments: 30 pages, 5 figures, 2 tables

Modular System Synthesis

Authors: Kanghee Park, Keith J. C. Johnson, Loris D'Antoni, Thomas Reps

Abstract: This paper describes a way to improve the scalability of program synthesis by exploiting modularity: larger programs are synthesized from smaller programs. The key issue is to make each "larger-created-from-smaller" synthesis sub-problem be of a similar nature, so that the kind of synthesis sub-problem that needs to be solved--and the size of each search space--has roughly the same character at ea… ▽ More This paper describes a way to improve the scalability of program synthesis by exploiting modularity: larger programs are synthesized from smaller programs. The key issue is to make each "larger-created-from-smaller" synthesis sub-problem be of a similar nature, so that the kind of synthesis sub-problem that needs to be solved--and the size of each search space--has roughly the same character at each level. This work holds promise for creating program-synthesis tools that have far greater capabilities than currently available tools, and opens new avenues for synthesis research: how synthesis tools should support modular system design, and how synthesis applications can best exploit such capabilities. △ Less

Submitted 14 August, 2023; originally announced August 2023.

The Dataset Multiplicity Problem: How Unreliable Data Impacts Predictions

Authors: Anna P. Meyer, Aws Albarghouthi, Loris D'Antoni

Abstract: We introduce dataset multiplicity, a way to study how inaccuracies, uncertainty, and social bias in training datasets impact test-time predictions. The dataset multiplicity framework asks a counterfactual question of what the set of resultant models (and associated test-time predictions) would be if we could somehow access all hypothetical, unbiased versions of the dataset. We discuss how to use t… ▽ More We introduce dataset multiplicity, a way to study how inaccuracies, uncertainty, and social bias in training datasets impact test-time predictions. The dataset multiplicity framework asks a counterfactual question of what the set of resultant models (and associated test-time predictions) would be if we could somehow access all hypothetical, unbiased versions of the dataset. We discuss how to use this framework to encapsulate various sources of uncertainty in datasets' factualness, including systemic social bias, data collection practices, and noisy labels or features. We show how to exactly analyze the impacts of dataset multiplicity for a specific model architecture and type of uncertainty: linear models with label errors. Our empirical analysis shows that real-world datasets, under reasonable assumptions, contain many test samples whose predictions are affected by dataset multiplicity. Furthermore, the choice of domain-specific dataset multiplicity definition determines what samples are affected, and whether different demographic groups are disparately impacted. Finally, we discuss implications of dataset multiplicity for machine learning practice and research, including considerations for when model outcomes should not be trusted. △ Less

Submitted 20 April, 2023; originally announced April 2023.

Comments: 25 pages, 8 figures. Accepted at FAccT '23

PECAN: A Deterministic Certified Defense Against Backdoor Attacks

Authors: Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni

Abstract: Neural networks are vulnerable to backdoor poisoning attacks, where the attackers maliciously poison the training set and insert triggers into the test input to change the prediction of the victim model. Existing defenses for backdoor attacks either provide no formal guarantees or come with expensive-to-compute and ineffective probabilistic guarantees. We present PECAN, an efficient and certified… ▽ More Neural networks are vulnerable to backdoor poisoning attacks, where the attackers maliciously poison the training set and insert triggers into the test input to change the prediction of the victim model. Existing defenses for backdoor attacks either provide no formal guarantees or come with expensive-to-compute and ineffective probabilistic guarantees. We present PECAN, an efficient and certified approach for defending against backdoor attacks. The key insight powering PECAN is to apply off-the-shelf test-time evasion certification techniques on a set of neural networks trained on disjoint partitions of the data. We evaluate PECAN on image classification and malware detection datasets. Our results demonstrate that PECAN can (1) significantly outperform the state-of-the-art certified backdoor defense, both in defense strength and efficiency, and (2) on real back-door attacks, PECAN can reduce attack success rate by order of magnitude when compared to a range of baselines from the literature. △ Less

Submitted 20 May, 2024; v1 submitted 27 January, 2023; originally announced January 2023.

Synthesizing Specifications

Authors: Kanghee Park, Loris D'Antoni, Thomas Reps

Abstract: Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: i) a query posed about a set of function definitions, and ii) a domain-specific langua… ▽ More Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: i) a query posed about a set of function definitions, and ii) a domain-specific language L in which the extracted property is to be expressed (we call properties in the language L-properties). Each of the property is a best L-property for the query: there is no other L-property that is strictly more precise. Furthermore, the set of synthesized L-properties is exhaustive: no more L-properties can be added to it to make the conjunction more precise. We implemented our method in a tool, Spyro. The ability to modify both the query and L provides a Spyro user with ways to customize the kind of specification to be synthesized. We use this ability to show that Spyro can be used in a variety of applications, such as mining program specifications, performing abstract-domain operations, and synthesizing algebraic properties of program modules. △ Less

Submitted 5 February, 2024; v1 submitted 26 January, 2023; originally announced January 2023.

Unrealizability Logic

Authors: **woo Kim, Loris D'Antoni, Thomas Reps

Abstract: We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box, meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In… ▽ More We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box, meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In this paper, we present a Hoare-style reasoning system, called unrealizability logic for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable. △ Less

Submitted 8 March, 2023; v1 submitted 14 November, 2022; originally announced November 2022.

Synthesizing Transducers from Complex Specifications

Authors: Anvay Grover, Ruediger Ehlers, Loris D'Antoni

Abstract: Automating string transformations has been one of the killer applications of program synthesis. Existing synthesizers that solve this problem produce programs in domain-specific languages (DSL) that are engineered to help the synthesizer, and therefore lack nice formal properties. This limitation prevents the synthesized programs from being used in verification applications (e.g., to check complex… ▽ More Automating string transformations has been one of the killer applications of program synthesis. Existing synthesizers that solve this problem produce programs in domain-specific languages (DSL) that are engineered to help the synthesizer, and therefore lack nice formal properties. This limitation prevents the synthesized programs from being used in verification applications (e.g., to check complex pre-post conditions) and makes the synthesizers hard to modify due to their reliance on the given DSL. We present a constraint-based approach to synthesizing transducers, a well-studied model with strong closure and decidability properties. Our approach handles three types of specifications: (i) input-output examples, (ii) input-output types expressed as regular languages, and (iii) input/output distances that bound how many characters the transducer can modify when processing an input string. Our work is the first to support such complex specifications and it does so by using the algorithmic properties of transducers to generate constraints that can be solved using off-the-shelf SMT solvers. Our synthesis approach can be extended to many transducer models and it can be used, thanks to closure properties of transducers, to compute repairs for partially correct transducers. △ Less

Submitted 28 August, 2022; v1 submitted 9 August, 2022; originally announced August 2022.

Certifying Data-Bias Robustness in Linear Regression

Authors: Anna P. Meyer, Aws Albarghouthi, Loris D'Antoni

Abstract: Datasets typically contain inaccuracies due to human error and societal biases, and these inaccuracies can affect the outcomes of models trained on such datasets. We present a technique for certifying whether linear regression models are pointwise-robust to label bias in the training dataset, i.e., whether bounded perturbations to the labels of a training dataset result in models that change the p… ▽ More Datasets typically contain inaccuracies due to human error and societal biases, and these inaccuracies can affect the outcomes of models trained on such datasets. We present a technique for certifying whether linear regression models are pointwise-robust to label bias in the training dataset, i.e., whether bounded perturbations to the labels of a training dataset result in models that change the prediction of test points. We show how to solve this problem exactly for individual test points, and provide an approximate but more scalable method that does not require advance knowledge of the test point. We extensively evaluate both techniques and find that linear models -- both regression- and classification-based -- often display high levels of bias-robustness. However, we also unearth gaps in bias-robustness, such as high levels of non-robustness for certain bias assumptions on some datasets. Overall, our approach can serve as a guide for when to trust, or question, a model's output. △ Less

Submitted 7 June, 2022; originally announced June 2022.

Comments: 19 pages, 8 figures

BagFlip: A Certified Defense against Data Poisoning

Authors: Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni

Abstract: Machine learning models are vulnerable to data-poisoning attacks, in which an attacker maliciously modifies the training set to change the prediction of a learned model. In a trigger-less attack, the attacker can modify the training set but not the test inputs, while in a backdoor attack the attacker can also modify test inputs. Existing model-agnostic defense approaches either cannot handle backd… ▽ More Machine learning models are vulnerable to data-poisoning attacks, in which an attacker maliciously modifies the training set to change the prediction of a learned model. In a trigger-less attack, the attacker can modify the training set but not the test inputs, while in a backdoor attack the attacker can also modify test inputs. Existing model-agnostic defense approaches either cannot handle backdoor attacks or do not provide effective certificates (i.e., a proof of a defense). We present BagFlip, a model-agnostic certified approach that can effectively defend against both trigger-less and backdoor attacks. We evaluate BagFlip on image classification and malware detection datasets. BagFlip is equal to or more effective than the state-of-the-art approaches for trigger-less attacks and more effective than the state-of-the-art approaches for backdoor attacks. △ Less

Submitted 16 October, 2022; v1 submitted 26 May, 2022; originally announced May 2022.

Comments: Neurips 2022

P4BID: Information Flow Control in P4

Authors: Karuna Grewal, Loris D'Antoni, Justin Hsu

Abstract: Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to program such switches. The increase in speed and programmability has inspired research in dataplane programming, where many complex functionalities, e.g., key-value stores and load balancers, can be implemented entirely… ▽ More Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to program such switches. The increase in speed and programmability has inspired research in dataplane programming, where many complex functionalities, e.g., key-value stores and load balancers, can be implemented entirely in network switches. However, dataplane programs may suffer from novel security errors that are not traditionally found in network switches. To address this issue, we present a new information-flow control type system for P4. We formalize our type system in a recently-proposed core version of P4, and we prove a soundness theorem: well-typed programs satisfy non-interference. We also implement our type system in a tool, P4bid, which extends the type checker in the p4c compiler, the reference compiler for the latest version of P4. We present several case studies showing that natural security, integrity, and isolation properties in networks can be captured by non-interference, and our type system can detect violations of these properties while certifying correct programs. △ Less

Submitted 14 June, 2022; v1 submitted 6 April, 2022; originally announced April 2022.

Prognosis: Closed-Box Analysis of Network Protocol Implementations

Authors: Tiago Ferreira, Harrison Brewton, Loris D'Antoni, Alexandra Silva

Abstract: We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing di… ▽ More We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing differences between models of two implementations of the same protocol, or improving testing via model-based test generation. Prognosis is modular and easily adaptable to different protocols (e.g., TCP and QUIC) and their implementations. We use Prognosis to learn models of (parts of) three QUIC implementations -- Quiche (Cloudflare), Google QUIC, and Facebook mvfst -- and use these models to analyze the differences between the various implementations. Our analysis provides insights into different design choices and uncovers potential bugs. Concretely, we have found critical bugs in multiple QUIC implementations, which have been acknowledged by the developers. △ Less

Submitted 14 November, 2021; originally announced January 2022.

Comments: ACM SIGCOMM 2021 Conference (SIGCOMM '21), August 23--27, 2021, Virtual Event, USA

ACM Class: F.3.1; F.1.1

Journal ref: In Proceedings of the 2021 ACM SIGCOMM 2021 Conference. ACM, New York, NY, USA, 762-774

Certifying Robustness to Programmable Data Bias in Decision Trees

Authors: Anna P. Meyer, Aws Albarghouthi, Loris D'Antoni

Abstract: Datasets can be biased due to societal inequities, human biases, under-representation of minorities, etc. Our goal is to certify that models produced by a learning algorithm are pointwise-robust to potential dataset biases. This is a challenging problem: it entails learning models for a large, or even infinite, number of datasets, ensuring that they all produce the same prediction. We focus on dec… ▽ More Datasets can be biased due to societal inequities, human biases, under-representation of minorities, etc. Our goal is to certify that models produced by a learning algorithm are pointwise-robust to potential dataset biases. This is a challenging problem: it entails learning models for a large, or even infinite, number of datasets, ensuring that they all produce the same prediction. We focus on decision-tree learning due to the interpretable nature of the models. Our approach allows programmatically specifying bias models across a variety of dimensions (e.g., missing data for minorities), composing types of bias, and targeting bias towards a specific group. To certify robustness, we use a novel symbolic technique to evaluate a decision-tree learner on a large, or infinite, number of datasets, certifying that each and every dataset produces the same prediction for a specific test point. We evaluate our approach on datasets that are commonly used in the fairness literature, and demonstrate our approach's viability on a range of bias models. △ Less

Submitted 8 October, 2021; originally announced October 2021.

Comments: To be published at NeurIPS 2021. 22 pages, 4 figures

ACM Class: I.2.2; I.5.0; K.4.2

Synthesizing Abstract Transformers

Authors: Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni, Thomas Reps, Subhajit Roy

Abstract: 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 $\textit{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 $\textit{op}$, (… ▽ More 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 $\textit{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 $\textit{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 $\textit{op}$ in abstract domain A, expressed in $L$ (an "$L$-transformer for $\textit{op}$ over A"). Moreover, the abstract transformer obtained is a most-precise $L$-transformer for $\textit{op}$ over A; that is, there is no other $L$-transformer for $\textit{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. △ Less

Submitted 15 August, 2022; v1 submitted 2 May, 2021; originally announced May 2021.

Comments: 17 Figures, 5 Tables, 32 pages

Synthesis with Asymptotic Resource Bounds

Authors: Qinhe** Hu, John Cyphert, Loris D'Antoni, Thomas Reps

Abstract: We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex… ▽ More We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity O(nlog(n)). Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These ty** rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool, SynPlexity, was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers. △ Less

Submitted 26 May, 2021; v1 submitted 6 March, 2021; originally announced March 2021.

Certified Robustness to Programmable Transformations in LSTMs

Authors: Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni

Abstract: Deep neural networks for natural language processing are fragile in the face of adversarial examples -- small input perturbations, like synonym substitution or word duplication, which cause a neural network to change its prediction. We present an approach to certifying the robustness of LSTMs (and extensions of LSTMs) and training models that can be efficiently certified. Our approach can certify… ▽ More Deep neural networks for natural language processing are fragile in the face of adversarial examples -- small input perturbations, like synonym substitution or word duplication, which cause a neural network to change its prediction. We present an approach to certifying the robustness of LSTMs (and extensions of LSTMs) and training models that can be efficiently certified. Our approach can certify robustness to intractably large perturbation spaces defined programmatically in a language of string transformations. Our evaluation shows that (1) our approach can train models that are more robust to combinations of string transformations than those produced using existing techniques; (2) our approach can show high certification accuracy of the resulting models. △ Less

Submitted 7 September, 2021; v1 submitted 15 February, 2021; originally announced February 2021.

Comments: EMNLP 2021

Semantics-Guided Synthesis

Authors: **woo Kim, Qinhe** Hu, Loris D'Antoni, Thomas Reps

Abstract: 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 lo… ▽ More 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 both SyGuS problems(i.e., over expressions) and synthesis problems over an imperative programming language. △ Less

Submitted 11 November, 2020; v1 submitted 22 August, 2020; originally announced August 2020.

Comments: Updated version for camera-ready

Automata Tutor v3

Authors: Loris D'Antoni, Martin Helfrich, Jan Kretinsky, Emanuel Ramneantu, Maximilian Weininger

Abstract: Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for hel** teachers and students in large courses on automata and formal languages.… ▽ More Computer science class enrollments have rapidly risen in the past decade. With current class sizes, standard approaches to grading and providing personalized feedback are no longer possible and new techniques become both feasible and necessary. In this paper, we present the third version of Automata Tutor, a tool for hel** teachers and students in large courses on automata and formal languages. The second version of Automata Tutor supported automatic grading and feedback for finite-automata constructions and has already been used by thousands of users in dozens of countries. This new version of Automata Tutor supports automated grading and feedback generation for a greatly extended variety of new problems, including problems that ask students to create regular expressions, context-free grammars, pushdown automata and Turing machines corresponding to a given description, and problems about converting between equivalent models - e.g., from regular expressions to nondeterministic finite automata. Moreover, for several problems, this new version also enables teachers and students to automatically generate new problem instances. We also present the results of a survey run on a class of 950 students, which shows very positive results about the usability and usefulness of the tool. △ Less

Submitted 14 May, 2020; v1 submitted 4 May, 2020; originally announced May 2020.

Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems

Authors: Qinhe** Hu, John Cyphert, Loris D'Antoni, Thomas Reps

Abstract: We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). We formulate the problem of proving that a SyGuS problem is unrealizable over a finite set of examples as one of solving a set of equations: the solution yields an overapproximation of the set of possible outputs that any term in the search space can p… ▽ More We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). We formulate the problem of proving that a SyGuS problem is unrealizable over a finite set of examples as one of solving a set of equations: the solution yields an overapproximation of the set of possible outputs that any term in the search space can produce on the given examples. If none of the possible outputs agrees with all of the examples, our technique has proven that the given SyGuS problem is unrealizable. We then present an algorithm for exactly solving the set of equations that result from SyGuS problems over linear integer arithmetic (LIA) and LIA with conditionals (CLIA), thereby showing that LIA and CLIA SyGuS problems over finitely many examples are decidable. We implement the proposed technique and algorithms in a tool called Nay. Nay can prove unrealizability for 70/132 existing SyGuS benchmarks, with running times comparable to those of the state-of-the-art tool Nope. Moreover, Nay can solve 11 benchmarks that Nope cannot solve. △ Less

Submitted 2 April, 2020; originally announced April 2020.

Journal ref: PLDI 2020

Robustness to Programmable String Transformations via Augmented Abstract Training

Authors: Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni

Abstract: Deep neural networks for natural language processing tasks are vulnerable to adversarial input perturbations. In this paper, we present a versatile language for programmatically specifying string transformations -- e.g., insertions, deletions, substitutions, swaps, etc. -- that are relevant to the task at hand. We then present an approach to adversarially training models that are robust to such us… ▽ More Deep neural networks for natural language processing tasks are vulnerable to adversarial input perturbations. In this paper, we present a versatile language for programmatically specifying string transformations -- e.g., insertions, deletions, substitutions, swaps, etc. -- that are relevant to the task at hand. We then present an approach to adversarially training models that are robust to such user-defined string transformations. Our approach combines the advantages of search-based techniques for adversarial training with abstraction-based techniques. Specifically, we show how to decompose a set of user-defined string transformations into two component specifications, one that benefits from search and another from abstraction. We use our technique to train models on the AG and SST2 datasets and show that the resulting models are robust to combinations of user-defined transformations mimicking spelling mistakes and other meaning-preserving transformations. △ Less

Submitted 2 September, 2020; v1 submitted 21 February, 2020; originally announced February 2020.

Comments: 12 pages, ICML 2020

D2R: Dataplane-Only Policy-Compliant Routing Under Failures

Authors: Kausik Subramanian, Anubhavnidhi Abhashkumar, Loris D'Antoni, Aditya Akella

Abstract: In networks today, the data plane handles forwarding---sending a packet to the next device in the path---and the control plane handles routing---deciding the path of the packet in the network. This architecture has limitations. First, when link failures occur, the data plane has to wait for the control plane to install new routes, and packet losses can occur due to delayed routing convergence or c… ▽ More In networks today, the data plane handles forwarding---sending a packet to the next device in the path---and the control plane handles routing---deciding the path of the packet in the network. This architecture has limitations. First, when link failures occur, the data plane has to wait for the control plane to install new routes, and packet losses can occur due to delayed routing convergence or central controller latencies. Second, policy-compliance is not guaranteed without sophisticated configuration synthesis or controller intervention. In this paper, we take advantage of the recent advances in fast programmable switches to perform policy-compliant route computations entirely in the data plane, thus providing fast reactions to failures. D2R, our new network architecture, can provide the illusion of a network fabric that is always available and policy-compliant, even under failures. We implement our data plane in P4 and demonstrate its viability in real world topologies. △ Less

Submitted 5 December, 2019; originally announced December 2019.

Proving Data-Poisoning Robustness in Decision Trees

Authors: Samuel Drews, Aws Albarghouthi, Loris D'Antoni

Abstract: Machine learning models are brittle, and small changes in the training data can result in different predictions. We study the problem of proving that a prediction is robust to data poisoning, where an attacker can inject a number of malicious elements into the training set to influence the learned model. We target decision-tree models, a popular and simple class of machine learning models that und… ▽ More Machine learning models are brittle, and small changes in the training data can result in different predictions. We study the problem of proving that a prediction is robust to data poisoning, where an attacker can inject a number of malicious elements into the training set to influence the learned model. We target decision-tree models, a popular and simple class of machine learning models that underlies many complex learning techniques. We present a sound verification technique based on abstract interpretation and implement it in a tool called Antidote. Antidote abstractly trains decision trees for an intractably large space of possible poisoned datasets. Due to the soundness of our abstraction, Antidote can produce proofs that, for a given input, the corresponding prediction would not have changed had the training set been tampered with or not. We demonstrate the effectiveness of Antidote on a number of popular datasets. △ Less

Submitted 23 June, 2020; v1 submitted 2 December, 2019; originally announced December 2019.

Comments: Changes: revisions to main text for clarity of presentation, and corrections to proofs in the appendices

Efficient Synthesis with Probabilistic Constraints

Authors: Samuel Drews, Aws Albarghouthi, Loris D'Antoni

Abstract: We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided inductive synthesis (DIGITS), which iteratively calls a synthesizer on finite sample sets from a given distribution. We make theoretical and algorithmic contributions: (i) We prove the surprising result that DIGITS only req… ▽ More We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided inductive synthesis (DIGITS), which iteratively calls a synthesizer on finite sample sets from a given distribution. We make theoretical and algorithmic contributions: (i) We prove the surprising result that DIGITS only requires a polynomial number of synthesizer calls in the size of the sample set, despite its ostensibly exponential behavior. (ii) We present a property-directed version of DIGITS that further reduces the number of synthesizer calls, drastically improving synthesis performance on a range of benchmarks. △ Less

Submitted 20 May, 2019; originally announced May 2019.

Proving Unrealizability for Syntax-Guided Synthesis

Authors: Qinhe** Hu, Jason Breck, John Cyphert, Loris D'Antoni, Thomas Reps

Abstract: Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general SyGuS instances in which the grammar describing the search space contains infinitely many programs. By encodin… ▽ More Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general SyGuS instances in which the grammar describing the search space contains infinitely many programs. By encoding the synthesis problem's grammar G as a nondeterministic program P_G, we reduce the unrealizability problem to a reachability problem such that, if a standard program-analysis tool can establish that a certain assertion in P_G always holds, then the synthesis problem is unrealizable. Our method can be used to augment any existing SyGus tool so that it can establish that a successfully synthesized program q is optimal with respect to some syntactic cost -- e.g., q has the fewest possible if-then-else operators. Using known techniques, grammar G can be automatically transformed to generate exactly all programs with lower cost than q -- e.g., fewer conditional expressions. Our algorithm can then be applied to show that the resulting synthesis problem is unrealizable. We implemented the proposed technique in a tool called NOPE. NOPE can prove unrealizability for 59/134 variants of existing linear-integer-arithmetic SyGus benchmarks, whereas all existing SyGus solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them. △ Less

Submitted 23 July, 2019; v1 submitted 14 May, 2019; originally announced May 2019.

Symbolic Register Automata

Authors: Loris D'Antoni, Tiago Ferreira, Matteo Sammartino, Alexandra Silva

Abstract: Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Registe… ▽ More Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results. △ Less

Submitted 23 May, 2019; v1 submitted 16 November, 2018; originally announced November 2018.

Program Repair via Direct State Manipulation

Authors: Qinhe** Hu, Isaac Evavold, Roopsha Samanta, Rishabh Singh, Loris D'Antoni

Abstract: The goal of program repair is to automatically fix programs to meet a specification. We propose a new specification mechanism, direct manipulation, in which the programmer can visualize the trace of a buggy program on a failing input and convey the intended program behavior by manipulating variable values at some location. The repair problem is to find a program that, on the same input, reaches th… ▽ More The goal of program repair is to automatically fix programs to meet a specification. We propose a new specification mechanism, direct manipulation, in which the programmer can visualize the trace of a buggy program on a failing input and convey the intended program behavior by manipulating variable values at some location. The repair problem is to find a program that, on the same input, reaches the location identified by the programmer with variable values equal to the manipulated ones. Since a single program execution under-specifies the overall program behavior, we augment our repair problem with quantitative objectives to find the program that agrees with the specification and is closest to the original one with respect to some distance. We formalize the repair problem, build a program repair tool JDial based on the Sketch synthesizer, and show the effectiveness of JDial on representative buggy benchmarks from introductory programming assignments. △ Less

Submitted 20 March, 2018; originally announced March 2018.

Learning Quick Fixes from Code Repositories

Authors: Reudismam Rolim, Gustavo Soares, Rohit Gheyi, Titus Barik, Loris D'Antoni

Abstract: Code analyzers such as Error Prone and FindBugs detect code patterns symptomatic of bugs, performance issues, or bad style. These tools express patterns as quick fixes that detect and rewrite unwanted code. However, it is difficult to come up with new quick fixes and decide which ones are useful and frequently appear in real code. We propose to rely on the collective wisdom of programmers and lear… ▽ More Code analyzers such as Error Prone and FindBugs detect code patterns symptomatic of bugs, performance issues, or bad style. These tools express patterns as quick fixes that detect and rewrite unwanted code. However, it is difficult to come up with new quick fixes and decide which ones are useful and frequently appear in real code. We propose to rely on the collective wisdom of programmers and learn quick fixes from revision histories in software repositories. We present REVISAR, a tool for discovering common Java edit patterns in code repositories. Given code repositories and their revision histories, REVISAR (i) identifies code edits from revisions and (ii) clusters edits into sets that can be described using an edit pattern. The designers of code analyzers can then inspect the patterns and add the corresponding quick fixes to their tools. We ran REVISAR on nine popular GitHub projects, and it discovered 89 useful edit patterns that appeared in 3 or more projects. Moreover, 64% of the discovered patterns did not appear in existing tools. We then conducted a survey with 164 programmers from 124 projects and found that programmers significantly preferred eight out of the nine of the discovered patterns. Finally, we submitted 16 pull requests applying our patterns to 9 projects and, at the time of the writing, programmers accepted 6 (60%) of them. The results of this work aid toolsmiths in discovering quick fixes and making informed decisions about which quick fixes to prioritize based on patterns programmers actually apply in practice. △ Less

Submitted 7 September, 2018; v1 submitted 10 March, 2018; originally announced March 2018.

Comments: 12 pages

TraceDiff: Debugging Unexpected Code Behavior Using Trace Divergences

Authors: Ryo Suzuki, Gustavo Soares, Andrew Head, Elena Glassman, Ruan Reis, Melina Mongiovi, Loris D'Antoni, Bjoern Hartmann

Abstract: Recent advances in program synthesis offer means to automatically debug student submissions and generate personalized feedback in massive programming classrooms. When automatically generating feedback for programming assignments, a key challenge is designing pedagogically useful hints that are as effective as the manual feedback given by teachers. Through an analysis of teachers' hint-giving pract… ▽ More Recent advances in program synthesis offer means to automatically debug student submissions and generate personalized feedback in massive programming classrooms. When automatically generating feedback for programming assignments, a key challenge is designing pedagogically useful hints that are as effective as the manual feedback given by teachers. Through an analysis of teachers' hint-giving practices in 132 online Q&A posts, we establish three design guidelines that an effective feedback design should follow. Based on these guidelines, we develop a feedback system that leverages both program synthesis and visualization techniques. Our system compares the dynamic code execution of both incorrect and fixed code and highlights how the error leads to a difference in behavior and where the incorrect code trace diverges from the expected solution. Results from our study suggest that our system enables students to detect and fix bugs that are not caught by students using another existing visual debugging tool. △ Less

Submitted 12 August, 2017; originally announced August 2017.

Comments: VL/HCC 2017

ACM Class: H.5.2

Quantifying Program Bias

Authors: Aws Albarghouthi, Loris D'Antoni, Samuel Drews, Aditya Nori

Abstract: With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate whether programs are biased. We propose a novel probabilistic program analysis technique and apply it to quantifying bias in decision-making programs. Specifically, we (i) present a sound and complete automated verification technique for proving quantitative pr… ▽ More With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate whether programs are biased. We propose a novel probabilistic program analysis technique and apply it to quantifying bias in decision-making programs. Specifically, we (i) present a sound and complete automated verification technique for proving quantitative properties of probabilistic programs; (ii) show that certain notions of bias, recently proposed in the fairness literature, can be phrased as quantitative correctness properties; and (iii) present FairSquare, the first verification tool for quantifying program bias, and evaluate it on a range of decision-making programs. △ Less

Submitted 6 March, 2017; v1 submitted 17 February, 2017; originally announced February 2017.

Fairness as a Program Property

Authors: Aws Albarghouthi, Loris D'Antoni, Samuel Drews, Aditya Nori

Abstract: We explore the following question: Is a decision-making program fair, for some useful definition of fairness? First, we describe how several algorithmic fairness questions can be phrased as program verification problems. Second, we discuss an automated verification technique for proving or disproving fairness of decision-making programs with respect to a probabilistic model of the population. We explore the following question: Is a decision-making program fair, for some useful definition of fairness? First, we describe how several algorithmic fairness questions can be phrased as program verification problems. Second, we discuss an automated verification technique for proving or disproving fairness of decision-making programs with respect to a probabilistic model of the population. △ Less

Submitted 19 October, 2016; originally announced October 2016.

A Symbolic Decision Procedure for Symbolic Alternating Finite Automata

Authors: Loris D'Antoni, Zachary Kincaid, Fang Wang

Abstract: We introduce Symbolic Alternating Finite Automata (s-AFA) as an expressive, succinct, and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean operations over s-AFAs have linear complexity, which is in sharp contrast with the quadratic cost of intersection and union for non-alternating symbolic automata. Due to this succinctness, emptiness and equivalence check… ▽ More We introduce Symbolic Alternating Finite Automata (s-AFA) as an expressive, succinct, and decidable model for describing sets of finite sequences over arbitrary alphabets. Boolean operations over s-AFAs have linear complexity, which is in sharp contrast with the quadratic cost of intersection and union for non-alternating symbolic automata. Due to this succinctness, emptiness and equivalence checking are PSpace-hard. We introduce an algorithm for checking the equivalence of two s-AFAs based on bisimulation up to congruence. This algorithm allows us to exploit the power of SAT and SMT solvers to efficiently search the state space of the s-AFAs. We evaluate our decision procedure on two verification and security applications: 1) checking satisfiability of linear temporal logic formulas over finite traces, and 2) checking equivalence of Boolean combinations of regular expressions. Our experiments show that our technique often outperforms existing techniques and it can be beneficial in both such applications. △ Less

Submitted 5 October, 2016; originally announced October 2016.

Comments: 12 pages

Learning Syntactic Program Transformations from Examples

Authors: Reudismam Rolim, Gustavo Soares, Loris D'Antoni, Oleksandr Polozov, Sumit Gulwani, Rohit Gheyi, Ryo Suzuki, Bjoern Hartmann

Abstract: IDEs, such as Visual Studio, automate common transformations, such as Rename and Extract Method refactorings. However, extending these catalogs of transformations is complex and time-consuming. A similar phenomenon appears in intelligent tutoring systems where instructors have to write cumbersome code transformations that describe "common faults" to fix similar student submissions to programming a… ▽ More IDEs, such as Visual Studio, automate common transformations, such as Rename and Extract Method refactorings. However, extending these catalogs of transformations is complex and time-consuming. A similar phenomenon appears in intelligent tutoring systems where instructors have to write cumbersome code transformations that describe "common faults" to fix similar student submissions to programming assignments. We present REFAZER, a technique for automatically generating program transformations. REFAZER builds on the observation that code edits performed by developers can be used as examples for learning transformations. Example edits may share the same structure but involve different variables and subexpressions, which must be generalized in a transformation at the right level of abstraction. To learn transformations, REFAZER leverages state-of-the-art programming-by-example methodology using the following key components: (a) a novel domain-specific language (DSL) for describing program transformations, (b) domain-specific deductive algorithms for synthesizing transformations in the DSL, and (c) functions for ranking the synthesized transformations. We instantiate and evaluate REFAZER in two domains. First, given examples of edits used by students to fix incorrect programming assignment submissions, we learn transformations that can fix other students' submissions with similar faults. In our evaluation conducted on 4 programming tasks performed by 720 students, our technique helped to fix incorrect submissions for 87% of the students. In the second domain, we use repetitive edits applied by developers to the same project to synthesize a program transformation that applies these edits to other locations in the code. In our evaluation conducted on 59 scenarios of repetitive edits taken from 3 C# open-source projects, REFAZER learns the intended program transformation in 83% of the cases. △ Less

Submitted 31 August, 2016; originally announced August 2016.

NoFAQ: Synthesizing Command Repairs from Examples

Authors: Loris D'Antoni, Rishabh Singh, Michael Vaughn

Abstract: Command-line tools are confusing and hard to use for novice programmers due to their cryptic error messages and lack of documentation. Novice users often resort to online help-forums for finding corrections to their buggy commands, but have a hard time in searching precisely for posts that are relevant to their problem and then applying the suggested solutions to their buggy command. We present… ▽ More Command-line tools are confusing and hard to use for novice programmers due to their cryptic error messages and lack of documentation. Novice users often resort to online help-forums for finding corrections to their buggy commands, but have a hard time in searching precisely for posts that are relevant to their problem and then applying the suggested solutions to their buggy command. We present a tool, NoFAQ, that uses a set of rules to suggest possible fixes when users write buggy commands that trigger commonly occurring errors. The rules are expressed in a language called FixIt and each rule pattern-matches against the user's buggy command and the corresponding error message, and uses these inputs to produce a possible fixed command. Our main contribution is an algorithm based on lazy VSA for synthesizing FixIt rules from examples of buggy and repaired commands. The algorithm allows users to add new rules in NoFAQ without having to manually encode them. We present the evaluation of NoFAQ on 92 benchmark problems and show that NoFAQ is able to instantly synthesize rules for 81 benchmark problems in real time using just 2 to 5 input-output examples for each rule. △ Less

Submitted 29 August, 2016; originally announced August 2016.

Comments: 15 Pages, 9 Figures

In the Maze of Data Languages

Authors: Loris D'Antoni

Abstract: In data languages the positions of strings and trees carry a label from a finite alphabet and a data value from an infinite alphabet. Extensions of automata and logics over finite alphabets have been defined to recognize data languages, both in the string and tree cases. In this paper we describe and compare the complexity and expressiveness of such models to understand which ones are better candi… ▽ More In data languages the positions of strings and trees carry a label from a finite alphabet and a data value from an infinite alphabet. Extensions of automata and logics over finite alphabets have been defined to recognize data languages, both in the string and tree cases. In this paper we describe and compare the complexity and expressiveness of such models to understand which ones are better candidates as regular models. △ Less

Submitted 29 August, 2012; originally announced August 2012.

Regular Functions, Cost Register Automata, and Generalized Min-Cost Problems

Authors: Rajeev Alur, Loris D'Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, Yifei Yuan

Abstract: Motivated by the successful application of the theory of regular languages to formal verification of finite-state systems, there is a renewed interest in develo** a theory of analyzable functions from strings to numerical values that can provide a foundation for analyzing {\em quantitative} properties of finite-state systems. In this paper, we propose a deterministic model for associating costs… ▽ More Motivated by the successful application of the theory of regular languages to formal verification of finite-state systems, there is a renewed interest in develo** a theory of analyzable functions from strings to numerical values that can provide a foundation for analyzing {\em quantitative} properties of finite-state systems. In this paper, we propose a deterministic model for associating costs with strings that is parameterized by operations of interest (such as addition, scaling, and $\min$), a notion of {\em regularity} that provides a yardstick to measure expressiveness, and study decision problems and theoretical properties of resulting classes of cost functions. Our definition of regularity relies on the theory of string-to-tree transducers, and allows associating costs with events that are conditional upon regular properties of future events. Our model of {\em cost register automata} allows computation of regular functions using multiple "write-only" registers whose values can be combined using the allowed set of operations. We show that classical shortest-path algorithms as well as algorithms designed for computing {\em discounted costs}, can be adopted for solving the min-cost problems for the more general classes of functions specified in our model. Cost register automata with $\min$ and increment give a deterministic model that is equivalent to {\em weighted automata}, an extensively studied nondeterministic model, and this connection results in new insights and new open problems. △ Less

Submitted 21 February, 2012; v1 submitted 2 November, 2011; originally announced November 2011.

Comments: ICALP12 submission, technical report/extended version. 33 pages+title page

Streaming Tree Transducers

Authors: Rajeev Alur, Loris D'Antoni

Abstract: Theory of tree transducers provides a foundation for understanding expressiveness and complexity of analysis problems for specification languages for transforming hierarchically structured data such as XML documents. We introduce streaming tree transducers as an analyzable, executable, and expressive model for transforming unranked ordered trees in a single pass. Given a linear encoding of the inp… ▽ More Theory of tree transducers provides a foundation for understanding expressiveness and complexity of analysis problems for specification languages for transforming hierarchically structured data such as XML documents. We introduce streaming tree transducers as an analyzable, executable, and expressive model for transforming unranked ordered trees in a single pass. Given a linear encoding of the input tree, the transducer makes a single left-to-right pass through the input, and computes the output in linear time using a finite-state control, a visibly pushdown stack, and a finite number of variables that store output chunks that can be combined using the operations of string-concatenation and tree-insertion. We prove that the expressiveness of the model coincides with transductions definable using monadic second-order logic (MSO). Existing models of tree transducers either cannot implement all MSO-definable transformations, or require regular look ahead that prohibits single-pass implementation. We show a variety of analysis problems such as type-checking and checking functional equivalence are solvable for our model. △ Less

Submitted 21 February, 2012; v1 submitted 13 April, 2011; originally announced April 2011.

Comments: 40 pages