Workshop MAPL 2017 – Author Index 
Contents 
Abstracts 
Authors

Abadi, Martín 
MAPL'17: "A Computational Model for ..."
A Computational Model for TensorFlow: An Introduction
Martín Abadi, Michael Isard, and Derek G. Murray (Google Brain, USA)
TensorFlow is a powerful, programmable system for machine learning.
This paper aims to provide the basics of a conceptual framework for
understanding the behavior of TensorFlow models during training and inference:
it describes an operational semantics, of the kind common in
the literature on programming languages. More broadly, the paper
suggests that a programminglanguage perspective is fruitful in
designing and in explaining systems such as TensorFlow.
@InProceedings{MAPL17p1,
author = {Martín Abadi and Michael Isard and Derek G. Murray},
title = {A Computational Model for TensorFlow: An Introduction},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {17},
doi = {10.1145/3088525.3088527},
year = {2017},
}
Publisher's Version
Article Search


Eisner, Jason 
MAPL'17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. 

Filardo, Nathaniel Wesley 
MAPL'17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. 

Foster, Jeffrey S. 
MAPL'17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA)
The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools.
To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier.
We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports.
@InProceedings{MAPL17p35,
author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter},
title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {3542},
doi = {10.1145/3088525.3088675},
year = {2017},
}
Publisher's Version
Article Search


FrancisLandau, Matthew 
MAPL'17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. 

Gray, Patrick 
MAPL'17: "Verified Perceptron Convergence ..."
Verified Perceptron Convergence Theorem
Charlie Murphy, Patrick Gray, and Gordon Stewart (Princeton University, USA; Ohio University, USA)
Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, onelayer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets).
Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitraryprecision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet  and occasionally exceed  the performance of the arbitraryprecision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building highassurance machinelearning systems that reuse existing codebases.
@InProceedings{MAPL17p43,
author = {Charlie Murphy and Patrick Gray and Gordon Stewart},
title = {Verified Perceptron Convergence Theorem},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {4350},
doi = {10.1145/3088525.3088673},
year = {2017},
}
Publisher's Version
Article Search
Info


Grossman, Dan 
MAPL'17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA)
Many applications compute with estimated and uncertain data. While
advances in probabilistic programming help developers build such
applications, debugging them remains extremely challenging. New types of
errors in probabilistic programs include 1) ignoring dependencies and
correlation between random variables and in training data, 2) poorly
chosen inference hyperparameters, and 3) incorrect statistical models. A
partial solution to prevent these errors in some languages forbids
developers from explicitly invoking inference. While this prevents some
dependence errors, it limits composition and control over inference, and
does not guarantee absence of other types of errors. This paper presents
the FLEXI programming model which supports constructs for invoking
inference in the language and reusing the results in other statistical
computations. We define a novel formalism for inference with a
Decorated Bayesian Network and present a tool, DePP, that
analyzes this representation to identify the above errors. We evaluate
DePP on a range of prototypical examples to show how it helps developers
to detect errors.
@InProceedings{MAPL17p18,
author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley},
title = {Debugging Probabilistic Programs},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {1826},
doi = {10.1145/3088525.3088564},
year = {2017},
}
Publisher's Version
Article Search


Isard, Michael 
MAPL'17: "A Computational Model for ..."
A Computational Model for TensorFlow: An Introduction
Martín Abadi, Michael Isard, and Derek G. Murray (Google Brain, USA)
TensorFlow is a powerful, programmable system for machine learning.
This paper aims to provide the basics of a conceptual framework for
understanding the behavior of TensorFlow models during training and inference:
it describes an operational semantics, of the kind common in
the literature on programming languages. More broadly, the paper
suggests that a programminglanguage perspective is fruitful in
designing and in explaining systems such as TensorFlow.
@InProceedings{MAPL17p1,
author = {Martín Abadi and Michael Isard and Derek G. Murray},
title = {A Computational Model for TensorFlow: An Introduction},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {17},
doi = {10.1145/3088525.3088527},
year = {2017},
}
Publisher's Version
Article Search


Khorasani, Farzad 
MAPL'17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. 

Koc, Ugur 
MAPL'17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA)
The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools.
To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier.
We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports.
@InProceedings{MAPL17p35,
author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter},
title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {3542},
doi = {10.1145/3088525.3088675},
year = {2017},
}
Publisher's Version
Article Search


