Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

DOI10.3233/FI-2020-1989zbMath1497.68106OpenAlexW3111118845MaRDI QIDQ4988925

Daniel Pardo, Alicia 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

symbolic executiondeductive verificationabstract subsumptioncontract inference

Mathematics Subject Classification ID

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

Related Items (1)

KERNELC

Uses Software

• ACSL
• z3
• Maude
• KindSpec

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modular inference of subprogram contracts for safety checking
• An overview of the K semantic framework
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Symbolic execution based on language transformation
• Symbolic abstract contract synthesis in a rewriting framework
• The Daikon system for dynamic detection of likely invariants
• From Rewriting Logic, to Programming Language Semantics, to Program Verification
• Bottom-Up Shape Analysis
• Symbolic execution and program testing
• An approach to object semantics based on terminal co-algebras
• All-Path Reachability Logic
• One-Path Reachability Logic
• Quick specifications for the busy programmer
• The additional difficulties for the automatic synthesis of specifications posed by logic features in functional-logic languages
• Shape Analysis for Composite Data Structures
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework