Abstract contract synthesis and verification in the symbolic K framework

DOI10.3233/FI-2020-1989MaRDI QIDQ4988925zbMATH OpenOpenAlexFDO

Authors D. Pardo, A. Villanueva, María Alpuente

Publication date 20 May 2021

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2020-1989

zbMATH Keywords

abstract subsumptioncontract inferencedeductive verificationsymbolic execution

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic abstract contract synthesis in a rewriting framework
• Higher order symbolic execution for contract verification and refutation
• Proofs-as-imperative-programs: application to synthesis of contracts
• Modular inference of subprogram contracts for safety checking
• Maximal specification synthesis

Cites work

• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An approach to object semantics based on terminal co-algebras
• An overview of the K semantic framework
• Bottom-Up Shape Analysis
• From rewriting logic, to programming language semantics, to program verification
• scientific article; zbMATH DE number 4050933 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• Modular inference of subprogram contracts for safety checking
• One-path reachability logic
• Quick specifications for the busy programmer
• Shape Analysis for Composite Data Structures
• Symbolic abstract contract synthesis in a rewriting framework
• Symbolic execution and program testing
• Symbolic execution based on language transformation
• The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages
• The Daikon system for dynamic detection of likely invariants
• Verification, Model Checking, and Abstract Interpretation

Cited in

(4)

• Symbolic abstract contract synthesis in a rewriting framework
• Higher order symbolic execution for contract verification and refutation
• KERNELC
• An active learning approach to synthesizing program contracts

Describes a project that uses

Uses Software

• KindSpec
• ACSL
• Maude
• z3

This page was built for publication: Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4988925)