Search

• < Previous
• 1
• Next >

---

All-Path Reachability Logic

Andrei Stefanescu ; Stefan Ciobaca ; Radu Mereuta ; Brandon Moore ; Traian Florin Serbanuta ; Grigore Rosu.

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&nbsp;[&hellip;]

---

Matching Logic

Grigore Rosu.

This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function&nbsp;[&hellip;]

---