Proving concurrent constraint programs correct

被引：0
|
作者：
Universiteit Utrecht, Utrecht, Netherlands [1 ]
机构：
来源：
ACM Trans Program Lang Syst | / 5卷 / 685-725期
关键词：
Computational linguistics - Constraint theory - Logic programming - Theorem proving;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
We introduce a simple compositional proof system for proving (partial) correctness of concurrent constraint programs (CCP). The proof system is based on a denotational approximation of the strongest postcondition semantics of CCP programs. The proof system is proved to be correct for full CCP and complete for the class of programs in which the denotational semantics characterizes exactly the strongest postcondition. This class includes the so-called confluent CCP, a special case of which is constraint logic programming with dynamic scheduling.
引用
收藏
相关论文
共 50 条
  • [31] Set-based failure analysis for logic programs and concurrent constraint programs
    Podelski, A
    Charatonik, W
    Müller, M
    PROGRAMMING LANGUAGES AND SYSTEMS, 1999, 1576 : 177 - 192
  • [32] Proving Calculational Proofs Correct
    Walter, Andrew T.
    Kumar, Ankit
    Manolios, Panagiotis
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, 393 : 133 - 150
  • [33] Proving an Execution of an Algorithm Correct?
    Davenport, James Harold
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2023, 2023, 14101 : 255 - 269
  • [34] PROVING SYSTOLIC SYSTEMS CORRECT
    HENNESSY, M
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (03): : 344 - 387
  • [35] CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
    Eilers, Marco
    Dardinier, Thibault
    Mueller, Peter
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (PLDI):
  • [36] Proving security protocols correct
    Paulson, Lawrence C.
    Proceedings - Symposium on Logic in Computer Science, 1999, : 370 - 381
  • [37] A temporal logic for reasoning about timed concurrent constraint programs
    de Boer, FS
    Gabbrielli, M
    Meo, MC
    EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 227 - 233
  • [38] A confluent semantic basis for the analysis of concurrent constraint logic programs
    Codish, M
    Falaschi, M
    Marriott, K
    Winsborough, W
    JOURNAL OF LOGIC PROGRAMMING, 1997, 30 (01): : 53 - 81
  • [39] Timed soft concurrent constraint programs: An interleaved and a parallel approach
    Bistarelli, Stefano
    Gabbrielli, Maurizio
    Meo, Maria Chiara
    Santini, Francesco
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2015, 15 : 743 - 782
  • [40] Verifying and Testing Concurrent Programs using Constraint Solver based Approaches
    Khanna, Dhriti
    Purandare, Rahul
    Sharma, Subodh
    2020 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE AND EVOLUTION (ICSME 2020), 2020, : 834 - 838
12345