PVS
From MaRDI portal
Software:16016
swMATH3484MaRDI QIDQ16016FDOQ16016
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Formal Proofs for Nonlinear Optimization
- A computer checked algebraic verification of a distributed summation algorithm
- Proof assistance for real-time systems using an interactive theorem prover
- Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
- Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
- Deductive verification of advanced out-of-order microprocessors.
- Rewriting, inference, and proof
- Verification of cache coherence protocols by aggregation of distributed transactions
- Extending Hoare logic to real-time
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- How testing helps to diagnose proof failures
- Tests and proofs for custom data generators
- Real Number Calculations and Theorem Proving
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- Title not available (Why is that?)
- A theory of formal synthesis via inductive learning
- Applied logic for computer scientists. Computational deduction and formal proofs
- Formal verification of a complex pipelined processor
- A general framework for pattern-driven modal tableaux
- Metalogical frameworks. II: Developing a reflected decision procedure
- A UTP semantic model for Orc language with execution status and fault handling
- Title not available (Why is that?)
- Semantic models of a timed distributed dataspace architecture
- On Shostak's decision procedure for combinations of theories
- Computer Aided Verification
- Automated complexity analysis of Nuprl extracted programs
- Simple network protocol simulation within Maude
- Theorem Proving in Higher Order Logics
- A comparison of tools for teaching formal software verification
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- A tool-supported proof system for multithreaded Java.
- Theorem Proving in Higher Order Logics
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- The stable revivals model in CSP-Prover
- Views of pi: definition and computation
- Interactive tool support for CSP \(\parallel\) B consistency checking
- Title not available (Why is that?)
- Title not available (Why is that?)
- A first order logic for specification of timed algorithms: Basic properties and a decidable class
- Mechanized proofs of opacity: a comparison of two techniques
- A practical integration of first-order reasoning and decision procedures
- Title not available (Why is that?)
- Making PVS accessible to generic services by interpretation in a universal format
- Proof certificates in PVS
- Networks of processes with parameterized state space
- Title not available (Why is that?)
- Title not available (Why is that?)
- Foundational extensible corecursion: a proof assistant perspective
- Formalizing the confluence of orthogonal rewriting systems
- Verifying Lock-Freedom Using Well-Founded Orders
- Proof-search in type-theoretic languages: An introduction
- A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
- A realistic involvement of formal methods
- Deductive verification of real-time systems using STeP
- Bounded model checking for timed automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verified Real Number Calculations: A Library for Interval Arithmetic
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- The future of logic: foundation-independence
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- A scalable module system
- Semantic essence of AsmL
- A Coq formalization of Lebesgue integration of nonnegative functions
- The coalgebraic class specification language CCSL
- Automating Induction with an SMT Solver
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Title not available (Why is that?)
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Theorem proving in cancellative abelian monoids (extended abstract)
- A decision procedure for linear ``big O equations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated theorem proving for special functions: the next phase
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- New results on rewrite-based satisfiability procedures
- Mathematical Knowledge Management
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Computer supported mathematics with \(\Omega\)MEGA
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- Efficiently checking propositional refutations in HOL theorem provers
- Modelling timed reactive systems from natural-language requirements
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A constructive algebraic hierarchy in Coq.
- A rewriting approach to satisfiability procedures.
- The cognitive agents specification language and verification environment
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
This page was built for software: PVS
