The following pages link to PVS (Q16016):
Displaying 50 items.
- Analysis of a biphase mark protocol with Uppaal and PVS (Q855013) (← links)
- Lock-free parallel and concurrent garbage collection by mark\&sweep (Q858913) (← links)
- Formal analysis of multiparty contract signing (Q861699) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- Specification and analysis of the AER/NCA active network protocol suite in real-time Maude (Q862853) (← links)
- A general lock-free algorithm using compare-and-swap (Q865625) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Verifying a signature architecture: a comparative case study (Q877156) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- Automated compositional proofs for real-time systems (Q882449) (← links)
- Using formal reasoning on a model of tasks for FreeRTOS (Q903515) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- A functional formalization of on chip communications (Q931433) (← links)
- The higher-order-logic Formath (Q935562) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings (Q955386) (← links)
- Goto elimination in program algebra (Q955712) (← links)
- Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections (Q970002) (← links)
- The proof monad (Q974136) (← links)
- A general technique for proving lock-freedom (Q1001810) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- A queue based mutual exclusion algorithm (Q1006897) (← links)
- Trace-based derivation of a scalable lock-free stack algorithm (Q1019022) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Invariant based programming: Basic approach and teaching experiences (Q1019025) (← links)
- A comparison of tools for teaching formal software verification (Q1019026) (← links)
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs (Q1025311) (← links)
- A formal framework for modeling and validating simulink diagrams (Q1037245) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Verification of cache coherence protocols by aggregation of distributed transactions (Q1265158) (← links)
- Metalogical frameworks. II: Developing a reflected decision procedure (Q1283204) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Extending Hoare logic to real-time (Q1346769) (← links)
- Automated theorem proving by test set induction (Q1355757) (← links)
- Verification of the Miller-Rabin probabilistic primality test. (Q1400288) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol (Q1402474) (← links)
- Incorporating decision procedures in implicit induction. (Q1404422) (← links)
- A constructive algebraic hierarchy in Coq. (Q1404425) (← links)
- Formal foundations of operational semantics (Q1426872) (← links)
- A mechanized proof environment for the convenient computations proof method (Q1426938) (← links)
- Formal verification of a complex pipelined processor (Q1426941) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Class refinement as semantics of correct object substitutability (Q1586166) (← links)
- Deductive verification of real-time systems using STeP (Q1589585) (← links)
