Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)

David Young; Ziyi Yang; Ilya Sergey; Alex Potanin

doi:10.4230/DARTS.10.2.25

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)

David Young, Ziyi Yang, Ilya Sergey, Alex Potanin

School of Computing

Research output: Contribution to journal › Short survey › peer-review

Abstract

This artifact provides a translator from Pika code to SuSLik specifications. Additionally, it contains a test suite and benchmark suite. These suites are fully automated using provided scripts. All source code is included.

Original language	English
Pages (from-to)	25:1-25:2
Journal	Dagstuhl Artifacts Series (DARTS)
Volume	10
Issue number	2
DOIs	https://doi.org/10.4230/DARTS.10.2.25
Publication status	Published - 2024

Access to Document

10.4230/DARTS.10.2.25

https://dblp.org/db/journals/darts/darts10.html#YoungYSP24

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers
Young, D., Yang, Z., Sergey, I. & Potanin, A., 12 Sept 2024, 38th European Conference on Object-Oriented Programming, ECOOP 2024. Aldrich, J. & Salvaneschi, G. (eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 26 p. 45. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 313).
Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

Open Access

Cite this

@article{d8de4a1046fb46368bb4cda301a67eeb,

title = "Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)",

abstract = "This artifact provides a translator from Pika code to SuSLik specifications. Additionally, it contains a test suite and benchmark suite. These suites are fully automated using provided scripts. All source code is included.",

author = "David Young and Ziyi Yang and Ilya Sergey and Alex Potanin",

note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2024",

doi = "10.4230/DARTS.10.2.25",

language = "English",

volume = "10",

pages = "25:1--25:2",

journal = "Dagstuhl Artifacts Series (DARTS)",

publisher = "Schloss Dagstuhl – Leibniz-Zentrum f{\"u}r Informatik",

number = "2",

}

TY - JOUR

T1 - Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)

AU - Young, David

AU - Yang, Ziyi

AU - Sergey, Ilya

AU - Potanin, Alex

N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2024

Y1 - 2024

N2 - This artifact provides a translator from Pika code to SuSLik specifications. Additionally, it contains a test suite and benchmark suite. These suites are fully automated using provided scripts. All source code is included.

AB - This artifact provides a translator from Pika code to SuSLik specifications. Additionally, it contains a test suite and benchmark suite. These suites are fully automated using provided scripts. All source code is included.

U2 - 10.4230/DARTS.10.2.25

DO - 10.4230/DARTS.10.2.25

M3 - Short survey

VL - 10

SP - 25:1-25:2

JO - Dagstuhl Artifacts Series (DARTS)

JF - Dagstuhl Artifacts Series (DARTS)

IS - 2

ER -

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)

Abstract

Access to Document

Fingerprint

Research output

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers

Cite this