Search

• < Previous
• 1
• Next >

---

History-Register Automata

Radu Grigore ; Nikos Tzevelekos.

Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous&nbsp;[&hellip;]

---

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;]

---