All-path reachability logic

Andrei Ştefǎnescu, Ştefan Ciobâč, Radu Mereuta, Brandon M. Moore, Traian Florin Şerbǎnutǎ, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g. concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language; the soundness has also been mechanized (Coq). This approach is implemented in a tool for semantics-based verification as part of the framework.

Original languageEnglish (US)
Title of host publicationRewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer
Pages425-440
Number of pages16
ISBN (Print)9783319089171
DOIs
StatePublished - 2014
Event25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: Jul 14 2014Jul 17 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8560 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
Country/TerritoryAustria
CityVienna
Period7/14/147/17/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'All-path reachability logic'. Together they form a unique fingerprint.

Cite this