The following pages link to PVS (Q16016):
Displaying 50 items.
- (Q3021914) (← links)
- (Q3024916) (← links)
- (Q3051901) (← links)
- Saoithín: A Theorem Prover for UTP (Q3055742) (← links)
- The Cognitive Agents Specification Language and Verification Environment (Q3056334) (← links)
- Axiomatic semantics of projection temporal logic programs (Q3060195) (← links)
- An Assume Guarantee Approach for Checking Quantified Array Assertions (Q3067480) (← links)
- (Q3075241) (← links)
- ExplainHoudini: Making Houdini Inference Transparent (Q3075491) (← links)
- Logical Formalisation and Analysis of the Mifare Classic Card in PVS (Q3087992) (← links)
- Towards Robustness Analysis Using PVS (Q3087998) (← links)
- Validating QBF Validity in HOL4 (Q3088005) (← links)
- Ordered chaining calculi for first-order theories of transitive relations (Q3158528) (← links)
- Specification and Verification of Multi-Agent Systems (Q3166991) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Combining Model Checking and Deduction (Q3176378) (← links)
- Soundly Proving B Method Formulæ Using Typed Sequent Calculus (Q3179401) (← links)
- An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs (Q3296349) (← links)
- (Q3370736) (← links)
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (Q3434629) (← links)
- The Lean Theorem Prover (System Description) (Q3454108) (← links)
- The Logic of U ·(TP)2 (Q3455647) (← links)
- (Q3497624) (← links)
- (Q3497626) (← links)
- Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS (Q3510806) (← links)
- Enhancing Program Verification with Lemmas (Q3512504) (← links)
- Safe Modification of Pointer Programs in Refinement Calculus (Q3521993) (← links)
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL (Q3523164) (← links)
- A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic (Q3523171) (← links)
- A Compressing Translation from Propositional Resolution to Natural Deduction (Q3525003) (← links)
- Verifying Lock-Freedom Using Well-Founded Orders (Q3525079) (← links)
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics (Q3535610) (← links)
- On the strength of proof-irrelevant type theories (Q3535620) (← links)
- Automating Algebraic Specifications of Non-freely Generated Data Types (Q3540070) (← links)
- Convergence Verification: From Shared Memory to Partially Synchronous Systems (Q3543300) (← links)
- Twenty Years of Theorem Proving for HOLs Past, Present and Future (Q3543642) (← links)
- LCF-Style Propositional Simplification with BDDs and SAT Solvers (Q3543649) (← links)
- Real Number Calculations and Theorem Proving (Q3543660) (← links)
- A Formalized Theory for Verifying Stability and Convergence of Automata in PVS (Q3543661) (← links)
- Complete Integer Decision Procedures as Derived Rules in HOL (Q3559760) (← links)
- Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover (Q3559766) (← links)
- First Order Logic with Domain Conditions (Q3559768) (← links)
- Formal Proof of SCHUR Conjugate Function (Q3582705) (← links)
- Towards MKM in the Large: Modular Representation and Scalable Software Architecture (Q3582723) (← links)
- Unraveling a Card Trick (Q3587256) (← links)
- Preserving Secrecy Under Refinement (Q3591420) (← links)
- Subset Coercions in Coq (Q3612448) (← links)
- Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm (Q3612661) (← links)
- Representing and Reasoning with Operational Semantics (Q3613396) (← links)
- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics (Q3613407) (← links)
