Towards the Formal Verification of Wigderson's Algorithm

被引：0
作者：
Phipathananunth, Siraphob [1 ]
机构：
[1] Yale Univ, New Haven, CT 06520 USA
来源：
COMPANION PROCEEDINGS OF THE 2023 ACM SIGPLAN INTERNATIONAL CONFERENCE ON SYSTEMS, PROGRAMMING, LANGUAGES, AND APPLICATIONS: SOFTWARE FOR HUMANITY, SPLASH COMPANION 2023 | 2023年
关键词：
formal verification; coq; graph coloring; approximation algorithms;
D O I：
10.1145/3618305.3623600
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present progress towards the formal verification of Wigderson's graph coloring algorithm in Coq. We have created a library of formalized graph theory that aims to bridge the literature gap between introductory material on Coq and large-scale formal developments, while providing a motivating case study. Our library contains over 180 proven theorems. The development is available at https://github.com/siraben/coq-wigderson.
引用
收藏
页码：40 / 42
页数：3
相关论文
共 50 条
  • [21] Formal Verification Problems in a Big Data World: Towards a Mighty Synergy
    Camilli, Matteo
    36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE COMPANION 2014), 2014, : 638 - 641
  • [22] Towards Formal Verification of Node RED-Based IoT Applications
    Garfatta, Ikram
    Souid, Nour Elhouda
    Klai, Kais
    VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS, VECOS 2023, 2024, 14368 : 90 - 104
  • [23] Formal verification of an access concurrency control algorithm for transaction time relations
    Makni, Achraf
    Bouaziz, Rafik
    Gargouri, Faiez
    ICEIS 2006: PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATIONAL SYSTEMS: DATABASES AND INFORMATION SYSTEMS INTEGRATION, 2006, : 269 - +
  • [24] Towards Embedded Systems Formal Verification Translation from SysML into Petri Nets
    Szmuc, Wojciech
    Szmuc, Tomasz
    PROCEEDINGS OF THE 25TH INTERNATIONAL CONFERENCE MIXED DESIGN OF INTEGRATED CIRCUITS AND SYSTEM (MIXDES 2018), 2018, : 420 - 423
  • [25] Towards Trustworthy RISC-V Designs: Formal Verification of the MFENCE Instruction
    Ponugoti, Kushal K.
    Karlapalem, Nikhila
    4TH INTERDISCIPLINARY CONFERENCE ON ELECTRICS AND COMPUTER, INTCEC 2024, 2024,
  • [26] Towards Formal Verification of Plans for Cognition-enabled Autonomous Robotic Agents
    Meywerk, Tim
    Walter, Marcel
    Herdt, Vladimir
    Grosse, Daniel
    Drechsler, Rolf
    2019 22ND EUROMICRO CONFERENCE ON DIGITAL SYSTEM DESIGN (DSD), 2019, : 129 - 136
  • [27] Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control
    Schiffl, Jonas
    Grundmann, Matthias
    Leinweber, Marc
    Stengele, Oliver
    Friebe, Sebastian
    Beckert, Bernhard
    PROCEEDINGS OF THE 26TH ACM SYMPOSIUM ON ACCESS CONTROL MODELS AND TECHNOLOGIES, SACMAT 2021, 2021, : 125 - 130
  • [28] Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
    Zhao, Xingyu
    Osborne, Matt
    Lantair, Jenny
    Robu, Valentin
    Flynn, David
    Huang, Xiaowei
    Fisher, Michael
    Papacchini, Fabio
    Ferrando, Angelo
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2019), 2019, 11724 : 105 - 124
  • [29] Formal Verification of Websites
    Flores, Sonia
    Lucas, Salvador
    Villanueva, Alicia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) : 103 - 118
  • [30] Formal Verification of a Keystore
    Boender, Jaap
    Badevic, Goran
    THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 49 - 64
12345