scientific article; zbMATH DE number 3410595
From MaRDI portal
zbMath0259.68009MaRDI QIDQ5674963
Publication date: 1972
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Unnamed Item, Formal verification of C systems code. Structured types, separation logic and theorem proving, Balancing the load. Leveraging a semantics stack for systems verification, Loop verification with invariants and contracts, Inter-process buffers in separation logic with rely-guarantee, Separation logics and modalities: a survey, Partitioned Memory Models for Program Analysis, An algebraic glimpse at bunched implications and separation logic, Doomed program points, Reasoning about memory layouts, Function extraction, A survey of state vectors, Region analysis for deductive verification of C programs, Verification conditions for source-level imperative programs, Lightweight Separation, Formal study of functional orbits in finite domains, Reasoning about Assignments in Recursive Data Structures, Formal verification of a C-like memory model and its uses for verifying program transformations, Verify heaps via unified model checking, Proving pointer programs in higher-order logic, Algebraic separation logic, Quantitative separation logic and programs with lists, Heaps and Data Structures: A Challenge for Automated Provers, Frame rule for mutually recursive procedures manipulating pointers, The correctness of the Schorr-Waite list marking algorithm, Data types, abstract data types and their specification problem, Verification of Equivalent-Results Methods, Operating system verification---an overview, A Theory of Pointers for the UTP, Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories, Some fundamental algebraic tools for the semantics of computation: II. Signed and abstract theories
