Ivy

swMATH10279MaRDI QIDQ22242FDOQ22242

Author name not available (Why is that?)

Official website: http://link.springer.com/chapter/10.1007/978-1-4757-3188-0_16

Cited In (67)

• Automated Reasoning
• IronFleet
• 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
• Title not available (Why is that?)
• ATP Cross-Verification of the Mizar MPTP Challenge Problems
• Translation of resolution proofs into short first-order proofs without choice axioms.
• Title not available (Why is that?)
• Integrating external deduction tools with ACL2
• Title not available (Why is that?)
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• CERES
• TRX
• Milawa
• TLAPS
• TLC
• Gandalf
• SystemOnTPTP
• MODIST
• Cubicle
• VeriCon
• PSync
• Automated proof construction in type theory using resolution
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• OMEGA
• HOL90
• ByMC
• ProofTool
• Chapar
• DynamoDB
• Verdi
• FastTrack
• GeoNames
• FLOTTER
• Translation of resolution proofs into short first-order proofs without choice axioms
• Temporal prophecy for proving temporal properties of infinite-state systems
• Pollack-inconsistency
• Computer solutions of problems in inverse semigroups.
• Formal proofs about rewriting using ACL2
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Learning inductive invariants by sampling from frequency distributions
• Extending Sledgehammer with SMT solvers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Minha
• Title not available (Why is that?)
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Title not available (Why is that?)
• More SPASS with Isabelle
• Ivy
• PRocH: proof reconstruction for HOL Light
• Hammering towards QED
• SGGS decision procedures
• Title not available (Why is that?)
• Towards Self-verification of HOL Light
• Koala
• dBug
• DCatch
• Title not available (Why is that?)

This page was built for software: Ivy