From bounded checking to verification of equivalence via symbolic up-to techniques

DOI10.1007/978-3-030-99527-0_10MaRDI QIDQ6535615zbMATH OpenFDO

Authors Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-99527-0_10

zbMATH Keywords

bounded model checkingcontextual equivalenceoperational game semanticssymbolic bisimulationup-to techniques

Mathematics Subject Classification ID

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

Recommendations

• A bounded model checking technique for higher-order programs
• Program equivalence in a simple language with state
• Bisimulation verification using the up to techniques
• Equivalence checking 40 years after: a review of bisimulation tools
• Model checking higher-order programs

Cites work

• A complete normal-form bisimilarity for state
• A contextual equivalence checker for IMJ*
• A Fully Abstract Trace Semantics for General References
• Algorithmic nominal game semantics
• Coinduction All the Way Up
• Enhancements of the bisimulation proof method
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• Incremental bounded model checking for embedded software
• Inference rules for proving the equivalence of recursive procedures
• Kripke open bisimulation. A marriage of game semantics and operational techniques
• Logical Bisimulations and Functional Languages
• Program verification using symbolic game semantics
• Relational Reasoning for Recursive Types and References
• Small bisimulations for reasoning about higher-order imperative programs
• State-dependent representation independence
• The marriage of bisimulations and Kripke logical relations
• Tools and Algorithms for the Construction and Analysis of Systems
• Typed Normal Form Bisimulation

Cited in

(3)

• A bounded model checking technique for higher-order programs
• Fully abstract normal form bisimulation for call-by-value PCF
• Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence

This page was built for publication: From bounded checking to verification of equivalence via symbolic up-to techniques

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