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

被引：0
|
作者：
Nagy, Shaan [1 ]
Kim, Jinwoo [2 ]
Reps, Thomas [1 ]
D'Antoni, Loris [3 ]
机构：
[1] University of Wisconsin-Madison, Madison, United States
[2] Seoul National University, Seoul, Korea, Republic of
[3] University of California San Diego, San Diego, United States
来源：
Proceedings of the ACM on Programming Languages | 2024年 / 8卷 / OOPSLA2期
关键词：
D O I：
10.1145/3689715
中图分类号：
学科分类号：
摘要：
25
引用
收藏
页码：113 / 139
相关论文
共 8 条
  • [1] Hoare-Style Logic for Unstructured Programs
    Lundberg, Didrik
    Guanciale, Roberto
    Lindner, Andreas
    Dam, Mads
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2020, 2020, 12310 : 193 - 213
  • [2] A Hoare-style proof system for robot programs
    Liu, YM
    EIGHTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-02)/FOURTEENTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-02), PROCEEDINGS, 2002, : 74 - 79
  • [3] Hoare-Style Verification of Graph Programs
    Poskitt, Christopher M.
    Plump, Detlef
    FUNDAMENTA INFORMATICAE, 2012, 118 (1-2) : 135 - 175
  • [4] Probabilistic Modal Kleene Algebra and Hoare-style Logic
    Qiao, Rui
    Wu, Jinzhao
    Gao, Xinyan
    ICNC 2008: FOURTH INTERNATIONAL CONFERENCE ON NATURAL COMPUTATION, VOL 3, PROCEEDINGS, 2008, : 652 - +
  • [5] A Probabilistic Hoare-style logic for game-based cryptographic proofs
    Gorin, Ricardo
    den Hartog, Jerry
    AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, 2006, 4052 : 252 - 263
  • [6] Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency
    Turon, Aaron
    Dreyer, Derek
    Birkedal, Lars
    ACM SIGPLAN NOTICES, 2013, 48 (09) : 377 - 390
  • [7] Neuro-symbolic Representation of Logic Programs Defining Infinite Sets
    Komendantskaya, Ekaterina
    Broda, Krysia
    Garcez, Artur d'Avila
    ARTIFICIAL NEURAL NETWORKS-ICANN 2010, PT I, 2010, 6352 : 301 - +
  • [8] Synthesis of positive logic programs for checking a class of definitions with infinite quantification
    Galan, Francisco J.
    Canete-Valdeon, Jose M.
    INFORMATION AND COMPUTATION, 2016, 249 : 205 - 236
1