The following pages link to PVS (Q16016):
Displaying 50 items.
- Computer arithmetic: Logic, calculation, and rewriting (Q2782482) (← links)
- Toward sharing libraries of mathematics between theorem provers (Q2782486) (← links)
- On Logic Embeddings and Gödel’s God (Q2787333) (← links)
- Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection (Q2797866) (← links)
- A Classical Realizability Model for a Semantical Value Restriction (Q2802494) (← links)
- Automating soundness proofs (Q2810691) (← links)
- Automated theorem proving for special functions: the next phase (Q2819703) (← links)
- LotrecScheme (Q2825417) (← links)
- Tests and Proofs for Enumerative Combinatorics (Q2827441) (← links)
- Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification (Q2827442) (← links)
- Formalized Timed Automata (Q2829277) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- Mechanical software verification: high level control aspects from a user's perspective (Q2841237) (← links)
- Greatest bisimulations for binary methods (Q2842564) (← links)
- Bounded model checking for timed automata (Q2842869) (← links)
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory (Q2843015) (← links)
- PVS strategies for proving abstraction properties of automata (Q2848044) (← links)
- MetiTarski’s Menagerie of Cooperating Systems (Q2849476) (← links)
- Formalizing Cut Elimination of Coalgebraic Logics in Coq (Q2851950) (← links)
- Interactions between PVS and Maple in symbolic analysis of control systems (Q2852044) (← links)
- Linking semantic models to support \(\mathrm{CSP} \parallel \mathrm{B}\) consistency checking (Q2863864) (← links)
- PVS\#: streamlined tacticals for PVS (Q2864359) (← links)
- Programmed strategies for program verification (Q2864527) (← links)
- A framework for establishing formal conformance between object models and object-oriented programs (Q2873618) (← links)
- Truly Modular (Co)datatypes for Isabelle/HOL (Q2879246) (← links)
- Recursive Functions on Lazy Lists via Domains and Topologies (Q2879262) (← links)
- A synthesis of the procedural and declarative styles of interactive theorem proving (Q2881098) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- A Proof Assistant for Alloy Specifications (Q2894289) (← links)
- Extending MKM Formats at the Statement Level (Q2907314) (← links)
- A Framework for Formally Verifying Software Transactional Memory Algorithms (Q2912700) (← links)
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem (Q2914757) (← links)
- Model Checking under Fairness in ProB and Its Application to Fair Exchange Protocols (Q2915106) (← links)
- An Axiomatization for Cylinder Computation Model (Q2920446) (← links)
- SMT-Based Bisimulation Minimisation of Markov Models (Q2926637) (← links)
- Rewriting Modulo SMT and Open System Analysis (Q2945139) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- Affine Arithmetic and Applications to Real-Number Proving (Q2945641) (← links)
- Foundational Property-Based Testing (Q2945645) (← links)
- Rewriting Strategies and Strategic Rewrite Programs (Q2945718) (← links)
- UTPCalc — A Calculator for UTP Predicates (Q2971182) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- (Q2979818) (← links)
- (Q2979821) (← links)
- (Q2979849) (← links)
- (Q2979871) (← links)
- Foundational extensible corecursion: a proof assistant perspective (Q2981955) (← links)
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (Q2986838) (← links)
- Certifying Synchrony for Free (Q2996188) (← links)
- (Q3021901) (← links)
