Automated Verification of Relational While-Programs

被引：0
|
作者：
Berghammer, Rudolf [1 ]
Hoefner, Peter [2 ,3 ]
Stucke, Insa [1 ]
机构：
[1] Christian Albrechts Univ Kiel, Inst Informat, Kiel, Germany
[2] NICTA, Sydney, NSW, Australia
[3] Univ New South Wales, Comp Sci & Engn, Sydney, NSW, Australia
来源：
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2014) | 2014年 / 8428卷
基金：
澳大利亚研究理事会;
关键词：
SYSTEM DESCRIPTION; CALCULUS; PROOFS;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Software verification is essential for safety-critical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relation-based discrete structures by combining relation algebra and the well-known assertion-based verification method with automated theorem proving. We present two examples in detail: a relational program for determining the reflexive-transitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of common-logical and relation-algebraic specifications.
引用
收藏
页码：173 / 190
页数：18
相关论文
共 11 条
  • [1] Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
    Mulder, Ike
    Krebbers, Robbert
    Geuvers, Herman
    PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22), 2022, : 809 - 824
  • [2] Probabilistic Relational Verification for Cryptographic Implementations
    Barthe, Gilles
    Fournet, Cedric
    Gregoire, Benjamin
    Strub, Pierre-Yves
    Swamy, Nikhil
    Zanella-Beguelin, Santiago
    ACM SIGPLAN NOTICES, 2014, 49 (01) : 193 - 205
  • [3] On Automated Program Construction and Verification
    Berghammer, Rudolf
    Struth, Georg
    MATHEMATICS OF PROGRAM CONSTRUCTION, PROCEEDINGS, 2010, 6120 : 22 - +
  • [4] Automated Verification of Fundamental Algebraic Laws
    Zakhour, George
    Weisenburger, Pascal
    Salvaneschi, Guido
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (PLDI):
  • [5] Tool-Based Verification of a Relational Vertex Coloring Program
    Berghammer, Rudolf
    Hoefner, Peter
    Stucke, Insa
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2015), 2015, 9348 : 275 - 292
  • [6] Automated Verification of Equivalence Properties of Cryptographic Protocols
    Chadha, Rohit
    Cheval, Vincent
    Ciobaca, Stefan
    Kremer, Steve
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2016, 17 (04)
  • [7] Automated Verification of Equivalence Properties of Cryptographic Protocols
    Chadha, Rohit
    Ciobaca, Stefan
    Kremer, Steve
    PROGRAMMING LANGUAGES AND SYSTEMS, 2012, 7211 : 108 - 127
  • [8] Automated and Modular Refinement Reasoning for Concurrent Programs
    Hawblitzel, Chris
    Petrank, Erez
    Qadeer, Shaz
    Tasiran, Serdar
    COMPUTER AIDED VERIFICATION, CAV 2015, PT II, 2015, 9207 : 449 - 465
  • [9] Automated Symbolic Verification of Telegram's MTProto 2.0
    Miculan, Marino
    Vitacolonna, Nicola
    SECRYPT 2021: PROCEEDINGS OF THE 18TH INTERNATIONAL CONFERENCE ON SECURITY AND CRYPTOGRAPHY, 2021, : 185 - 197
  • [10] Formal analysis and verification of security for automated trust negotiation
    Liu, Xin-Xin
    Tang, Shao-Hua
    Huanan Ligong Daxue Xuebao/Journal of South China University of Technology (Natural Science), 2013, 41 (01): : 77 - 82+94
12