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 491 articles , 4 standard articles )
Showing results 1 to 20 of 491.
Sorted by year (- 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)
- Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
- Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
- Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
- Nagashima, Yutaka; Kumar, Ramana: A proof strategy language and proof script generation for Isabelle/HOL (2017)
- Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
- Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
- Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
- Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano: Infinite-state invariant checking with IC3 and predicate abstraction (2016)
- Halmagrand, Pierre: Soundly proving B method formulæusing typed sequent calculus (2016)
- Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (2016)
- John, Ajith K.; Chakraborty, Supratik: A layered algorithm for quantifier elimination from linear modular constraints (2016)
- Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
- Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
- Rabe, Florian: The future of logic: foundation-independence (2016)
- Rossi, Matteo; Mandrioli, Dino; Morzenti, Angelo; Ferrucci, Luca: A temporal logic for micro- and macro-step-based real-time systems: foundations and applications (2016)
- Wang, Timothy; Jobredeaux, Romain; Pantel, Marc; Garoche, Pierre-Loic; Feron, Eric; Henrion, Didier: Credible autocoding of convex optimization algorithms (2016)
- Wimmer, Simon: Formalized timed automata (2016)
- Zhan, Bohua: AUTO2, A saturation-based heuristic prover for higher-order logic (2016)