A formalisation of consistent consequence for Boolean equation systems

DOI10.1007/978-3-319-66107-0_29zbMath1484.68318OpenAlexW2749282081MaRDI QIDQ1687766

Tim A. C. Willemse, Herman Geuvers, Myrthe van Delft

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_29

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• mCRL2

Cites Work

• Compositional verification of asynchronous concurrent systems using CADP
• A lattice-theoretical fixpoint theorem and its applications
• Consistent Consequence for Boolean Equation Systems
• Introduction to Bisimulation and Coinduction
• Liveness Analysis for Parameterised Boolean Equation Systems
• Consistent Correlations for Parameterised Boolean Equation Systems with Applications in Correctness Proofs for Manipulations
• Abstraction in Fixpoint Logic
• An Overview of the mCRL2 Toolset and Its Recent Advances

This page was built for publication: A formalisation of consistent consequence for Boolean equation systems