检索结果-内蒙古大学图书馆

25th International Symposium on Trends in Functional Programming

作者： Wu, Dongyu Fluet, Matthew Rochester Inst Technol Rochester NY 14623 USA

ISBN: (纸本)9783031745577;9783031745584

A type- and control-flow analysis is a program analysis that yields both type-flow information, approximating the types that may instantiate type variables, and control-flow information, approximating the values (especially lambda- and Lambda-expressions) that may be bound to variables. Moreover, each of the flows informs the other;control-flow establishes the types that may instantiate Lambda-bound type variables by determining the Lambda-expressions that flow to a type-application expression, while type-flow filters control-flow by rejecting the flow of values having static types that are incompatible (according to the type-flow information) with the static type of the receiving variable. In previous work [1,13,14], we introduced a (monovariant) type- and control-flow analysis for System F (with recursion). While System F has an expressive type system and has served as a useful core calculus in which to express interesting language features, it only allows abstraction over types and does not allow abstraction over type constructors. Increasingly, researchers are looking at System F-omega, with both term- and type-level abstraction over types of arbitrary kind, as a core calculus in which to explore advanced language features. Hence, we are motivated to define a type- and control-flow analysis for System F-omega that is able to analyze the rich structure of System F-omega types. In this work, we present a preliminary type- and control-flow analysis for System F-omega (with recursion). As in previous work, we give both a specification-based formulation of the analysis, used to prove soundness of the analysis, and a flow-graph-based formulation, used to guide the implementation of an algorithm. While the macro structure of the development for System F-omega follows that for System F, moving to System F-omega introduces subtle challenges that have left some unanswered questions about the meta-theory. In particular, the decidability of type compatibility defined in ter

关键词： control-flow analysis Type-flow analysis System F-omega

来源：评论

学校读者我要写书评

暂无评论

Pushdown control-flow analysis for Free 16

Pushdown Control-Flow Analysis for Free

引用

43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

作者： Gilray, Thomas Lyde, Steven Adams, Michael D. Might, Matthew Van Horn, David Univ Utah Salt Lake City UT 84112 USA Univ Maryland Bethesda MD USA

ISBN: (纸本)9781450335492

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been published that provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, implementing CFA2 and PDCFA requires significant engineering effort. Furthermore, all three are computationally expensive. For a monovariant analysis, CFA2 is in O(2(n)), PDCFA is in O(n(6)), and AAC is in O(n(8)). In this paper, we describe a new technique that builds on these but is both straightforward to implement and computationally inexpensive. The crucial insight is an unusual state-dependent allocation strategy for the addresses of continuations. Our technique imposes only a constant-factor overhead on the underlying analysis and costs only O(n(3)) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis.

关键词： Static analysis control-flow analysis Abstract interpretation Pushdown analysis Store-allocated continuations

来源：评论

学校读者我要写书评

暂无评论

Allocation Characterizes Polyvariance A Unified Methodology for Polyvariant control-flow analysis 2016

Allocation Characterizes Polyvariance A Unified Methodology ...

引用

21st ACM SIGPLAN International Conference on Functional Programming (ICFP)

作者： Gilray, Thomas Adams, Michael D. Might, Matthew Univ Utah Salt Lake City UT 84112 USA

ISBN: (纸本)9781450342193

The polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off an analysis strikes between precision and complexity. For example, call sensitivity supposes that values will tend to correlate with recent call sites, object sensitivity supposes that values will correlate with the allocation points of related objects, the Cartesian product algorithm supposes correlations between the values of arguments to the same function, and so forth. In this paper, we describe a unified methodology for implementing and understanding polyvariance in a higher-order setting (i.e., for control-flow analyses). We do this by extending the method of abstracting abstract machines (AAM), a systematic approach to producing an abstract interpretation of abstract-machine semantics. AAM eliminates recursion within a language's semantics by passing around an explicit store, and thus places importance on the strategy an analysis uses for allocating abstract addresses within the abstract heap or store. We build on AAM by showing that the design space of possible abstract allocators exactly and uniquely corresponds to the design space of polyvariant strategies. This allows us to both unify and generalize polyvariance as tunings of a single function. Changes to the behavior of this function easily recapitulate classic styles of analysis and produce novel variations, combinations of techniques, and fundamentally new techniques.

