External Behavior of a Logic Program and Verification of Refactoring

被引：2
|
作者：
Fandinno, Jorge [1 ]
Hansen, Zachary [1 ]
Lierler, Yuliya [1 ]
Lifschitz, Vladimir [2 ]
Temple, Nathan [2 ]
机构：
[1] Univ Nebraska, Omaha, NE 68182 USA
[2] Univ Texas Austin, Austin, TX USA
来源：
THEORY AND PRACTICE OF LOGIC PROGRAMMING | 2023年 / 23卷 / 04期
关键词：
answer set programming; software verification; proof assistant; automated reasoning;
D O I：
10.1017/S1471068423000200
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.
引用
收藏
页码：933 / 947
页数：15
相关论文
共 50 条
  • [21] LEVER. A logic extraction and verification program for MOS circuits
    Wang, P.-H.P.
    McNamee, L.
    Proceedings of the ISMM International Symposium Computer Applications in Design, Simulation and Analysis, 1991,
  • [22] Testing First-Order Logic Axioms in Program Verification
    Ahn, Ki Yung
    Denney, Ewen
    TEST AND PROOFS, PROCEEDINGS, 2010, 6143 : 22 - +
  • [23] From Rewriting Logic, to Programming Language Semantics, to Program Verification
    Rosu, Grigore
    LOGIC, REWRITING, AND CONCURRENCY, 2015, 9200 : 598 - 616
  • [24] Matching Logic: A New Program Verification Approach (NIER Track)
    Rosu, Grigore
    Stefanescu, Andrei
    2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2011, : 868 - 871
  • [25] Syntax-driven Program Verification of Matching Logic Properties
    Bianculli, Domenico
    Filieri, Antonio
    Ghezzi, Carlo
    Mandrioli, Dino
    Rizzi, Alessandro Maria
    2015 IEEE/ACM 3RD FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING, 2015, : 68 - 74
  • [26] Modelling and verification of program logic controllers using timed automata
    Wang, R.
    Song, X.
    Gu, M.
    IET SOFTWARE, 2007, 1 (04) : 127 - 131
  • [27] HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification
    Garcia, Luis
    Mitsch, Stefan
    Platzer, Andre
    ICCPS '19: PROCEEDINGS OF THE 2019 10TH ACM/IEEE INTERNATIONAL CONFERENCE ON CYBER-PHYSICAL SYSTEMS, 2019, : 47 - 56
  • [28] Verification of Cooperative Vehicle Behavior using Temporal Logic
    Voelker, Marcus
    Kloock, Maximilian
    Rabanus, Leon
    Alrifaee, Bassam
    Kowalewski, Stefan
    IFAC PAPERSONLINE, 2019, 52 (08): : 99 - 104
  • [29] Synchronizing Model and Program Refactoring
    Massoni, Tiago
    Gheyi, Rohit
    Borba, Paulo
    FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, 2011, 6527 : 96 - +
  • [30] Java']Java program verification via a Hoare logic with abrupt termination
    Huisman, M
    Jacobs, B
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2000, 1783 : 284 - 303
12345