Generalized arrays for Stainless frames

DOI10.1007/978-3-030-94583-1_17MaRDI QIDQ2152661zbMATH OpenOpenAlexFDO

Authors Georg Stefan Schmid, Viktor Kuncak

Publication date 8 July 2022

Full work available at URL https://doi.org/10.1007/978-3-030-94583-1_17

zbMATH Keywords

verificationsatisfiability modulo theoriesdynamic framesarray theoriesshared mutable data structures

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Generalized metallic structures
• Generalized Riordan arrays
• Structural properties of Costas arrays
• Generalised Complementary Arrays
• scientific article; zbMATH DE number 5369600
• Optimal design of steel frame structures
• scientific article; zbMATH DE number 123902
• Reflective metalogical frameworks
• Tessellation-like rod-joint frameworks

Cites work

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Array Folds Logic
• Automated mutual induction proof in separation logic
• Automatic verification of Java programs with dynamic frames
• Compositional shape analysis by means of bi-abduction
• Comprehending monads
• Dafny: an automatic program verifier for functional correctness
• Dijkstra monads for free
• Induction for SMT solvers
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Model checking algorithms for hyperproperties (invited paper)
• Model-based theory combination
• Modular product programs
• Notions of computation and monads
• Programming Languages and Systems
• The existence of refinement mappings
• The relationship between separation logic and implicit dynamic frames
• Verification of non-functional programs using interpretations in type theory
• Verification, Model Checking, and Abstract Interpretation
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(2)

• Enforcing structural invariants using dynamic frames
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs

Describes a project that uses

Uses Software

• IronFleet
• jStar
• CVC4
• Boogie
• VeriFast
• Scala
• z3
• Isabelle/HOL
• Dafny
• Coq

This page was built for publication: Generalized arrays for Stainless frames

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2152661)