A Proof System for MSVL Programs in Coq

DOI10.1007/978-3-319-57708-1_8zbMath1461.68058OpenAlexW2606289262MaRDI QIDQ4989018

Lin Qian, Zhenhua Duan, Nan Zhang, Cong Tian

Publication date: 20 May 2021

Published in: Structured Object-Oriented Formal Language and Method (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-57708-1_8

zbMATH Keywords

CoqMSVLinteractive theorem proversemi-automatic proof

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) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq

This page was built for publication: A Proof System for MSVL Programs in Coq