The following pages link to PVS (Q16016):
Displaying 50 items.
- TAME: Using PVS strategies for special-purpose theorem proving (Q1601865) (← links)
- Proof assistance for real-time systems using an interactive theorem prover (Q1603708) (← links)
- On the desirability of mechanizing calculational proofs (Q1607098) (← links)
- A general setting for flexibly combining and augmenting decision procedures (Q1610671) (← links)
- How testing helps to diagnose proof failures (Q1624590) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- Applied logic for computer scientists. Computational deduction and formal proofs (Q1627457) (← links)
- A UTP semantic model for Orc language with execution status and fault handling (Q1633048) (← links)
- Mechanized proofs of opacity: a comparison of two techniques (Q1673658) (← links)
- A theory of formal synthesis via inductive learning (Q1674868) (← links)
- A formal proof generator from semi-formal proof documents (Q1675786) (← links)
- A formal proof in Coq of Lasalle's invariance principle (Q1687728) (← links)
- Proof certificates in PVS (Q1687741) (← links)
- Making PVS accessible to generic services by interpretation in a universal format (Q1687752) (← links)
- Reasoning about algebraic data types with abstractions (Q1694026) (← links)
- From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (Q1704601) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- An assertion-based proof system for multithreaded Java (Q1770359) (← links)
- Semantic models of a timed distributed dataspace architecture (Q1770360) (← links)
- Zero, successor and equality in BDDs (Q1772774) (← links)
- Formal methods for smart cards: an experience report (Q1776578) (← links)
- Formalizing ring theory in PVS (Q1791143) (← links)
- Tactics and certificates in Meta Dedukti (Q1791152) (← links)
- Fast machine words in Isabelle/HOL (Q1791180) (← links)
- Relational parametricity and quotient preservation for modular (co)datatypes (Q1791181) (← links)
- Boosting the reuse of formal specifications (Q1791193) (← links)
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (Q1798665) (← links)
- Automatically finding theory morphisms for knowledge management (Q1798969) (← links)
- Theories as types (Q1799118) (← links)
- Mechanical verification of an ideal incremental ABR conformance algorithm (Q1810852) (← links)
- An overview of a formal framework for managing mathematics (Q1810918) (← links)
- Dependent types for program termination verification (Q1850960) (← links)
- Using PVS to validate the algorithms of an exact arithmetic. (Q1853641) (← links)
- Coalgebras and monads in the semantics of Java (Q1853752) (← links)
- Automata-driven automated induction (Q1854445) (← links)
- High-automation proofs for properties of requirements models (Q1856143) (← links)
- Mechanized result verification: An industrial application (Q1856154) (← links)
- Design and verification of distributed recovery blocks with CSP (Q1870210) (← links)
- A refinement of de Bruijn's formal language of mathematics (Q1876109) (← links)
- Weakest pre-condition reasoning for Java programs with JML annotations (Q1881666) (← links)
- Source code verification of a secure payment applet (Q1881671) (← links)
- An experiment concerning mathematical proofs on computers with French undergraduate students (Q1884267) (← links)
- Contexts in mathematical reasoning and computation (Q1895411) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Lock-free dynamic hash tables with open addressing (Q1953636) (← links)
- Rewriting logic and its applications. 8th international workshop, WRLA 2010, held as a satellite event of ETAPS 2010, Paphos, Cyprus, March 20--21, 2010. Revised selected papers (Q1958747) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- Formal analysis of the compact position reporting algorithm (Q1996426) (← links)
