The following pages link to PVS (Q16016):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (Q264193) (← links)
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- Modelling timed reactive systems from natural-language requirements (Q315301) (← links)
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Rewriting modulo SMT and open system analysis (Q347384) (← links)
- Recent advances in program verification through computer algebra (Q351971) (← links)
- A complete proof system for propositional projection temporal logic (Q391223) (← links)
- A scalable module system (Q391632) (← links)
- Verification of distributed systems with local-global predicates (Q432134) (← links)
- Provably correct conflict prevention bands algorithms (Q436402) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Polynomial function intervals for floating-point software verification (Q457251) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Formal communication elimination and sequentialization equivalence proofs for distributed system models (Q466919) (← links)
- Applications of real number theorem proving in PVS (Q469367) (← links)
- An inductive approach to strand spaces (Q470008) (← links)
- Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
- A temporal logic for micro- and macro-step-based real-time systems: foundations and applications (Q530560) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- A mechanical verification of the stressing algorithm for negative cost cycle detection in networks (Q532429) (← links)
- Optimal deployment of eventually-serializable data services (Q545558) (← links)
- Structured derivations: a unified proof style for teaching mathematics (Q607406) (← links)
- Theorem prover approach to semistructured data design (Q609020) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Automated flaw detection in algebraic specifications (Q616853) (← links)
- Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (Q617922) (← links)
- Bisimulation conversion and verification procedure for goal-based control systems (Q633304) (← links)
- A formal library of set relations and its application to synchronous languages (Q654904) (← links)
- A scalable lock-free stack algorithm (Q666004) (← links)
- Verifying relative safety, accuracy, and termination for program approximations (Q682353) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- The world's shortest correct exact real arithmetic program? (Q714620) (← links)
- A theory of software product line refinement (Q714875) (← links)
- Frame rule for mutually recursive procedures manipulating pointers (Q732009) (← links)
- Correctness and concurrent complexity of the black-white bakery algorithm (Q736464) (← links)
- Test-data generation for control coverage by proof (Q736805) (← links)
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (Q736916) (← links)
- A formal proof of the deadline driven scheduler in PPTL axiomatic system (Q744103) (← links)
- On the refinement of liveness properties of distributed systems (Q763239) (← links)
- Translating Java for multiple model checkers: The Bandera back-end (Q816196) (← links)
- Automated analysis of fault-tolerance in distributed systems (Q816197) (← links)
- Formal verification of the VAMP floating point unit (Q816201) (← links)
- A complete mechanization of correctness of a string-preprocessing algorithm (Q816208) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- ProofViz: an interactive visual proof explorer (Q832103) (← links)
- Formal memory models for the verification of low-level operating-system code (Q835773) (← links)
- Verification of sequential and concurrent programs (Q837527) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Cones and foci: A mechanical framework for protocol verification (Q853730) (← links)
