Proving reachability-logic formulas incrementally

DOI10.1007/978-3-319-44802-2_8MaRDI QIDQ2827839zbMATH OpenOpenAlexFDO

Authors Vlad Rusu, Andrei Arusoaie

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

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

Recommendations

• One-path reachability logic
• A constructor-based reachability logic for rewrite theories
• Reachability logic: an efficient fragment of transitive closure logic

Cites work

• 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.
• Concurrency verification. Introduction to compositional and noncompositional methods
• Matching logic: an alternative to Hoare/Floyd logic
• One-path reachability logic
• Towards a unified theory of operational and axiomatic semantics
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Why3 -- where programs meet provers

Cited in

(7)

• One-path reachability logic
• From hoare logic to matching logic reachability
• Reachability logic: an efficient fragment of transitive closure logic
• Program logics and their applications
• Executing and verifying higher-order functional-imperative programs in Maude
• Low-level reachability analysis based on formal logic
• Unification in matching logic

Describes a project that uses

Uses Software

• WhyML
• Maude
• z3
• Why3

This page was built for publication: Proving reachability-logic formulas incrementally

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