Ivy
From MaRDI portal
Cited in
(71)- Towards Self-verification of HOL Light
- Automated Reasoning
- Sound verification procedures for temporal properties of infinite-state systems
- Understanding Resolution Proofs through Herbrand’s Theorem
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Synchronizing the asynchronous
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Using the TPTP Language for Writing Derivations and Finite Interpretations
- A decidable and expressive fragment of many-sorted first-order linear temporal logic
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- Bounded quantifier instantiation for checking inductive invariants
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Integrating external deduction tools with ACL2
- Translation of resolution proofs into short first-order proofs without choice axioms.
- scientific article; zbMATH DE number 2079834 (Why is no real title available?)
- scientific article; zbMATH DE number 1614692 (Why is no real title available?)
- ACL2
- RegStab
- AutoBayes/CC
- RESTART
- CERES
- TRX
- Milawa
- TLAPS
- TLC
- Gandalf
- SystemOnTPTP
- MODIST
- Cubicle
- VeriCon
- PSync
- OMEGA
- HOL90
- ByMC
- ProofTool
- Chapar
- DynamoDB
- Verdi
- FastTrack
- GeoNames
- FLOTTER
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Automated proof construction in type theory using resolution
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Translation of resolution proofs into short first-order proofs without choice axioms
- Ivy
- dBug
- DCatch
- Koala
- IronFleet
- Temporal prophecy for proving temporal properties of infinite-state systems
- Formal proofs about rewriting using ACL2
- Computer solutions of problems in inverse semigroups.
- Pollack-inconsistency
- Learning inductive invariants by sampling from frequency distributions
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Minha
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- scientific article; zbMATH DE number 1796151 (Why is no real title available?)
- scientific article; zbMATH DE number 2079835 (Why is no real title available?)
- More SPASS with Isabelle
- PRocH: proof reconstruction for HOL Light
- Hammering towards QED
- SGGS decision procedures
- scientific article; zbMATH DE number 7533356 (Why is no real title available?)
- scientific article; zbMATH DE number 1948188 (Why is no real title available?)
This page was built for software: Ivy
