PVS
PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.
Keywords for this software
References in zbMATH (referenced in 566 articles , 4 standard articles )
Showing results 1 to 20 of 566.
Sorted by year (- Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
- Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
- Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
- He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
- Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
- Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
- Müller, Dennis; Kohlhase, Michael; Rabe, Florian: Automatically finding theory morphisms for knowledge management (2018)
- Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
- Newell, Josh; Pang, Linna; Tremaine, David; Wassyng, Alan; Lawford, Mark: Translation of IEC 61131-3 function block diagrams to PVS for formal verification with real-time nuclear application (2018)
- Petiot, Guillaume; Kosmatov, Nikolai; Botella, Bernard; Giorgetti, Alain; Julliand, Jacques: How testing helps to diagnose proof failures (2018)
- Rabe, Florian: A modular type reconstruction algorithm (2018)
- Sardar, Muhammad Usama; Afaq, Nida; Hasan, Osman; Hoque, Khaza Anuarul: Towards probabilistic formal analysis of SATS-simultaneously moving aircraft (SATS-SMA) (2018)
- Shankar, Natarajan: Combining model checking and deduction (2018)
- Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)
- Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
- Aguado, F.; Ascariz, P.; Cabalar, P.; Pérez, G.; Vidal, C.: Verification for ASP denotational semantics: a case study using the PVS theorem prover (2017)
- Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
- Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal (\alpha)-equivalence with A and AC function symbols (2017)
- Ayala-Rincón, Mauricio; de Moura, Flávio L. C.: Applied logic for computer scientists. Computational deduction and formal proofs (2017)
- Ayala-Rincón, Mauricio (ed.); Muñoz, César A. (ed.): Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (2017)