PVS
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A parallelized theorem prover for a logic with parallel execution
- Proof assistant decision procedures for formalizing origami
- scientific article; zbMATH DE number 1251178 (Why is no real title available?)
- A complete proof system for propositional projection temporal logic
- Goto elimination in program algebra
- Coalgebraic theories of sequences in PVS
- The seventeen provers of the world. Foreword by Dana S. Scott..
- scientific article; zbMATH DE number 1670799 (Why is no real title available?)
- scientific article; zbMATH DE number 1614688 (Why is no real title available?)
- Hidden verification for computational mathematics
- High-automation proofs for properties of requirements models
- Mechanized result verification: An industrial application
- Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal
- Universal extensions to simulate specifications
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- Formal proof of a wave equation resolution scheme: the method error
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- Verified Real Number Calculations: A Library for Interval Arithmetic
- A user-friendly interface for a lightweight verification system
- A logical framework combining model and proof theory
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal methods for smart cards: an experience report
- Verifying relative safety, accuracy, and termination for program approximations
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs
- scientific article; zbMATH DE number 2185723 (Why is no real title available?)
- scientific article; zbMATH DE number 1670798 (Why is no real title available?)
- Verification, Model Checking, and Abstract Interpretation
- Formal Proofs for Nonlinear Optimization
- The future of logic: foundation-independence
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
- A framework for developing stand-alone certifiers
- A mechanical verification of the stressing algorithm for negative cost cycle detection in networks
- scientific article; zbMATH DE number 1979548 (Why is no real title available?)
- scientific article; zbMATH DE number 2080036 (Why is no real title available?)
- scientific article; zbMATH DE number 2090312 (Why is no real title available?)
- Incorporating decision procedures in implicit induction.
- scientific article; zbMATH DE number 1543047 (Why is no real title available?)
- Formal semantics of a VDM extension for distributed embedded systems
- Axiomatic semantics of projection temporal logic programs
- DNA Computing
- A formalization of the Smith normal form in higher-order logic
- Formal analysis of multiparty contract signing
- scientific article; zbMATH DE number 1086721 (Why is no real title available?)
- A computer checked algebraic verification of a distributed summation algorithm
- ProofViz: an interactive visual proof explorer
- scientific article; zbMATH DE number 2085344 (Why is no real title available?)
- scientific article; zbMATH DE number 2090144 (Why is no real title available?)
- A realizability interpretation of Church's simple theory of types
- On the desirability of mechanizing calculational proofs
- Correct Hardware Design and Verification Methods
- scientific article; zbMATH DE number 2090517 (Why is no real title available?)
- scientific article; zbMATH DE number 1852158 (Why is no real title available?)
- A scalable module system
- Canonization for disjoint unions of theories
- Proof assistance for real-time systems using an interactive theorem prover
- ProofWidgets
- Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
- Compositional verification of a communication protocol for a remotely operated aircraft
- Programming Languages and Systems
- Building reliable, high-performance networks with the Nuprl proof development system
- scientific article; zbMATH DE number 1956576 (Why is no real title available?)
- scientific article; zbMATH DE number 1796121 (Why is no real title available?)
- Semantic essence of AsmL
- scientific article; zbMATH DE number 1860617 (Why is no real title available?)
- scientific article; zbMATH DE number 1860624 (Why is no real title available?)
- Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
- A Coq formalization of Lebesgue integration of nonnegative functions
- Formalizing ordinal partition relations using Isabelle/HOL
- Formal memory models for the verification of low-level operating-system code
- The coalgebraic class specification language CCSL
- A framework for formally verifying software transactional memory algorithms
- Formal analysis of the compact position reporting algorithm
- scientific article; zbMATH DE number 1951639 (Why is no real title available?)
- Optimal deployment of eventually-serializable data services
- Verifying a signature architecture: a comparative case study
- Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model
- Logic-based specification languages for intelligent software agents
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Automating Algebraic Specifications of Non-freely Generated Data Types
- Design and verification of distributed recovery blocks with CSP
- A scalable lock-free stack algorithm
- Mechanical verification of an ideal incremental ABR conformance algorithm
- scientific article; zbMATH DE number 1231700 (Why is no real title available?)
- scientific article; zbMATH DE number 2000403 (Why is no real title available?)
- Automated compositional proofs for real-time systems
- scientific article; zbMATH DE number 7121901 (Why is no real title available?)
- Deductive verification of advanced out-of-order microprocessors.
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- A queue based mutual exclusion algorithm
- Automating Induction with an SMT Solver
- A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
- A decision procedure for univariate polynomial systems based on root counting and interval subdivision
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- scientific article; zbMATH DE number 1980938 (Why is no real title available?)
- The seven virtues of simple type theory
- scientific article; zbMATH DE number 1863374 (Why is no real title available?)
- scientific article; zbMATH DE number 1863380 (Why is no real title available?)
This page was built for software: PVS
