Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

Kevin Batz; Mingshuai Chen; Sebastian Junges; Benjamin Lucien Kaminski; Joost Pieter Katoen; Christoph Matheja

doi:10.1007/978-3-031-30820-8_25

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

Kevin Batz
, Mingshuai Chen
, Sebastian Junges
, Benjamin Lucien Kaminski
, Joost Pieter Katoen
, Christoph Matheja

RWTH Aachen University
Zhejiang University
Radboud University Nijmegen
Saarland University

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

235 Downloads (Orbit)

Abstract

Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.

Original language	English
Title of host publication	Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Volume	13994
Publisher	Springer
Publication date	2023
Pages	410-429
ISBN (Print)	978-3-031-30819-2
ISBN (Electronic)	978-3-031-30820-8
DOIs	https://doi.org/10.1007/978-3-031-30820-8_25
Publication status	Published - 2023
Event	29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023

Conference

Conference	29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Country/Territory	France
City	Paris
Period	22/04/2023 → 27/04/2023

Access to Document

10.1007/978-3-031-30820-8_25Licence: CC BY

FulltextFinal published version, 1.04 MBLicence: CC BY

OpenUrl availability

Check availability in DTU Findit

Cite this

Batz, K., Chen, M., Junges, S., Kaminski, B. L., Katoen, J. P., & Matheja, C. (2023). Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 410-429). Springer. https://doi.org/10.1007/978-3-031-30820-8_25

@inproceedings{12fadc93f6b64a4f81d64c7b44a30618,

title = "Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants",

abstract = "Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.",

author = "Kevin Batz and Mingshuai Chen and Sebastian Junges and Kaminski, \{Benjamin Lucien\} and Katoen, \{Joost Pieter\} and Christoph Matheja",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s).; 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ; Conference date: 22-04-2023 Through 27-04-2023",

year = "2023",

doi = "10.1007/978-3-031-30820-8\_25",

language = "English",

isbn = " 978-3-031-30819-2",

volume = "13994",

pages = "410--429",

booktitle = "Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",

publisher = "Springer",

}

Batz, K, Chen, M, Junges, S, Kaminski, BL, Katoen, JP & Matheja, C 2023, Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. in Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. vol. 13994, Springer, pp. 410-429, 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 22/04/2023. https://doi.org/10.1007/978-3-031-30820-8_25

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. / Batz, Kevin; Chen, Mingshuai; Junges, Sebastian et al.
Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol. 13994 Springer, 2023. p. 410-429.

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

TY - GEN

T1 - Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

AU - Batz, Kevin

AU - Chen, Mingshuai

AU - Junges, Sebastian

AU - Kaminski, Benjamin Lucien

AU - Katoen, Joost Pieter

AU - Matheja, Christoph

PY - 2023

Y1 - 2023

N2 - Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.

AB - Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.

U2 - 10.1007/978-3-031-30820-8_25

DO - 10.1007/978-3-031-30820-8_25

M3 - Article in proceedings

AN - SCOPUS:85161388834

SN - 978-3-031-30819-2

VL - 13994

SP - 410

EP - 429

BT - Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer

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

Y2 - 22 April 2023 through 27 April 2023

ER -

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this