kth.sePublikationer KTH
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
ROOSTERIZE: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning
Univ Texas Austin, Austin, TX 78712 USA..
KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.ORCID-id: 0000-0003-0228-1240
Univ Texas Austin, Austin, TX 78712 USA..
Univ Texas Austin, Austin, TX 78712 USA..
2021 (Engelska)Ingår i: 2021 IEEE/ACM 43RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021, s. 21-24Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

Naming conventions are an important concern in large verification projects using proof assistants, such as Coq. In particular, lemma names are used by proof engineers to effectively understand and modify Coq code. However, providing accurate and informative lemma names is a complex task, which is currently often carried out manually. Even when lemma naming is automated using rule-based tools, generated names may fail to adhere to important conventions not specified explicitly. We demonstrate a toolchain, dubbed ROOSTERIZE, which automatically suggests lemma names in Coq projects. ROOSTERIZE leverages a neural network model trained on existing Coq code, thus avoiding manual specification of naming conventions. To allow proof engineers to conveniently access suggestions from ROOSTERIZE during Coq project development, we integrated the toolchain into the popular Visual Studio Code editor. Our evaluation shows that ROOSTERIZE substantially outperforms strong baselines for suggesting lemma names and is useful in practice. The demo video for ROOSTERIZE can be viewed at: https://youtu.be/HZ5ac7Q14rc.

Ort, förlag, år, upplaga, sidor
Institute of Electrical and Electronics Engineers (IEEE) , 2021. s. 21-24
Serie
Proceedings of the IEEE-ACM International Conference on Software Engineering Companion, ISSN 2574-1926
Nyckelord [en]
Coq, lemma names, neural networks
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:kth:diva-304562DOI: 10.1109/ICSE-Companion52605.2021.00026ISI: 000706450400006Scopus ID: 2-s2.0-85115700795OAI: oai:DiVA.org:kth-304562DiVA, id: diva2:1609396
Konferens
IEEE/ACM 43rd International Conference on Software Engineering (ICSE), MAY 25-28, 2021, ELECTR NETWORK
Anmärkning

Part of proceedings: ISBN 978-1-6654-1219-3, QC 20230117

Tillgänglig från: 2021-11-08 Skapad: 2021-11-08 Senast uppdaterad: 2023-01-17Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Person

Palmskog, Karl

Sök vidare i DiVA

Av författaren/redaktören
Palmskog, Karl
Av organisationen
Teoretisk datalogi, TCS
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 68 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf