scientific article; zbMATH DE number 2110621
From MaRDI portal
Publication:4823141
zbMath1097.68632MaRDI QIDQ4823141
Publication date: 26 October 2004
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
A Formalization of Properties of Continuous Functions on Closed Intervals ⋮ Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory ⋮ Theory exploration powered by deductive synthesis ⋮ The Imandra Automated Reasoning System (System Description) ⋮ Mining the Archive of Formal Proofs ⋮ Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras ⋮ Parallelized sequential composition and hardware weak memory models ⋮ Second-order properties of undirected graphs ⋮ Relation-algebraic verification of Borůvka's minimum spanning tree algorithm ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Relational characterisations of paths ⋮ Reasoning about actions with loops via Hoare logic ⋮ A program logic for resources ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ Analytic Tableaux for Higher-Order Logic with Choice ⋮ Monotonicity Inference for Higher-Order Formulas ⋮ Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion ⋮ Premise Selection in the Naproche System ⋮ A formal proof of the expressiveness of deep learning ⋮ Fifty years of Hoare's logic ⋮ An algebraic framework for minimum spanning tree problems ⋮ GRUNGE: a grand unified ATP challenge ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ Probabilistic guarded commands mechanized in HOL ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Verifying graph programs with monadic second-order logic
Uses Software
