Automating Soundness Proofs

DOI10.1016/j.entcs.2009.07.076zbMath1339.68160OpenAlexW2008256913MaRDI QIDQ2810691

Muck J. Van Weerdenburg

Publication date: 3 June 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.076

zbMATH Keywords

theorem provingstructural operational semanticssoundnessaxiomatisation

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Proving the validity of equations in GSOS languages using rule-matching bisimilarity

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• PVS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Structured operational semantics and bisimulation as a congruence
• Isabelle. A generic theorem prover
• Finite axiom systems for testing preorder and De Simone process languages
• Isabelle/HOL. A proof assistant for higher-order logic
• Untersuchungen über das logische Schliessen. I
• The origins of structural operational semantics
• Process Algebra
• The meaning of negative premises in transition system specifications
• Using a generalisation critic to find bisimulations for coinductive proofs
• Foundations of Software Science and Computational Structures

This page was built for publication: Automating Soundness Proofs