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 a formal verification of OWL-S Process Models
    Ankolekar, A
    Paolucci, M
    Sycara, K
    SEMANTIC WEB - ISWC 2005, PROCEEDINGS, 2005, 3729 : 37 - 51
  • [2] Towards the Formal Verification of Optical Interconnects
    Afshar, Sanaz Khan
    Hasan, Osman
    Tahar, Sofiene
    2014 IEEE 12TH INTERNATIONAL NEW CIRCUITS AND SYSTEMS CONFERENCE (NEWCAS), 2014, : 157 - 160
  • [3] Towards formal verification of analog designs
    Gupta, S
    Krogh, BH
    Rutenbar, RA
    ICCAD-2004: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, IEEE/ACM DIGEST OF TECHNICAL PAPERS, 2004, : 210 - 217
  • [4] Towards Formal Verification of Distributed Algorithms
    Bollig, Benedikt
    2015 22ND INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING (TIME), 2015, : 3 - 3
  • [5] 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
  • [6] Towards formal verification on the system level
    Drechsler, R
    15TH IEEE INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, PROCEEDINGS: SHORTENING THE PATH FROM SPECIFICATION TO PROTOTYPE, 2004, : 2 - 5
  • [7] Towards formal verification of TOOLBUS scripts
    Fokkink, Wan
    Klint, Paul
    Lisser, Bert
    Usenko, Yaroslav S.
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2008, 5140 : 160 - 166
  • [8] 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
  • [9] Formal verification of a deadlock detection algorithm
    Verbeek, Freek
    Schmaltz, Julien
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (70): : 103 - 112
  • [10] Formal Modeling and Verification of Lycklama and Hadzilacos's Mutual Exclusion Algorithm
    Nigro, Libero
    MATHEMATICS, 2024, 12 (16)
12345