Towards a Unified Theory of Operational and Axiomatic Semantics

DOI10.1007/978-3-642-31585-5_33zbMath1367.68075OpenAlexW1605391443MaRDI QIDQ3167025

Andrei Ştefănescu, Grigore Roşu

Publication date: 1 November 2012

Published in: Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-31585-5_33

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Executing and verifying higher-order functional-imperative programs in Maude ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ The rewriting logic semantics project: a progress report ⋮ A language-independent proof system for full program equivalence ⋮ All-Path Reachability Logic ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model ⋮ Proving Reachability-Logic Formulas Incrementally

Uses Software

• ACL2
• CASL
• z3
• CIRC
• Maude
• Toolchain
• PLT Redex
• K Prover
• Java+ITP

This page was built for publication: Towards a Unified Theory of Operational and Axiomatic Semantics