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 a general methodology for formal verification on spiking neural P systems [J].

Perez-Jimenez, Mario J. ;

Valencia-Cabrera, Luis ;

Orellana-Martin, David ;

Ramirez-de-Arellano, Antonio .

THEORETICAL COMPUTER SCIENCE, 2024, 1011

[22] Formal Verification Problems in a Big Data World: Towards a Mighty Synergy [J].

Camilli, Matteo .

36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE COMPANION 2014), 2014, :638-641

[23] Towards Formal Verification of Node RED-Based IoT Applications [J].

Garfatta, Ikram ;

Souid, Nour Elhouda ;

Klai, Kais .

VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS, VECOS 2023, 2024, 14368 :90-104

[24] Towards Hazard Analysis Result Verification for Autonomous Ships: A Formal Verification Method Based on Timed Automata [J].

Zhou, Xiang-Yu ;

Jin, Shiqi ;

Mei, Yang ;

Sun, Xu ;

Yang, Xue ;

Nie, Shengzheng ;

Zhang, Wenjun .

JOURNAL OF MARINE SCIENCE AND ENGINEERING, 2025, 13 (06)

[25] Formal verification of an access concurrency control algorithm for transaction time relations [J].

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-+

[26] Towards Embedded Systems Formal Verification Translation from SysML into Petri Nets [J].

Szmuc, Wojciech ;

Szmuc, Tomasz .

PROCEEDINGS OF THE 25TH INTERNATIONAL CONFERENCE MIXED DESIGN OF INTEGRATED CIRCUITS AND SYSTEM (MIXDES 2018), 2018, :420-423

[27] Towards Formal Verification of Plans for Cognition-enabled Autonomous Robotic Agents [J].

Meywerk, Tim ;

Walter, Marcel ;

Herdt, Vladimir ;

Grosse, Daniel ;

Drechsler, Rolf .

2019 22ND EUROMICRO CONFERENCE ON DIGITAL SYSTEM DESIGN (DSD), 2019, :129-136

[28] Towards Trustworthy RISC-V Designs: Formal Verification of the MFENCE Instruction [J].

Ponugoti, Kushal K. ;

Karlapalem, Nikhila .

4TH INTERDISCIPLINARY CONFERENCE ON ELECTRICS AND COMPUTER, INTCEC 2024, 2024,

[29] Towards Correct Smart Contracts: A Case Study on Formal Verification of Access Control [J].

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

[30] Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management [J].

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

← 1 2 3 4 5 →