:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Colvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa, Su, Roger C.
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2407.20559
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Reasoning about distributive laws in a concurrent refinement algebra
by: Meinicke, Larissa A., et al.
Published: (2024)

Restructuring a concurrent refinement algebra
by: Hayes, Ian J., et al.
Published: (2024)

Reasoning about expression evaluation under interference
by: Hayes, Ian J., et al.
Published: (2024)

Data reification in a concurrent rely-guarantee algebra
by: Meinicke, Larissa A., et al.
Published: (2024)

Reasoning about concurrent loops and recursion with rely-guarantee rules
by: Hayes, Ian J., et al.
Published: (2025)

Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
by: Tobler, James, et al.
Published: (2026)

Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols
by: Yatapanage, Nisansala P., et al.
Published: (2023)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
by: Lahav, Ori, et al.
Published: (2023)

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning
by: Dardik, Ian, et al.
Published: (2025)

Recomposition: A New Technique for Efficient Compositional Verification
by: Dardik, Ian, et al.
Published: (2024)

Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
by: Jamroga, Wojciech, et al.
Published: (2025)

Practical Deductive Verification of OCaml Programs (Extended Version)
by: Pereira, Mário
Published: (2024)

The Architecture of Truth
by: Kent, Robert E.
Published: (2024)

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA
by: Palmskog, Karl, et al.
Published: (2025)

Canonicity in power and modal logics of finite achronal width
by: Goldblatt, Robert, et al.
Published: (2022)

Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
by: Férée, Hugo, et al.
Published: (2026)

BayesL: a Logical Framework for the Verification of Bayesian Networks
by: Nicoletti, Stefano M., et al.
Published: (2025)

VerifyThis 2019: A Program Verification Competition (Extended Report)
by: Dross, Claire, et al.
Published: (2020)

Uniform interpolation with constructive diamond
by: van der Giessen, Iris, et al.
Published: (2026)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
by: Lyon, Tim S., et al.
Published: (2024)

Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification
by: Singh, Vikash, et al.
Published: (2026)

Verifying Lock-free Search Structure Templates
by: Patel, Nisarg, et al.
Published: (2024)

Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4
by: Zhang, Jianyu, et al.
Published: (2026)

Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
by: de Groot, Jim, et al.
Published: (2026)

Semantical Analysis of Intuitionistic Modal Logics between CK and IK
by: de Groot, Jim, et al.
Published: (2024)

Formal Verification of the Empty Hexagon Number
by: Subercaseaux, Bernardo, et al.
Published: (2024)

Hyperproperty Verification as CHC Satisfiability
by: Itzhaky, Shachar, et al.
Published: (2023)

Craig Interpolation in Program Verification
by: Rümmer, Philipp
Published: (2026)

Tools at the Frontiers of Quantitative Verification
by: Andriushchenko, Roman, et al.
Published: (2024)

Verification of Configurable SRA Systems
by: Cimatti, Alessandro, et al.
Published: (2026)

Revisiting Differential Verification: Equivalence Verification with Confidence
by: Teuber, Samuel, et al.
Published: (2024)

A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
by: Tsai, Wei-Lun, et al.
Published: (2026)

A Note on the Practice of Logical Inferentialism
by: Gheorghiu, Alexander V., et al.
Published: (2024)

On effective constructions of existentially closed groups
by: Scott, I
Published: (2024)

An $\mathrm{NSOP}_{1}$ theory without the existence axiom
by: Mutchnik, Scott
Published: (2024)

Tarski's least fixed point theorem: A predicative type theoretic formulation
by: Ray, Ian
Published: (2024)

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
by: Lindner, Andreas, et al.
Published: (2023)

Runtime Verification of Interactions Using Automata
by: Weil-Kennedy, Chana, et al.
Published: (2025)

Formal Verification of Isothermal Chemical Reactors
by: Feyzishendi, Parivash, et al.
Published: (2025)