The following pages link to (Q4823141):
Displaying 50 items.
- Weakly expressive models for Hoare logic (Q805248) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Refinement concepts formalised in higher order logic (Q916409) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- A language independent proof of the soundness and completeness of generalized Hoare logic (Q1122978) (← links)
- The \(HOL\) logic extended with quantification over type variables (Q1309243) (← links)
- Isabelle/HOL. A proof assistant for higher-order logic (Q1600086) (← links)
- Reasoning about actions with loops via Hoare logic (Q1712544) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← links)
- Hoare's logic and VDM (Q1805402) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Verifying graph programs with monadic second-order logic (Q2117269) (← links)
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
- A formally verified abstract account of Gödel's incompleteness theorems (Q2305432) (← links)
- A program logic for resources (Q2463560) (← links)
- Probabilistic guarded commands mechanized in HOL (Q2576950) (← links)
- Second-order properties of undirected graphs (Q2695354) (← links)
- Relation-algebraic verification of Borůvka's minimum spanning tree algorithm (Q2695356) (← links)
- Formalising general correctness (Q2845516) (← links)
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL (Q2938044) (← links)
- Formalising Knot Theory in Isabelle/HOL (Q2945656) (← links)
- Completeness of Hoare Logic Relative to the Standard Model (Q2971129) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- (Q3024884) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- Hoare logic for Java in Isabelle/HOL (Q4329634) (← links)
- (Q4417837) (← links)
- More Church-Rosser proofs (in Isabelle/HOL) (Q4647561) (← links)
- A Formalization of Properties of Continuous Functions on Closed Intervals (Q5041063) (← links)
- Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory (Q5041273) (← links)
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL (Q5049005) (← links)
- The Imandra Automated Reasoning System (System Description) (Q5049029) (← links)
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras (Q5098718) (← links)
- Automated Deduction – CADE-20 (Q5394605) (← links)
- Theorem Proving in Higher Order Logics (Q5464647) (← links)
- Logic-Free Reasoning in Isabelle/Isar (Q5505517) (← links)
- Theoretical Aspects of Computing - ICTAC 2004 (Q5709983) (← links)
- Automata, Languages and Programming (Q5716757) (← links)
- Analytic Tableaux for Higher-Order Logic with Choice (Q5747752) (← links)
- Monotonicity Inference for Higher-Order Formulas (Q5747753) (← links)
- Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion (Q5747766) (← links)
- Premise Selection in the Naproche System (Q5747782) (← links)
- (Q5875430) (← links)
- A formal proof of the expressiveness of deep learning (Q5915784) (← links)
- Parallelized sequential composition and hardware weak memory models (Q6045051) (← links)
