scientific article
From MaRDI portal
Publication:2721096
zbMath0963.68036MaRDI QIDQ2721096
Publication date: 1 July 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML, Formal verification of C systems code. Structured types, separation logic and theorem proving, Laws of Programming for References, Blaming the client: on data refinement in the presence of pointers, Inter-process buffers in separation logic with rely-guarantee, On building cyclic and shared structures in Haskell, An algebraic glimpse at bunched implications and separation logic, Doomed program points, Reasoning about memory layouts, Region analysis for deductive verification of C programs, Verification conditions for source-level imperative programs, Lightweight Separation, Analysis of correct synchronization of operating system components, Formal study of functional orbits in finite domains, Reasoning about Assignments in Recursive Data Structures, Verification of the Schorr-Waite Algorithm – From Trees to Graphs, A program logic for resources, Formal verification of a C-like memory model and its uses for verifying program transformations, Verification of finite iterations over collections of variable data structures, Proving pointer programs in higher-order logic, Heaps and Data Structures: A Challenge for Automated Provers, Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs, A Machine-Checked Framework for Relational Separation Logic, Operating system verification---an overview, Verifying Whiley programs with Boogie, Reasoning about Separation Using Abstraction and Reification