PVS
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A general technique for proving lock-freedom
- Efficiently checking propositional refutations in HOL theorem provers
- A queue based mutual exclusion algorithm
- Trace-based derivation of a scalable lock-free stack algorithm
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Invariant based programming: Basic approach and teaching experiences
- A comparison of tools for teaching formal software verification
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- A formal framework for modeling and validating simulink diagrams
- Operating system verification---an overview
- Data compression for proof replay
- Verification of cache coherence protocols by aggregation of distributed transactions
- Metalogical frameworks. II: Developing a reflected decision procedure
- ACL2
- AXIOM
- Coq
- FMona
- IMPS: An interactive mathematical proof system
- Isabelle
- LEO-II
- MetiTarski
- Nitpick
- ObjectCheck
- An overview of the Tecton proof system
- PAG
- Extending Hoare logic to real-time
- jsCoq
- HolPy
- Automated theorem proving by test set induction
- SACLIB
- SDSAT
- Theorema
- TkWinHOL
- TPS
- Valigator
- Zing
- ML
- Alloy
- Verification of the Miller-Rabin probabilistic primality test.
- Kronos
- A rewriting approach to satisfiability procedures.
- Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
- Incorporating decision procedures in implicit induction.
- A constructive algebraic hierarchy in Coq.
- CLEAN
- Formal foundations of operational semantics
- A mechanized proof environment for the convenient computations proof method
- Formal verification of a complex pipelined processor
- Isabelle/HOL
- SyncGen
- Isabelle/Isar
- LARCH
- GOLOG
- CASL
- SCTL-MUS
- ACSAR
- ASTRAL
- CACTUS
- MASCOT
- LOTOS
- MOTOR
- KARO
- SPARK
- KRAKATOA
- ATERM
- Proof-search in type-theoretic languages: An introduction
- RAISE
- IF-2.0
- Class refinement as semantics of correct object substitutability
- CCSL
- OMRS
- Deductive verification of real-time systems using STeP
- TCOZ
- APTS
- MAYA
- SPIN
- TAME: Using PVS strategies for special-purpose theorem proving
- Proof assistance for real-time systems using an interactive theorem prover
- KeYmaera
- On the desirability of mechanizing calculational proofs
- A general setting for flexibly combining and augmenting decision procedures
- How testing helps to diagnose proof failures
- Tests and proofs for custom data generators
- Applied logic for computer scientists. Computational deduction and formal proofs
- Fujaba
- HyTech
- A UTP semantic model for Orc language with execution status and fault handling
- ACSL
- 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
- JML
- Spec#
- Isar
- Omnibus
- MetaPRL
- Frama-C
- UCLID
- Uppaal
- Mizar
This page was built for software: PVS
