PVS

swMATH3484MaRDI QIDQ16016FDOQ16016

Author name not available (Why is that?)

Described by source

• A Brief Overview of PVS
• Fixpoints and search in PVS
• Unnamed Publication
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• High-automation proofs for properties of requirements models
• Mechanized result verification: An industrial application
• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• A formalization of the Smith normal form in higher-order logic
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Canonization for disjoint unions of theories
• Formal analysis of the compact position reporting algorithm
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Design and verification of distributed recovery blocks with CSP
• The Imandra Automated Reasoning System (System Description)
• Source code verification of a secure payment applet
• Extensional higher-order paramodulation in Leo-III
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• Completeness in PVS of a nominal unification algorithm
• Automated Reasoning with Analytic Tableaux and Related Methods
• An experiment concerning mathematical proofs on computers with French undergraduate students
• A Compressing Translation from Propositional Resolution to Natural Deduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Contexts in mathematical reasoning and computation
• A Modular Type Reconstruction Algorithm
• A Complete Axiomatic Semantics for the CSP Stable-Failures Model
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• Equivalent semantic models for a distributed dataspace architecture.
• The coinductive approach to verifying cryptographic protocols.
• Zero, successor and equality in BDDs
• Mechanical verification of concurrency control and recovery protocols
• Formalizing Cut Elimination of Coalgebraic Logics in Coq
• Formalization of the integral calculus in the PVS theorem prover
• Boosting the reuse of formal specifications
• Formalizing ring theory in PVS
• Relational parametricity and quotient preservation for modular (co)datatypes
• Tactics and certificates in Meta Dedukti
• Automatically finding theory morphisms for knowledge management
• Theories as types
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• From LCF to Isabelle/HOL
• Formalizing Ordinal Partition Relations Using Isabelle/HOL
• A layered algorithm for quantifier elimination from linear modular constraints
• An overview of a formal framework for managing mathematics
• Experiences from exporting major proof assistant libraries
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
• Title not available (Why is that?)
• Using semantic correctness in multidatabases to achieve local autonomy, distribute coordination, and maintain global integrity
• A case study in class library verification: Java's vector class
• A timed verification of the IEEE 1394 Leader election protocol
• The Coq library as a theory graph
• Reasoning about algebraic data types with abstractions
• Modelling algebraic structures and morphisms in ACL2
• Title not available (Why is that?)
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• Removing algebraic data types from constrained Horn clauses using difference predicates
• A complete proof system for propositional projection temporal logic
• Hidden verification for computational mathematics
• A logical framework combining model and proof theory
• Universal extensions to simulate specifications
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Incorporating decision procedures in implicit induction.
• Title not available (Why is that?)
• 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
• Formal analysis of multiparty contract signing
• Mechanical verification of an ideal incremental ABR conformance algorithm
• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• A scalable lock-free stack algorithm
• Automated compositional proofs for real-time systems
• A queue based mutual exclusion algorithm
• Computer-assisted analysis of the Anderson-Hájek ontological controversy
• Analysis of a biphase mark protocol with Uppaal and PVS
• Lock-free parallel and concurrent garbage collection by mark\&sweep
• Nonblocking Algorithms and Backward Simulation
• Trace-based derivation of a scalable lock-free stack algorithm
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Operational semantics for timed systems. A non-standard approach to uniform modeling of timed and hybrid systems.
• Automated Deduction – CADE-20
• Towards MKM in the large: modular representation and scalable software architecture
• Verification of distributed systems with local-global predicates
• Provably correct conflict prevention bands algorithms
• Coalgebras for binary methods: Properties of bisimulations and invariants
• Coalgebras and monads in the semantics of Java
• Stack-based access control and secure information flow
• Formal Modeling and Analysis of Timed Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verification of sequential and concurrent programs
• A functional formalization of on chip communications
• Rewriting Strategies and Strategic Rewrite Programs
• Automata-driven automated induction
• Title not available (Why is that?)
• Polynomial function intervals for floating-point software verification
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for software: PVS