关键词： Polyvariance Static analysis control-flow analysis Abstract interpretation Abstract allocation Context sensitivity

来源：评论

学校读者我要写书评

暂无评论

Allocation Characterizes Polyvariance A Unified Methodology for Polyvariant control-flow analysis

引用

ACM SIGPLAN NOTICES 2016年第9期51卷 407-420页

作者： Gilray, Thomas Adams, Michael D. Might, Matthew Univ Utah Salt Lake City UT 84112 USA

关键词： Polyvariance Static analysis control-flow analysis Abstract interpretation Abstract allocation Context sensitivity

来源：评论

学校读者我要写书评

暂无评论

Pushdown control-flow analysis for Free

引用

ACM SIGPLAN NOTICES 2016年第1期51卷 691-704页

作者： Gilray, Thomas Lyde, Steven Adams, Michael D. Might, Matthew Van Horn, David Univ Utah Salt Lake City UT 84112 USA Univ Maryland Bethesda MD USA

关键词： Static analysis control-flow analysis Abstract interpretation Pushdown analysis Store-allocated continuations

来源：评论

学校读者我要写书评

暂无评论

A Methodology for the analysis of Robotic Systems via Process Mining 27th

A Methodology for the Analysis of Robotic Systems via Proces...

引用

27th International Conference on Enterprise Design, Operations, and Computing (EDOC)

作者： Corradini, Flavio Pettinari, Sara Re, Barbara Rossi, Lorenzo Tiezzi, Francesco Univ Camerino Sch Sci & Technol Camerino Italy Univ Florence Applicaz Informat Dipartimento Stat Florence Italy

ISBN: (纸本)9783031465864;9783031465871

Robotic systems are widely adopted in various application scenarios. A very complex task for developers is the analysis of robotic systems' behavior, which is required to ensure trustworthy interaction with the surrounding environment. Available analysis techniques, like field tests, depend on human observations, while automated techniques, like formal analysis, suffer from the complexity of the systems. Recent works show the applicability of process mining for the analysis of event data generated by robots to increase the understanding of system behavior. However, robots produce data at such a low granularity that process mining cannot provide a meaningful description of the system's behavior. We tackle this problem by proposing a process mining-based methodology to prepare and analyze the data coming from the execution of a robotic system. The methodology supports the system developer in producing an event log compliant with process mining techniques and is used to analyze multiple perspectives of robots' behavior. We implemented the methodology in a tool supporting its phases. We use the tool on a robotic smart agriculture scenario to evaluate the feasibility and effectiveness of the methodology.

关键词： Robotic Systems Process Mining Multi-Perspective Event Logs control-flow analysis Spatial analysis

来源：评论

学校读者我要写书评

暂无评论

m-CFA Exhibits Perfect Stack Precision 21st

m-CFA Exhibits Perfect Stack Precision

引用

21st Asian Symposium on Programming Languages and Systems (APLAS)

作者： Germane, Kimball Brigham Young Univ Provo UT 84601 USA

ISBN: (纸本)9789819983100;9789819983117

m-CFA is a hierarchy of control-flow analyses (CFA) formulated as abstract machines and designed to exhibit polynomial time complexity while remaining usefully precise. The Pushdown for Free technique (P4F) prescribes a continuation allocator which induces perfect stack precision wherein each function invocation returns to only its call. Unfortunately, it is difficult to apply P4F to m-CFA as P4F is developed in an ANF setting but m-CFA is formulated in a CPS setting. In this paper, we recall that ANF corresponds to a CPS sublanguage without non-local control and show that m-CFA behaves identically on both. With an ANF-based m-CFA in hand, we turn to applying P4F only to discover that it already follows the prescription. In other words, m-CFA has always had perfect stack precision, a characteristic neither intended nor recognized, at its development or since. In addition to being surprising, we discuss how this result allows a spectrum of non-local control constructs to be supported more easily and with more precision than previous techniques.

