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 条

[31] Late Breaking Results: Towards Efficient Formal Verification of Dot Product Architectures [J].

Weingarten, Lennart ;

Datta, Kamalika ;

Drechsler, Rolf .

2025 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE, DATE, 2025,

[32] Formal Verification of Websites [J].

Flores, Sonia ;

Lucas, Salvador ;

Villanueva, Alicia .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) :103-118

[33] Formal Verification of a Keystore [J].

Boender, Jaap ;

Badevic, Goran .

THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 :49-64

[34] Formal verification of μ-charts [J].

Goldson, D .

APSEC 2002: NINTH ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, 2002, :129-136

[35] Formal Specification and Verification of JXTA's Endpoint Routing Protocol [J].

Konga, Yannick L. Kala ;

Djouani, Karim .

IEEE AFRICON 2011, 2011,

[36] Formal verification of cP systems using Coq [J].

Yezhou Liu ;

Radu Nicolescu ;

Jing Sun .

Journal of Membrane Computing, 2021, 3 :205-220

[37] Formal verification of cP systems using Coq [J].

Liu, Yezhou ;

Nicolescu, Radu ;

Sun, Jing .

JOURNAL OF MEMBRANE COMPUTING, 2021, 3 (03) :205-220

[38] Formal Verification and Co-Simulation in the Design of a Synchronous Motor Control Algorithm [J].

Bernardeschi, Cinzia ;

Dini, Pierpaolo ;

Domenici, Andrea ;

Palmieri, Maurizio ;

Saponara, Sergio .

ENERGIES, 2020, 13 (16)

[39] Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic [J].

Marconi, Francesco ;

Bersani, Marcello M. ;

Erascu, Madalina ;

Rossi, Matteo .

FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2016, 2016, 10009 :193-209

[40] Towards the Formal Verification of SysML Specifications : Translation of Activity Diagrams into Modular Petri Nets [J].

Rahim, Messaoud ;

Hammad, Ahmed ;

Boukala-Ioualalen, Malika .

3RD INTERNATIONAL CONFERENCE ON APPLIED COMPUTING AND INFORMATION TECHNOLOGY (ACIT 2015) 2ND INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE AND INTELLIGENCE (CSI 2015), 2015, :509-516

← 1 2 3 4 5 →