The following pages link to PVS (Q16016):
Displaying 50 items.
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (Q2069874) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
- Formalization of the computational theory of a Turing complete functional language model (Q2102949) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- Sound reasoning in \textit{tock}-CSP (Q2120813) (← links)
- A language with type-dependent equality (Q2128827) (← links)
- Pegasus: sound continuous invariant generation (Q2147687) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- A sound and complete proof system for a unified temporal logic (Q2197533) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- Atomic actions, and their refinements to isolated protocols (Q2268472) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- The Coq library as a theory graph (Q2287907) (← links)
- NIL: learning nonlinear interpolants (Q2305413) (← links)
- Terminal satisfiability in GSTE (Q2336669) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- Formally verified tableau-based reasoners for a description logic (Q2351147) (← links)
- Formalization of Bernstein polynomials and applications to global optimization (Q2351165) (← links)
- On the formalization of gamma function in HOL (Q2352499) (← links)
- Credible autocoding of convex optimization algorithms (Q2358081) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Variants of Gödel's ontological proof in a natural deduction calculus (Q2363503) (← links)
- Infinite-state invariant checking with IC3 and predicate abstraction (Q2363814) (← links)
- A layered algorithm for quantifier elimination from linear modular constraints (Q2363817) (← links)
- Classification of alignments between concepts of formal mathematical systems (Q2364703) (← links)
- Constructor-based observational logic (Q2369030) (← links)
- Invariants for the FoCaL language (Q2379680) (← links)
- Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (Q2402234) (← links)
- A proof strategy language and proof script generation for Isabelle/HOL (Q2405272) (← links)
- Verifying a scheduling protocol of safety-critical systems (Q2424721) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Compositional verification of a communication protocol for a remotely operated aircraft (Q2442952) (← links)
- Hidden verification for computational mathematics (Q2456559) (← links)
- Dealing with algebraic expressions over a field in Coq using Maple (Q2456560) (← links)
- Cost enforcement in the real-time specification for Java (Q2460195) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Universal extensions to simulate specifications (Q2475808) (← links)
- A challenge for atomicity verification (Q2482021) (← links)
- Unifying simulatability definitions in cryptographic systems under different timing assumptions (Q2484407) (← links)
- Verifying security protocols with PVS: widening the rank function approach (Q2484411) (← links)
- Rewriting of imperative programs into logical equations (Q2486260) (← links)
- Canonization for disjoint unions of theories (Q2486580) (← links)
- Refinement verification of the lazy caching algorithm (Q2509154) (← links)
- Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic (Q2517836) (← links)
- A certifying square root and division elimination (Q2520687) (← links)
