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 条
  • [1] Towards Formal Verification of Program Obfuscation
    Lu, Weiyun
    Sistany, Bahman
    Felty, Amy
    Scott, Philip
    2020 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (EUROS&PW 2020), 2020, : 635 - 644
  • [2] A FORMAL VERIFICATION ALGORITHM FOR PIPELINED PROCESSORS
    SHONAI, T
    SHIMIZU, T
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1995, E78A (05) : 618 - 631
  • [3] Towards formal verification of IoT protocols: A Review
    Hofer-Schmitz, Katharina
    Stojanovic, Branka
    COMPUTER NETWORKS, 2020, 174
  • [4] Towards formal verification of ASIP based on HDPN
    Gao, Yanyan
    Li, Xi
    Ma, Hongxing
    ICECT: 2009 INTERNATIONAL CONFERENCE ON ELECTRONIC COMPUTER TECHNOLOGY, PROCEEDINGS, 2009, : 26 - 32
  • [5] Dynamic GSPNs: formal definition, transformation towards GSPNs and formal verification
    Tigane, Samir
    Kahloul, Laid
    Baarir, Souheib
    Bourekkache, Samir
    PROCEEDINGS OF THE 13TH EAI INTERNATIONAL CONFERENCE ON PERFORMANCE EVALUATION METHODOLOGIES AND TOOLS ( VALUETOOLS 2020), 2020, : 164 - 171
  • [6] ALGORITHM FOR FORMAL VERIFICATION OF BUSINESS PROCESS TEMPLATES
    Varosyan, A. S.
    CYBERNETICS AND SYSTEMS ANALYSIS, 2011, 47 (02) : 228 - 240
  • [7] Formal Verification of a Distributed Algorithm for Task Execution
    Nath, Amar
    Niyogi, Rajdeep
    COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2020, PT V, 2020, 12253 : 120 - 131
  • [8] Towards formal verification of cryptographic circuits: A functional approach
    Bitat, Abir
    Merniz, Salah
    2018 3RD INTERNATIONAL CONFERENCE ON PATTERN ANALYSIS AND INTELLIGENT SYSTEMS (PAIS), 2018, : 158 - 163
  • [9] Formal Modelling and Verification of the Clock Synchronisation Algorithm of FlexRay
    Asokan, Shimmi
    Kochaleema, K. H.
    Kumar, G. Santhosh
    DEFENCE SCIENCE JOURNAL, 2023, 73 (01) : 41 - 50
  • [10] Towards Formal Verification of Adaptive Cruise Controller using SpaceEx
    Mishra, Ambuj
    Roy, Subir K.
    2016 INTERNATIONAL CONFERENCE ON VLSI SYSTEMS, ARCHITECTURES, TECHNOLOGY AND APPLICATIONS (VLSI-SATA), 2016,
12345