Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

被引：8

作者：

Batz, Kevin ^{[1
]}

Chen, Mingshuai ^{[2
]}

Junges, Sebastian ^{[3
]}

Kaminski, Benjamin Lucien ^{[4
,5
]}

Katoen, Joost-Pieter ^{[1
]}

Matheja, Christoph ^{[6
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

[2] Zhejiang Univ, Hangzhou, Peoples R China

[3] Radboud Univ Nijmegen, Nijmegen, Netherlands

[4] Saarland Univ, Saarbrucken, Germany

[5] UCL, London, England

[6] Tech Univ Denmark, Lyngby, Denmark

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023 | 2023年 / 13994卷

关键词：

SYMBOLIC MODEL CHECKING; GENERATION;

D O I：

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

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：410 / 429

页数：20

共 50 条

[1] Inductive Verification of Data Model Invariants for Web Applications
Bocic, Ivan
Bultan, Tevfik
36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2014), 2014, : 620 - 631
[2] INDUCTIVE LEARNING APPLIED TO PROGRAM CONSTRUCTION AND VERIFICATION
BRATKO, I
GROBELNIK, M
KNOWLEDGE ORIENTED SOFTWARE DESIGN, 1993, 27 : 169 - 182
[3] Verification of Program Transformations with Inductive Refinement Types
Al-Sibahi, Ahmad Salim
Jensen, Thomas P.
Dimovski, Aleksandar S.
Wasowski, Andrzej
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2021, 30 (01)
[4] MAPPINGS AND INDUCTIVE INVARIANTS
JUNG, CFK
COLLOQUIUM MATHEMATICUM, 1973, 28 (01) : 29 - 31
[5] Proof-Carrying Hardware via Inductive Invariants
Isenberg, Tobias
Platzner, Marco
Wehrheim, Heike
Wiersema, Tobias
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2017, 22 (04)
[6] Formal verification of Pentium®4 components with symbolic simulation and inductive invariants
Kaivola, R
COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 170 - 184
[7] PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs
Andriushchenko, Roman
Ceska, Milan
Junges, Sebastian
Katoen, Joost-Pieter
Stupinsky, Simon
COMPUTER AIDED VERIFICATION (CAV 2021), PT I, 2021, 12759 : 856 - 869
[8] NuITP: An Inductive Theorem Prover for Equational Program Verification
Duran, Francisco
Escobar, Santiago
Meseguer, Jose
Sapina, Julia
26TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, PPDP 2024, 2024,
[9] AN INDUCTIVE PROGRAM SYNTHESIS SYSTEM - NDIPS
XU, JF
DAI, M
WANG, ZJ
UNIVERSITY COMPUTING, 1990, 12 (03): : 92 - 97
[10] Knowledge Refactoring for Inductive Program Synthesis
Dumancic, Sebastijan
Guns, Tias
Cropper, Andrew
THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 7271 - 7278

← 1 2 3 4 5 →