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] Towards Formal Verification of a TPM Software Stack
    Ziani, Yani
    Kosmatov, Nikolai
    Loulergue, Frederic
    Perez, Daniel Gracia
    Bernier, Teo
    INTEGRATED FORMAL METHODS, IFM 2023, 2024, 14300 : 93 - 112
  • [22] Towards formal verification of web service composition
    Rouached, Mohsen
    Perrin, Olivier
    Godart, Claude
    BUSINESS PROCESS MANAGEMENT, PROCEEDINGS, 2006, 4102 : 257 - 273
  • [23] 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
  • [24] Towards Formal Evaluation and Verification of Probabilistic Design
    Lee, Nian-Ze
    Jiang, Jie-Hong R.
    2014 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2014, : 340 - 347
  • [25] Towards Formal Verification of Optimized and Industrial Multipliers
    Mahzoon, Alireza
    Grosse, Daniel
    Scholl, Christoph
    Drechsler, Rolf
    PROCEEDINGS OF THE 2020 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE 2020), 2020, : 544 - 549
  • [26] 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
  • [27] 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
  • [28] ALGORITHM FOR FORMAL VERIFICATION OF BUSINESS PROCESS TEMPLATES
    Varosyan, A. S.
    CYBERNETICS AND SYSTEMS ANALYSIS, 2011, 47 (02) : 228 - 240
  • [29] Formal verification of the Ricart-Agrawala algorithm
    Sedletsky, E
    Pnueli, A
    Ben-Ari, M
    FST TCS 2000: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2000, 1974 : 325 - 335
  • [30] Towards a formal verification of process model's properties -: SimplePDL and TOCL case study
    Combemale, Benoit
    Garoche, Pieffe-Loiec
    Cregut, Xavier
    Thirioux, Xavier
    Vernadat, Francois
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: INFORMATION SYSTEMS ANALYSIS AND SPECIFICATION, 2007, : 80 - +
12345