McKinley, Kathryn S. 
MAPL'17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA)
Many applications compute with estimated and uncertain data. While
advances in probabilistic programming help developers build such
applications, debugging them remains extremely challenging. New types of
errors in probabilistic programs include 1) ignoring dependencies and
correlation between random variables and in training data, 2) poorly
chosen inference hyperparameters, and 3) incorrect statistical models. A
partial solution to prevent these errors in some languages forbids
developers from explicitly invoking inference. While this prevents some
dependence errors, it limits composition and control over inference, and
does not guarantee absence of other types of errors. This paper presents
the FLEXI programming model which supports constructs for invoking
inference in the language and reusing the results in other statistical
computations. We define a novel formalism for inference with a
Decorated Bayesian Network and present a tool, DePP, that
analyzes this representation to identify the above errors. We evaluate
DePP on a range of prototypical examples to show how it helps developers
to detect errors.
@InProceedings{MAPL17p18,
author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley},
title = {Debugging Probabilistic Programs},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {1826},
doi = {10.1145/3088525.3088564},
year = {2017},
}
Publisher's Version
Article Search


Murphy, Charlie 
MAPL'17: "Verified Perceptron Convergence ..."
Verified Perceptron Convergence Theorem
Charlie Murphy, Patrick Gray, and Gordon Stewart (Princeton University, USA; Ohio University, USA)
Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, onelayer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets).
Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitraryprecision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet  and occasionally exceed  the performance of the arbitraryprecision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building highassurance machinelearning systems that reuse existing codebases.
@InProceedings{MAPL17p43,
author = {Charlie Murphy and Patrick Gray and Gordon Stewart},
title = {Verified Perceptron Convergence Theorem},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {4350},
doi = {10.1145/3088525.3088673},
year = {2017},
}
Publisher's Version
Article Search
Info


Murray, Derek G. 
MAPL'17: "A Computational Model for ..."
A Computational Model for TensorFlow: An Introduction
Martín Abadi, Michael Isard, and Derek G. Murray (Google Brain, USA)
TensorFlow is a powerful, programmable system for machine learning.
This paper aims to provide the basics of a conceptual framework for
understanding the behavior of TensorFlow models during training and inference:
it describes an operational semantics, of the kind common in
the literature on programming languages. More broadly, the paper
suggests that a programminglanguage perspective is fruitful in
designing and in explaining systems such as TensorFlow.
@InProceedings{MAPL17p1,
author = {Martín Abadi and Michael Isard and Derek G. Murray},
title = {A Computational Model for TensorFlow: An Introduction},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {17},
doi = {10.1145/3088525.3088527},
year = {2017},
}
Publisher's Version
Article Search


Mytkowicz, Todd 
MAPL'17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA)
Many applications compute with estimated and uncertain data. While
advances in probabilistic programming help developers build such
applications, debugging them remains extremely challenging. New types of
errors in probabilistic programs include 1) ignoring dependencies and
correlation between random variables and in training data, 2) poorly
chosen inference hyperparameters, and 3) incorrect statistical models. A
partial solution to prevent these errors in some languages forbids
developers from explicitly invoking inference. While this prevents some
dependence errors, it limits composition and control over inference, and
does not guarantee absence of other types of errors. This paper presents
the FLEXI programming model which supports constructs for invoking
inference in the language and reusing the results in other statistical
computations. We define a novel formalism for inference with a
Decorated Bayesian Network and present a tool, DePP, that
analyzes this representation to identify the above errors. We evaluate
DePP on a range of prototypical examples to show how it helps developers
to detect errors.
@InProceedings{MAPL17p18,
author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley},
title = {Debugging Probabilistic Programs},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {1826},
doi = {10.1145/3088525.3088564},
year = {2017},
}
Publisher's Version
Article Search


Naik, Mayur 
MAPL'17: "Combining the Logical and ..."
Combining the Logical and the Probabilistic in Program Analysis
Xin Zhang, Xujie Si, and Mayur Naik (Georgia Institute of Technology, USA; University of Pennsylvania, USA)
Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology.
@InProceedings{MAPL17p27,
author = {Xin Zhang and Xujie Si and Mayur Naik},
title = {Combining the Logical and the Probabilistic in Program Analysis},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {2734},
doi = {10.1145/3088525.3088563},
year = {2017},
}
Publisher's Version
Article Search


