Formally Verified Resource Bounds through Implicit Computational Complexity

被引：0
|
作者：
Rusch, Neea [1 ]
机构：
[1] Augusta Univ, Augusta, GA 30912 USA
来源：
COMPANION PROCEEDINGS OF THE 2022 ACM SIGPLAN INTERNATIONAL CONFERENCE ON SYSTEMS, PROGRAMMING, LANGUAGES, AND APPLICATIONS: SOFTWARE FOR HUMANITY, SPLASH COMPANION 2022 | 2022年
关键词：
Implicit Computational Complexity; Automatic Complexity Analysis; Program Verification;
D O I：
10.1145/3563768.3565545
中图分类号：
学科分类号：
摘要：
Automatic complexity analysis has not reached mainstream adoption due to outstanding challenges, such as scalability and usability, and no formally verified analyzer exists. However, the need to evaluate resource usage is crucial: even a guaranteed correct program, whose memory usage exceeds available resources, is unreliable. The field of Implicit Computational Complexity (ICC) offers a potential avenue to resolving some of these outstanding challenges by introducing unique, machine-independent, and flexible approaches to program analysis. But since ICC techniques are mostly theoretical, it is unclear how strongly these assumptions hold in practice. This project defines a 3-directional plan-focused on practical analysis, compiler-integration, and formal verification-to assess the suitability of ICC to address outstanding challenges in automatic complexity analysis.
引用
收藏
页码：17 / 20
页数：4
相关论文
共 50 条
  • [41] Computational complexity of determining resource loops in reentrant plow lines
    Lewis, FL
    Horne, BG
    Abdallah, CT
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2000, 30 (02): : 222 - 229
  • [42] Recognition of Activities in Resource Constrained Environments; Reducing the Computational Complexity
    Espinilla, M.
    Rivera, A.
    Perez-Godoy, M. D.
    Medina, J.
    Martinez, L.
    Nugent, C.
    UBIQUITOUS COMPUTING AND AMBIENT INTELLIGENCE, UCAMI 2016, PT II, 2016, 10070 : 64 - 74
  • [43] APPLICATIONS OF MATRIX-METHODS TO THE THEORY OF LOWER BOUNDS IN COMPUTATIONAL-COMPLEXITY
    RAZBOROV, AA
    COMBINATORICA, 1990, 10 (01) : 81 - 93
  • [44] A UNIFORM METHOD FOR PROVING LOWER BOUNDS ON THE COMPUTATIONAL-COMPLEXITY OF LOGICAL THEORIES
    COMPTON, KJ
    HENSON, CW
    ANNALS OF PURE AND APPLIED LOGIC, 1990, 48 (01) : 1 - 79
  • [45] On fundamental tradeoffs between delay bounds and computational complexity in packet scheduling algorithms
    Xu, JJ
    Lipton, RJ
    IEEE-ACM TRANSACTIONS ON NETWORKING, 2005, 13 (01) : 15 - 28
  • [46] Fine-Grained Complexity Theory: Conditional Lower Bounds for Computational Geometry
    Bringmann, Karl
    CONNECTING WITH COMPUTABILITY, 2021, 12813 : 60 - 70
  • [47] On fundamental tradeoffs between delay bounds and computational complexity in packet scheduling algorithms
    Xu, J
    Lipton, RJ
    ACM SIGCOMM COMPUTER COMMUNICATION REVIEW, 2002, 32 (04) : 279 - 292
  • [48] Low Computational Complexity Design of Resource Sharing and Precoding for Multicast Services
    Exposito, Victor
    Gresset, Nicolas
    2018 25TH INTERNATIONAL CONFERENCE ON TELECOMMUNICATIONS (ICT), 2018, : 27 - 31
  • [49] Computational complexity and approximability of social welfare optimization in multiagent resource allocation
    Nhan-Tam Nguyen
    Trung Thanh Nguyen
    Magnus Roos
    Jörg Rothe
    Autonomous Agents and Multi-Agent Systems, 2014, 28 : 256 - 289
  • [50] Computational complexity and approximability of social welfare optimization in multiagent resource allocation
    Nhan-Tam Nguyen
    Trung Thanh Nguyen
    Roos, Magnus
    Rothe, Joerg
    AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2014, 28 (02) : 256 - 289
12345