Machine-checked Verification of Cognitive Agents

被引：3
|
作者：
Jensen, Alexander Birch [1 ]
机构：
[1] Tech Univ Denmark, DTU Compute Dept Appl Math & Comp Sci, Bldg 324, DK-2800 Lyngby, Denmark
来源：
ICAART: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE - VOL 1 | 2022年
关键词：
Cognitive Agent Systems; Formal Verification; Isabelle/HOL;
D O I：
10.5220/0010838700003116
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The ability to demonstrate reliability is an important aspect in deployment of software systems. This applies to cognitive multi-agent systems in particular due to their inherent complexity. We are still pursuing better approaches to demonstrate their reliability. The use of proof assistants and theorem proving has proven itself successful in verifying traditional software programs. This paper explores how to apply theorem proving to verify agent programs. We present our most recent work on formalizing a verification framework for cognitive agents using the proof assistant Isabelle/HOL.
引用
收藏
页码：245 / 256
页数：12
相关论文
共 50 条
  • [1] A machine-checked soundness proof for an efficient verification condition generator
    Vogels, Frédéric
    Jacobs, Bart
    Piessens, Frank
    [J]. Proceedings of the ACM Symposium on Applied Computing, 2010, : 2517 - 2522
  • [2] A machine-checked correctness proof for Pastry
    Azmy, Noran
    Merz, Stephan
    Weidenbach, Christoph
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 64 - 80
  • [3] A Machine-Checked Model of Safe Composition
    Delaware, Benjamin
    Cook, William
    Batory, Don
    [J]. FOAL09: FOUNDATIONS OF ASPECT-ORIENTED LANGUAGES, 2009, : 31 - 35
  • [4] Machine-Checked Semantic Session Typing
    Hinrichsen, Jonas Kastberg
    Louwrink, Daniel
    Krebbers, Robbert
    Bengtson, Jesper
    [J]. CPP '21: PROCEEDINGS OF THE 10TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2021, : 178 - 198
  • [5] A Machine-Checked Framework for Relational Separation Logic
    Manuel Crespo, Juan
    Kunz, Cesar
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 122 - 137
  • [6] A Machine-Checked Proof of the Odd Order Theorem
    Gonthier, Georges
    Asperti, Andrea
    Avigad, Jeremy
    Bertot, Yves
    Cohen, Cyril
    Garillot, Francois
    Le Roux, Stephane
    Mahboubi, Assia
    O'Connor, Russell
    Biha, Sidi Ould
    Pasca, Ioana
    Rideau, Laurence
    Solovyev, Alexey
    Tassi, Enrico
    Thery, Laurent
    [J]. INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 163 - 179
  • [7] Machine-Checked Proofs for Realizability Checking Algorithms
    Katis, Andreas
    Gacek, Andrew
    Whalen, Michael W.
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, 2016, 9593 : 110 - 123
  • [8] A Machine-Checked Implementation of Buchberger's Algorithm
    Laurent Théry
    [J]. Journal of Automated Reasoning, 2001, 26 : 107 - 137
  • [9] Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
    Chargueraud, Arthur
    Pottier, Francois
    [J]. INTERACTIVE THEOREM PROVING, 2015, 9236 : 137 - 153
  • [10] A machine-checked implementation of Buchberger's algorithm
    Théry, L
    [J]. JOURNAL OF AUTOMATED REASONING, 2001, 26 (02) : 107 - 137
12345