SPLASH Companion 2022 – Companion Proceedings

Frontmatter

Keynotes

(I Can’t Get No) Verification (Keynote)
Atsushi Igarashi
(Kyoto University, Japan)


@InProceedings{SPLASH Companion22p1, author = {Atsushi Igarashi}, title = {(I Can’t Get No) Verification (Keynote)}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3563768.3570524}, year = {2022}, } Publisher's Version Article: splashcomp22key-key1-p doi:10.1145/3563768.3570524

The State of Debugging in 2022 (Keynote)
Robert O’Callahan
(Google Research, New Zealand)


@InProceedings{SPLASH Companion22p2, author = {Robert O’Callahan}, title = {The State of Debugging in 2022 (Keynote)}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {2-1}, doi = {10.1145/3563768.3570525}, year = {2022}, } Publisher's Version Article: splashcomp22key-key2-p doi:10.1145/3563768.3570525

Myths and Mythconceptions: What Does It Mean to Be a Programming Language, Anyhow? (Keynote)
Mary Shaw
(Carnegie Mellon University, USA)


@InProceedings{SPLASH Companion22p3, author = {Mary Shaw}, title = {Myths and Mythconceptions: What Does It Mean to Be a Programming Language, Anyhow? (Keynote)}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {3-2}, doi = {10.1145/3563768.3570526}, year = {2022}, } Publisher's Version Article: splashcomp22key-key3-p doi:10.1145/3563768.3570526

Improving the Quality of Creative Practices with Pattern Languages (Keynote)
Takashi Iba
(Keio University, Japan)


@InProceedings{SPLASH Companion22p4, author = {Takashi Iba}, title = {Improving the Quality of Creative Practices with Pattern Languages (Keynote)}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {4-3}, doi = {10.1145/3563768.3570527}, year = {2022}, } Publisher's Version Article: splashcomp22key-key4-p doi:10.1145/3563768.3570527

Posters

Provably Correct Smart Contracts: An Approach using DeepSEA
Daniel Britten, Vilhelm Sjöberg, and Steve Reeves
(University of Waikato, New Zealand; CertiK, USA)


@InProceedings{SPLASH Companion22p5, author = {Daniel Britten and Vilhelm Sjöberg and Steve Reeves}, title = {Provably Correct Smart Contracts: An Approach using DeepSEA}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {5-4}, doi = {10.1145/3563768.3564116}, year = {2022}, } Publisher's Version Article: splashcomp22posters-p6-p doi:10.1145/3563768.3564116

Multiverse Notebook: A Notebook Environment for Safe and Efficient Exploration
Tomoki Nakamaru and Shigeyuki Sato
(University of Tokyo, Japan)


@InProceedings{SPLASH Companion22p7, author = {Tomoki Nakamaru and Shigeyuki Sato}, title = {Multiverse Notebook: A Notebook Environment for Safe and Efficient Exploration}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {7-6}, doi = {10.1145/3563768.3564117}, year = {2022}, } Publisher's Version Article: splashcomp22posters-p41-p doi:10.1145/3563768.3564117

Explicit Code Reuse Recommendation
Dov Fraivert and David H. Lorenz
(Open University of Israel, Israel)


@InProceedings{SPLASH Companion22p9, author = {Dov Fraivert and David H. Lorenz}, title = {Explicit Code Reuse Recommendation}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {9-8}, doi = {10.1145/3563768.3564118}, year = {2022}, } Publisher's Version Article: splashcomp22posters-p89-p doi:10.1145/3563768.3564118

Composing Linear Types and Separation Logic Proofs of Memory Safety
Pilar Selene Linares Arévalo
(University of Melbourne, Australia)


@InProceedings{SPLASH Companion22p11, author = {Pilar Selene Linares Arévalo}, title = {Composing Linear Types and Separation Logic Proofs of Memory Safety}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {11-10}, doi = {10.1145/3563768.3564119}, year = {2022}, } Publisher's Version Article: splashcomp22posters-p99-p doi:10.1145/3563768.3564119

Doctoral Symposium

Program Synthesis for Artifacts beyond Programs
Pankaj Kumar Kalita
(IIT Kanpur, India)


