LCTD: Tests-Guided Proofs for C Programs on LLVM

Olli Saarikivi; Keijo Heljanko

doi:10.1007/978-3-662-49674-9_62

LCTD: Tests-Guided Proofs for C Programs on LLVM

Olli Saarikivi^*, Keijo Heljanko

^*Corresponding author for this work

Department of Computer Science

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

1 Citation (Scopus)

Abstract

LCTD is an open source verification tool for C programs. It uses the LLVM compiler framework to instrument programs for verification with the DASH algorithm. LCTD has been submitted to the BitVectorsReach category of SV-COMP 2016.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Marsha Chechik, Jean-Francois Raskin
Publisher	Springer Verlag
Pages	927-929
Number of pages	3
Volume	9636
ISBN (Electronic)	978-3-662-49674-9
ISBN (Print)	978-3-662-49673-2
DOIs	https://doi.org/10.1007/978-3-662-49674-9_62
Publication status	Published - 2016
MoE publication type	A4 Article in a conference publication
Event	International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016 Conference number: 22

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9636
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated title	TACAS
Country	Netherlands
City	Eindhoven
Period	02/04/2016 → 08/04/2016

Access to Document

10.1007/978-3-662-49674-9_62

Link to publication in Scopus

Fingerprint Dive into the research topics of 'LCTD: Tests-Guided Proofs for C Programs on LLVM'. Together they form a unique fingerprint.

Cite this

Saarikivi, O., & Heljanko, K. (2016). LCTD: Tests-Guided Proofs for C Programs on LLVM. In M. Chechik, & J-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 927-929). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9636). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_62

Saarikivi, Olli ; Heljanko, Keijo. / LCTD : Tests-Guided Proofs for C Programs on LLVM. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Marsha Chechik ; Jean-Francois Raskin. Vol. 9636 Springer Verlag, 2016. pp. 927-929 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a4877979922d423982afa0277d70cb59,

title = "LCTD: Tests-Guided Proofs for C Programs on LLVM",

abstract = "LCTD is an open source verification tool for C programs. It uses the LLVM compiler framework to instrument programs for verification with the DASH algorithm. LCTD has been submitted to the BitVectorsReach category of SV-COMP 2016.",

author = "Olli Saarikivi and Keijo Heljanko",

note = "Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016; International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ; Conference date: 02-04-2016 Through 08-04-2016",

year = "2016",

doi = "10.1007/978-3-662-49674-9_62",

language = "English",

isbn = "978-3-662-49673-2",

volume = "9636",

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

publisher = "Springer Verlag",

pages = "927--929",

editor = "Marsha Chechik and Jean-Francois Raskin",

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

address = "Germany",

}

Saarikivi, O & Heljanko, K 2016, LCTD: Tests-Guided Proofs for C Programs on LLVM. in M Chechik & J-F Raskin (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 9636, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9636, Springer Verlag, pp. 927-929, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, Netherlands, 02/04/2016. https://doi.org/10.1007/978-3-662-49674-9_62

LCTD : Tests-Guided Proofs for C Programs on LLVM. / Saarikivi, Olli; Heljanko, Keijo.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Marsha Chechik; Jean-Francois Raskin. Vol. 9636 Springer Verlag, 2016. p. 927-929 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9636).

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

TY - GEN

T1 - LCTD

T2 - International Conference on Tools and Algorithms for the Construction and Analysis of Systems

AU - Saarikivi, Olli

AU - Heljanko, Keijo

N1 - Conference code: 22

PY - 2016

Y1 - 2016

N2 - LCTD is an open source verification tool for C programs. It uses the LLVM compiler framework to instrument programs for verification with the DASH algorithm. LCTD has been submitted to the BitVectorsReach category of SV-COMP 2016.

AB - LCTD is an open source verification tool for C programs. It uses the LLVM compiler framework to instrument programs for verification with the DASH algorithm. LCTD has been submitted to the BitVectorsReach category of SV-COMP 2016.

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

U2 - 10.1007/978-3-662-49674-9_62

DO - 10.1007/978-3-662-49674-9_62

M3 - Conference contribution

AN - SCOPUS:84964019040

SN - 978-3-662-49673-2

VL - 9636

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

SP - 927

EP - 929

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

A2 - Chechik, Marsha

A2 - Raskin, Jean-Francois

PB - Springer Verlag

Y2 - 2 April 2016 through 8 April 2016

ER -

Saarikivi O, Heljanko K. LCTD: Tests-Guided Proofs for C Programs on LLVM. In Chechik M, Raskin J-F, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9636. Springer Verlag. 2016. p. 927-929. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-49674-9_62