Verifying a local generic solver in Coq

Martin Hofmann; Aleksandr Karbyshev; Helmut Seidl

doi:10.1007/978-3-642-15769-1_21

Verifying a local generic solver in Coq

Martin Hofmann, Aleksandr Karbyshev, Helmut Seidl

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 Scopus citations

Abstract

Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solver RLD which can be applied to constraint systems x ⊇ f_x, x ∈ V, over some lattice D where the right-hand sides f _x are given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistant Coq.

Original language	English
Title of host publication	Static Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages	340-355
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-15769-1_21
State	Published - 2010
Event	17th International Static Analysis Symposium, SAS 2010 - Perpignan, France Duration: 14 Sep 2010 → 16 Sep 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6337 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Static Analysis Symposium, SAS 2010
Country/Territory	France
City	Perpignan
Period	14/09/10 → 16/09/10

Access to Document

10.1007/978-3-642-15769-1_21

Cite this

Hofmann, M., Karbyshev, A., & Seidl, H. (2010). Verifying a local generic solver in Coq. In Static Analysis - 17th International Symposium, SAS 2010, Proceedings (pp. 340-355). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS). https://doi.org/10.1007/978-3-642-15769-1_21

@inproceedings{9d5559c6df65478bb5a51768163356b1,

title = "Verifying a local generic solver in Coq",

abstract = "Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solver RLD which can be applied to constraint systems x ⊇ fx, x ∈ V, over some lattice D where the right-hand sides f x are given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistant Coq.",

author = "Martin Hofmann and Aleksandr Karbyshev and Helmut Seidl",

year = "2010",

doi = "10.1007/978-3-642-15769-1_21",

language = "English",

isbn = "3642157688",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "340--355",

booktitle = "Static Analysis - 17th International Symposium, SAS 2010, Proceedings",

note = "17th International Static Analysis Symposium, SAS 2010 ; Conference date: 14-09-2010 Through 16-09-2010",

}

Hofmann, M, Karbyshev, A & Seidl, H 2010, Verifying a local generic solver in Coq. in Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6337 LNCS, pp. 340-355, 17th International Static Analysis Symposium, SAS 2010, Perpignan, France, 14/09/10. https://doi.org/10.1007/978-3-642-15769-1_21

Verifying a local generic solver in Coq. / Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut.
Static Analysis - 17th International Symposium, SAS 2010, Proceedings. 2010. p. 340-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6337 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verifying a local generic solver in Coq

AU - Hofmann, Martin

AU - Karbyshev, Aleksandr

AU - Seidl, Helmut

PY - 2010

Y1 - 2010

N2 - Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solver RLD which can be applied to constraint systems x ⊇ fx, x ∈ V, over some lattice D where the right-hand sides f x are given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistant Coq.

AB - Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solver RLD which can be applied to constraint systems x ⊇ fx, x ∈ V, over some lattice D where the right-hand sides f x are given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistant Coq.

UR - http://www.scopus.com/inward/record.url?scp=78149238250&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-15769-1_21

DO - 10.1007/978-3-642-15769-1_21

M3 - Conference contribution

AN - SCOPUS:78149238250

SN - 3642157688

SN - 9783642157684

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 340

EP - 355

BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings

T2 - 17th International Static Analysis Symposium, SAS 2010

Y2 - 14 September 2010 through 16 September 2010

ER -

Verifying a local generic solver in Coq

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this