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 504 articles , 4 standard articles )
Showing results 1 to 20 of 504.
Sorted by year (- Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
- Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
- Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (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)
- Zhan, Bohua: AUTO2, A saturation-based heuristic prover for higher-order logic (2016)
- Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: A user-friendly library of real analysis for Coq (2015)
- Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
- de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
- Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
- Muñoz, César A.: Formal methods in air traffic management: the case of unmanned aircraft systems (invited lecture) (2015)
- Narkawicz, Anthony; Muñoz, César; Dutle, Aaron: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems (2015)
- Paraskevopoulou, Zoe; Hriţcu, Cătălin; Dénès, Maxime; Lampropoulos, Leonidas; Pierce, Benjamin C.: Foundational property-based testing (2015)
- Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
- Banach, Richard; Zhu, Huibiao; Su, Wen; Huang, Runlei: Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (2014)
- Bertran, Miquel; Babot, Francesc; Climent, August: Formal communication elimination and sequentialization equivalence proofs for distributed system models (2014)
- Cavalcanti, Ana; King, Steve; O’Halloran, Colin; Woodcock, Jim: Test-data generation for control coverage by proof (2014)