Nandi, Chandrakana 
MAPL'17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA)
Many applications compute with estimated and uncertain data. While
advances in probabilistic programming help developers build such
applications, debugging them remains extremely challenging. New types of
errors in probabilistic programs include 1) ignoring dependencies and
correlation between random variables and in training data, 2) poorly
chosen inference hyperparameters, and 3) incorrect statistical models. A
partial solution to prevent these errors in some languages forbids
developers from explicitly invoking inference. While this prevents some
dependence errors, it limits composition and control over inference, and
does not guarantee absence of other types of errors. This paper presents
the FLEXI programming model which supports constructs for invoking
inference in the language and reusing the results in other statistical
computations. We define a novel formalism for inference with a
Decorated Bayesian Network and present a tool, DePP, that
analyzes this representation to identify the above errors. We evaluate
DePP on a range of prototypical examples to show how it helps developers
to detect errors.
@InProceedings{MAPL17p18,
author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley},
title = {Debugging Probabilistic Programs},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {1826},
doi = {10.1145/3088525.3088564},
year = {2017},
}
Publisher's Version
Article Search


Porter, Adam A. 
MAPL'17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA)
The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools.
To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier.
We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports.
@InProceedings{MAPL17p35,
author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter},
title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {3542},
doi = {10.1145/3088525.3088675},
year = {2017},
}
Publisher's Version
Article Search


Saadatpanah, Parsa 
MAPL'17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA)
The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools.
To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier.
We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports.
@InProceedings{MAPL17p35,
author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter},
title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {3542},
doi = {10.1145/3088525.3088675},
year = {2017},
}
Publisher's Version
Article Search


Sampson, Adrian 
MAPL'17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA)
Many applications compute with estimated and uncertain data. While
advances in probabilistic programming help developers build such
applications, debugging them remains extremely challenging. New types of
errors in probabilistic programs include 1) ignoring dependencies and
correlation between random variables and in training data, 2) poorly
chosen inference hyperparameters, and 3) incorrect statistical models. A
partial solution to prevent these errors in some languages forbids
developers from explicitly invoking inference. While this prevents some
dependence errors, it limits composition and control over inference, and
does not guarantee absence of other types of errors. This paper presents
the FLEXI programming model which supports constructs for invoking
inference in the language and reusing the results in other statistical
computations. We define a novel formalism for inference with a
Decorated Bayesian Network and present a tool, DePP, that
analyzes this representation to identify the above errors. We evaluate
DePP on a range of prototypical examples to show how it helps developers
to detect errors.
@InProceedings{MAPL17p18,
author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley},
title = {Debugging Probabilistic Programs},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {1826},
doi = {10.1145/3088525.3088564},
year = {2017},
}
Publisher's Version
Article Search


Si, Xujie 
MAPL'17: "Combining the Logical and ..."
Combining the Logical and the Probabilistic in Program Analysis
Xin Zhang, Xujie Si, and Mayur Naik (Georgia Institute of Technology, USA; University of Pennsylvania, USA)
Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology.
@InProceedings{MAPL17p27,
author = {Xin Zhang and Xujie Si and Mayur Naik},
title = {Combining the Logical and the Probabilistic in Program Analysis},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {2734},
doi = {10.1145/3088525.3088563},
year = {2017},
}
Publisher's Version
Article Search


Stewart, Gordon 
MAPL'17: "Verified Perceptron Convergence ..."
Verified Perceptron Convergence Theorem
Charlie Murphy, Patrick Gray, and Gordon Stewart (Princeton University, USA; Ohio University, USA)
Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, onelayer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets).
Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitraryprecision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet  and occasionally exceed  the performance of the arbitraryprecision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building highassurance machinelearning systems that reuse existing codebases.
@InProceedings{MAPL17p43,
author = {Charlie Murphy and Patrick Gray and Gordon Stewart},
title = {Verified Perceptron Convergence Theorem},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {4350},
doi = {10.1145/3088525.3088673},
year = {2017},
}
Publisher's Version
Article Search
Info


Vieira, Tim 
MAPL'17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. 

Zhang, Xin 
MAPL'17: "Combining the Logical and ..."
Combining the Logical and the Probabilistic in Program Analysis
Xin Zhang, Xujie Si, and Mayur Naik (Georgia Institute of Technology, USA; University of Pennsylvania, USA)
Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology.
@InProceedings{MAPL17p27,
author = {Xin Zhang and Xujie Si and Mayur Naik},
title = {Combining the Logical and the Probabilistic in Program Analysis},
booktitle = {Proc.\ MAPL},
publisher = {ACM},
pages = {2734},
doi = {10.1145/3088525.3088563},
year = {2017},
}
Publisher's Version
Article Search

23 authors
proc time: 0.06