Verifying reachability invariants of linked structures | Zendy

Greg Nelson | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Verifying reachability invariants of linked structures

Author(s) -

Greg Nelson

Publication year - 1983

Publication title -

citeseer x (the pennsylvania state university)

Language(s) - English

Resource type - Conference proceedings

ISBN - 0-89791-090-7

DOI - 10.1145/567067.567073

Subject(s) - reachability , predicate abstraction , predicate (mathematical logic) , correctness , computer science , axiom , programming language , proof theory , automated theorem proving , theoretical computer science , predicate transformer semantics , algorithm , mathematics , model checking , mathematical proof , semantics (computer science) , operational semantics , geometry

The paper introduces a reachability predicate for linear lists, develops the elementary axiomatic theory of the predicate, and illustrates its appiicadon to program verification wKh a formal proof of correctness for a short program that traverses and splices linear lists.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research