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 条

[41] Planning for Change in a Formal Verification of the Raft Consensus Protocol [J].

Woos, Doug ;

Wilcox, James R. ;

Anton, Steve ;

Tatlock, Zachary ;

Ernst, Michael D. ;

Anderson, Thomas .

PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, :154-165

[42] Methods of Formal Software Verification in the Context of Distributed Systems [J].

Fatkina, Anna ;

Iakushkin, Oleg ;

Selivanov, Dmitry ;

Korkhov, Vladimir .

COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2019, PT II: 19TH INTERNATIONAL CONFERENCE, SAINT PETERSBURG, RUSSIA, JULY 1-4, 2019, PROCEEDINGS, PART II, 2019, 11620 :546-555

[43] Formal Verification of a Space System's User Interface With the IVY Workbench [J].

Campos, Jose Creissac ;

Sousa, Manuel ;

Bergue Alves, Miriam C. ;

Harrison, Michael D. .

IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS, 2016, 46 (02) :303-316

[44] Coverage metrics for formal verification [J].

Hana Chockler ;

Orna Kupferman ;

Moshe Vardi .

International Journal on Software Tools for Technology Transfer, 2006, 8 (4-5) :373-386

[45] Polynomial Formal Verification of Multipliers [J].

Martin Keim ;

Rolf Drechsler ;

Bernd Becker ;

Michael Martin ;

Paul Molitor .

Formal Methods in System Design, 2003, 22 :39-58

[46] The MODUS Approach to Formal Verification [J].

Brewka, Lukasz ;

Soler, Jose ;

Berger, Michael .

BUSINESS SYSTEMS RESEARCH JOURNAL, 2014, 5 (01) :21-33

[47] Formal Verification of a Transistor PCell [J].

Langner, Kerstin ;

Scheible, Juergen .

2017 13TH CONFERENCE ON PH.D. RESEARCH IN MICROELECTRONICS AND ELECTRONICS (PRIME), 2017, :205-208

[48] Formal Verification of the Sumcheck Protocol [J].

Bosshard, Azucena Garvia ;

Bootle, Jonathan ;

Sprenger, Christoph .

2024 IEEE 37TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, CSF 2024, 2024, :605-619

[49] Formal Verification of Differential Privacy [J].

Gaboardi, Marco .

PLAS'18: PROCEEDINGS OF THE 13TH WORKSHOP ON PROGRAMMING LANGUAGES AND ANALYSIS FOR SECURITY, 2018, :1-1

[50] Polynomial formal verification of multipliers [J].

Keim, M ;

Drechsler, R ;

Becker, B ;

Martin, M ;

Molitor, P .

FORMAL METHODS IN SYSTEM DESIGN, 2003, 22 (01) :39-58

← 1 2 3 4 5 →