PVS
From MaRDI portal
Software:16016
No author found.
Related Items (only showing first 100 items - show all)
Credible autocoding of convex optimization algorithms ⋮ Sound reasoning in \textit{tock}-CSP ⋮ A refinement of de Bruijn's formal language of mathematics ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Variants of Gödel's ontological proof in a natural deduction calculus ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ Classification of alignments between concepts of formal mathematical systems ⋮ A language with type-dependent equality ⋮ Weakest pre-condition reasoning for Java programs with JML annotations ⋮ Source code verification of a secure payment applet ⋮ How testing helps to diagnose proof failures ⋮ Tests and proofs for custom data generators ⋮ An experiment concerning mathematical proofs on computers with French undergraduate students ⋮ Constructor-based observational logic ⋮ Applied logic for computer scientists. Computational deduction and formal proofs ⋮ A UTP semantic model for Orc language with execution status and fault handling ⋮ Invariants for the FoCaL language ⋮ Contexts in mathematical reasoning and computation ⋮ Pegasus: sound continuous invariant generation ⋮ Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings ⋮ A proof strategy language and proof script generation for Isabelle/HOL ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ A theory of formal synthesis via inductive learning ⋮ A formal proof generator from semi-formal proof documents ⋮ TPS: A theorem-proving system for classical type theory ⋮ A formal proof in Coq of Lasalle's invariance principle ⋮ Proof certificates in PVS ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ Reasoning about algebraic data types with abstractions ⋮ A sound and complete proof system for a unified temporal logic ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Automation for interactive proof: first prototype ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ Lock-free dynamic hash tables with open addressing ⋮ 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 ⋮ Compositional verification of a communication protocol for a remotely operated aircraft ⋮ A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Hidden verification for computational mathematics ⋮ Dealing with algebraic expressions over a field in Coq using Maple ⋮ Cost enforcement in the real-time specification for Java ⋮ Completeness in PVS of a nominal unification algorithm ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ Translating higher-order clauses to first-order clauses ⋮ Universal extensions to simulate specifications ⋮ Formal analysis of the compact position reporting algorithm ⋮ A challenge for atomicity verification ⋮ Unifying simulatability definitions in cryptographic systems under different timing assumptions ⋮ Verifying security protocols with PVS: widening the rank function approach ⋮ Rewriting of imperative programs into logical equations ⋮ Canonization for disjoint unions of theories ⋮ An assertion-based proof system for multithreaded Java ⋮ Semantic models of a timed distributed dataspace architecture ⋮ Zero, successor and equality in BDDs ⋮ Atomic actions, and their refinements to isolated protocols ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Formal methods for smart cards: an experience report ⋮ From LCF to Isabelle/HOL ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Fifty years of Hoare's logic ⋮ Refinement verification of the lazy caching algorithm ⋮ Formalizing ring theory in PVS ⋮ Tactics and certificates in Meta Dedukti ⋮ Fast machine words in Isabelle/HOL ⋮ Relational parametricity and quotient preservation for modular (co)datatypes ⋮ Boosting the reuse of formal specifications ⋮ The Coq library as a theory graph ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Automatically finding theory morphisms for knowledge management ⋮ Theories as types ⋮ Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic ⋮ A certifying square root and division elimination ⋮ Mechanical verification of an ideal incremental ABR conformance algorithm ⋮ An overview of a formal framework for managing mathematics ⋮ Verified interactive computation of definite integrals ⋮ NIL: learning nonlinear interpolants ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ Experiences from exporting major proof assistant libraries ⋮ Terminal satisfiability in GSTE ⋮ Dependent types for program termination verification ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Using PVS to validate the algorithms of an exact arithmetic. ⋮ Coalgebras and monads in the semantics of Java ⋮ Automata-driven automated induction ⋮ High-automation proofs for properties of requirements models ⋮ Mechanized result verification: An industrial application ⋮ Formalization of the computational theory of a Turing complete functional language model ⋮ A formalization of the Smith normal form in higher-order logic ⋮ TAME: Using PVS strategies for special-purpose theorem proving ⋮ Modelling algebraic structures and morphisms in ACL2 ⋮ Proof assistance for real-time systems using an interactive theorem prover ⋮ Formally verified tableau-based reasoners for a description logic ⋮ Formalization of Bernstein polynomials and applications to global optimization ⋮ On the formalization of gamma function in HOL ⋮ On the desirability of mechanizing calculational proofs ⋮ A general setting for flexibly combining and augmenting decision procedures ⋮ Design and verification of distributed recovery blocks with CSP
This page was built for software: PVS