关键词： Static analysis control-flow analysis Abstract interpretation

来源：评论

学校读者我要写书评

暂无评论

Beyond Relooper: Recursive Translation of Unstructured control flow to Structured control flow (Functional Pearl)

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2022年第ICFP期6卷 1–22页

作者： Ramsey, Norman Tweag Paris France Tufts Univ Medford MA 02155 USA

In many compilers, control flow is represented using an arbitrary directed graph. But in some interesting target languages, including JavaScript and WebAssembly, intraprocedural control flow can be expressed only in structured ways, using loops, conditionals, and multilevel breaks or exits. As was shown by Peterson, Kasami, and Tokura in 1973, such structured control flow can be obtained by translating arbitrary control flow. The translation uses two standard analyses, but as published, it takes three passes-Dwhich may explain why it was overlooked by Emscripten, a popular compiler from C to JavaScript. By tweaking the analyses and by applying fundamental ideas from functional programming (recursive functions and immutable abstract-syntax trees), the translation, along with a couple of code improvements, can be implemented in a single pass. This new implementation is slated to be added to the Glasgow Haskell Compiler. Its single-pass translation, its immutable representation, and its use of dominator trees make it much easier to reason about than the original translation.

关键词： WebAssembly control-flow analysis dominator tree reverse postorder numbering Haskell

来源：评论

学校读者我要写书评

暂无评论

Newly-single and loving it: improving higher-order must-alias analysis with heap fragments

Newly-single and loving it: improving higher-order must-alia...

引用

作者： Germane, Kimball Mccarthy, Jay Brigham Young University ProvoUT United States University of Massachusetts at Lowell LowellMA United States

Theories of higher-order must-alias analysis, often under the guise of environment analysis, provide deep behavioral insight. But these theories - -in particular those that are most insightful otherwise - -can reason about recursion only in limited cases. This weakness is not inherent to the theories but to the frameworks in which they're defined: machine models which thread the heap through evaluation. Since these frameworks allocate each abstract resource in the heap, the constituent theories of environment analysis conflate co-live resources identified in the abstract, such as recursively-created bindings. We present heap fragments as a general technique to allow these theories to reason about recursion in a general and robust way. We instantiate abstract counting in a heap-fragment framework and compare its performance to a precursor entire-heap framework. We also sketch an approach to realizing binding invariants, a more powerful environment analysis, in the heap-fragment framework. © 2021 Owner/Author.

关键词： abstract counting control-flow analysis heap fragments must-alias analysis

来源：评论

学校读者我要写书评

暂无评论

Newly-Single and Loving It: Improving Higher-Order Must-Alias analysis with Heap Fragments

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2021年第ICFP期5卷 1–28页

作者： Germane, Kimball McCarthy, Jay Brigham Young Univ Provo UT 84602 USA Univ Massachusetts Lowell Lowell MA USA

Theories of higher-order must-alias analysis, often under the guise of environment analysis, provide deep behavioral insight. But these theories-in particular those that are most insightful otherwise-can reason about recursion only in limited cases. This weakness is not inherent to the theories but to the frameworks in which they're defined: machine models which thread the heap through evaluation. Since these frameworks allocate each abstract resource in the heap, the constituent theories of environment analysis conflate co-live resources identified in the abstract, such as recursively-created bindings. We present heap fragments as a general technique to allow these theories to reason about recursion in a general and robust way. We instantiate abstract counting in a heap-fragment framework and compare its performance to a precursor entire-heap framework. We also sketch an approach to realizing binding invariants, a more powerful environment analysis, in the heap-fragment framework.

关键词： control-flow analysis must-alias analysis abstract counting heap fragments

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：