Proving Reachability-Logic Formulas Incrementally

DOI10.1007/978-3-319-44802-2_8zbMath1367.68076OpenAlexW2290990225MaRDI QIDQ2827839

Andrei Arusoaie, Vlad Rusu

Publication date: 21 October 2016

Published in: Rewriting Logic and Its Applications (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01282379/file/paper.pdf

Mathematics Subject Classification ID

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

Related Items (1)

Executing and verifying higher-order functional-imperative programs in Maude

Uses Software

• Why3
• z3
• Maude
• WhyML

Cites Work

• Unnamed Item
• A generic framework for symbolic execution: a coinductive approach
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Matching Logic: An Alternative to Hoare/Floyd Logic
• Towards a Unified Theory of Operational and Axiomatic Semantics
• All-Path Reachability Logic
• One-Path Reachability Logic
• Why3 — Where Programs Meet Provers

This page was built for publication: Proving Reachability-Logic Formulas Incrementally