@InProceedings{SPLASH Companion22p13, author = {Pankaj Kumar Kalita}, title = {Program Synthesis for Artifacts beyond Programs}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {13-12}, doi = {10.1145/3563768.3565544}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p6-p doi:10.1145/3563768.3565544

Formally Verified Resource Bounds through Implicit Computational Complexity
Neea Rusch
(Augusta University, USA)


@InProceedings{SPLASH Companion22p18, author = {Neea Rusch}, title = {Formally Verified Resource Bounds through Implicit Computational Complexity}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {18-17}, doi = {10.1145/3563768.3565545}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p10-p doi:10.1145/3563768.3565545

Programming Support for Local-First Software: Enabling the Design of Privacy-Preserving Distributed Software without Relying on the Cloud
Julian Haas
(TU Darmstadt, Germany)


@InProceedings{SPLASH Companion22p23, author = {Julian Haas}, title = {Programming Support for Local-First Software: Enabling the Design of Privacy-Preserving Distributed Software without Relying on the Cloud}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {23-22}, doi = {10.1145/3563768.3565546}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p16-p doi:10.1145/3563768.3565546

Proving Obliviousness of Probabilistic Algorithms with Formal Verification
Pengbo Yan
(University of Melbourne, Australia)


@InProceedings{SPLASH Companion22p28, author = {Pengbo Yan}, title = {Proving Obliviousness of Probabilistic Algorithms with Formal Verification}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {28-27}, doi = {10.1145/3563768.3565547}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p17-p doi:10.1145/3563768.3565547

Towards Automated Updates of Software Dependencies
Dhanushka Jayasuriya
(University of Auckland, New Zealand)


@InProceedings{SPLASH Companion22p33, author = {Dhanushka Jayasuriya}, title = {Towards Automated Updates of Software Dependencies}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {33-32}, doi = {10.1145/3563768.3565548}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p27-p doi:10.1145/3563768.3565548

Verification of Hardware and Software with Fuzzing and Proofs
Sujit Kumar Muduli
(IIT Kanpur, India)


@InProceedings{SPLASH Companion22p38, author = {Sujit Kumar Muduli}, title = {Verification of Hardware and Software with Fuzzing and Proofs}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {38-37}, doi = {10.1145/3563768.3565549}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p38-p doi:10.1145/3563768.3565549

Grammar Inference for Ad Hoc Parsers
Michael Schröder
(TU Wien, Austria)


@InProceedings{SPLASH Companion22p43, author = {Michael Schröder}, title = {Grammar Inference for Ad Hoc Parsers}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {43-42}, doi = {10.1145/3563768.3565550}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p41-p doi:10.1145/3563768.3565550

Verification of Programs with Concealed Components
Sumit Lahiri
(IIT Kanpur, India)


@InProceedings{SPLASH Companion22p48, author = {Sumit Lahiri}, title = {Verification of Programs with Concealed Components}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {48-47}, doi = {10.1145/3563768.3565551}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p79-p doi:10.1145/3563768.3565551

Towards a Verified Cost Model for Call-by-Push-Value
Zhuo Chen
(University of Melbourne, Australia)


@InProceedings{SPLASH Companion22p53, author = {Zhuo Chen}, title = {Towards a Verified Cost Model for Call-by-Push-Value}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {53-52}, doi = {10.1145/3563768.3565552}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p81-p doi:10.1145/3563768.3565552

Modelling the Quantification of Technical Debt
Judith Perera
(University of Auckland, New Zealand)


@InProceedings{SPLASH Companion22p58, author = {Judith Perera}, title = {Modelling the Quantification of Technical Debt}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {58-57}, doi = {10.1145/3563768.3565553}, year = {2022}, } Publisher's Version Article: splashcomp22doc-p94-p doi:10.1145/3563768.3565553

Student Research Competition

Graduate Papers

Simple Extensible Programming through Precisely-Typed Open Recursion
Andong Fan
(Hong Kong University of Science and Technology, China)


@InProceedings{SPLASH Companion22p63, author = {Andong Fan}, title = {Simple Extensible Programming through Precisely-Typed Open Recursion}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {63-62}, doi = {10.1145/3563768.3563951}, year = {2022}, } Publisher's Version Article: splashcomp22src-id2978-p doi:10.1145/3563768.3563951

LoRe: Local-First Reactive Programming with Verified Safety Guarantees
Julian Haas
(TU Darmstadt, Germany)


@InProceedings{SPLASH Companion22p67, author = {Julian Haas}, title = {LoRe: Local-First Reactive Programming with Verified Safety Guarantees}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {67-66}, doi = {10.1145/3563768.3563952}, year = {2022}, } Publisher's Version Article: splashcomp22src-id1133-p doi:10.1145/3563768.3563952

Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm
Yahui Song and Wei-Ngan Chin
(National University of Singapore, Singapore)


@InProceedings{SPLASH Companion22p71, author = {Yahui Song and Wei-Ngan Chin}, title = {Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {71-70}, doi = {10.1145/3563768.3563953}, year = {2022}, } Publisher's Version Article: splashcomp22src-id9583-p doi:10.1145/3563768.3563953

CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis
Chengpeng Wang
(Hong Kong University of Science and Technology, China)


@InProceedings{SPLASH Companion22p75, author = {Chengpeng Wang}, title = {CodeSpider: Automatic Code Querying with Multi-modal Conjunctive Query Synthesis}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {75-74}, doi = {10.1145/3563768.3563954}, year = {2022}, } Publisher's Version Article: splashcomp22src-id1832-p doi:10.1145/3563768.3563954

ARENA: Enhancing Abstract Refinement for Neural Network Verification
Yuyi Zhong, Quang-Trung Ta, and Siau-Cheng Khoo
(National University of Singapore, Singapore)


@InProceedings{SPLASH Companion22p79, author = {Yuyi Zhong and Quang-Trung Ta and Siau-Cheng Khoo}, title = {ARENA: Enhancing Abstract Refinement for Neural Network Verification}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {79-78}, doi = {10.1145/3563768.3563955}, year = {2022}, } Publisher's Version Article: splashcomp22src-id6999-p doi:10.1145/3563768.3563955

Foundationally Sound Annotation Verifier via Control Flow Splitting
Litao Zhou
(Shanghai Jiao Tong University, China)


@InProceedings{SPLASH Companion22p83, author = {Litao Zhou}, title = {Foundationally Sound Annotation Verifier via Control Flow Splitting}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {83-82}, doi = {10.1145/3563768.3563956}, year = {2022}, } Publisher's Version Article: splashcomp22src-id9734-p doi:10.1145/3563768.3563956

A Study of the Impact of Callbacks in Staged Static+Dynamic Partial Analysis
Aditya Anand
(IIT Mandi, India)


@InProceedings{SPLASH Companion22p87, author = {Aditya Anand}, title = {A Study of the Impact of Callbacks in Staged Static+Dynamic Partial Analysis}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {87-86}, doi = {10.1145/3563768.3563957}, year = {2022}, } Publisher's Version Article: splashcomp22src-id9908-p doi:10.1145/3563768.3563957

Undergraduate Papers

Termination of Recursive Functions by Lexicographic Orders of Linear Combinations
Raphael Douglas Giles
(UNSW, Australia)


@InProceedings{SPLASH Companion22p91, author = {Raphael Douglas Giles}, title = {Termination of Recursive Functions by Lexicographic Orders of Linear Combinations}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {91-90}, doi = {10.1145/3563768.3563958}, year = {2022}, } Publisher's Version Article: splashcomp22src-id2437-p doi:10.1145/3563768.3563958

Qiwi: A Beginner Friendly Quantum Language
Abhinandan Pal and Anubhab Ghosh
(IIIT Kalyani, India)


@InProceedings{SPLASH Companion22p95, author = {Abhinandan Pal and Anubhab Ghosh}, title = {Qiwi: A Beginner Friendly Quantum Language}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {95-94}, doi = {10.1145/3563768.3563959}, year = {2022}, } Publisher's Version Article: splashcomp22src-id3394-p doi:10.1145/3563768.3563959

Using Mutations to Analyze Formal Specifications
Siraphob Phipathananunth
(Vanderbilt University, USA)


@InProceedings{SPLASH Companion22p99, author = {Siraphob Phipathananunth}, title = {Using Mutations to Analyze Formal Specifications}, booktitle = {Proc.\ SPLASH Companion}, publisher = {ACM}, pages = {99-98}, doi = {10.1145/3563768.3563960}, year = {2022}, } Publisher's Version Article: splashcomp22src-id7593-p doi:10.1145/3563768.3563960

proc time: 0.12