Generalized arrays for Stainless frames

DOI10.1007/978-3-030-94583-1_17zbMath1498.68172OpenAlexW4206114225MaRDI QIDQ2152661

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

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

Uses Software

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

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Notions of computation and monads
• The existence of refinement mappings
• Automatic verification of Java programs with dynamic frames
• Isabelle/HOL. A proof assistant for higher-order logic
• Model checking algorithms for hyperproperties (invited paper)
• Modular product programs
• Automated mutual induction proof in separation logic
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Model-based Theory Combination
• The Relationship between Separation Logic and Implicit Dynamic Frames
• Dafny: An Automatic Program Verifier for Functional Correctness
• Comprehending monads
• Verification of non-functional programs using interpretations in type theory
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Array Folds Logic
• Induction for SMT Solvers
• Dijkstra monads for free
• Compositional Shape Analysis by Means of Bi-Abduction
• Programming Languages and Systems
• Verification, Model Checking, and Abstract Interpretation