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.


References in zbMATH (referenced in 504 articles , 4 standard articles )

Showing results 1 to 20 of 504.
Sorted by year (citations)

1 2 3 ... 24 25 26 next

  1. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  2. Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
  3. Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (2016)
  4. Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
  5. Rabe, Florian: The future of logic: foundation-independence (2016)
  6. Rossi, Matteo; Mandrioli, Dino; Morzenti, Angelo; Ferrucci, Luca: A temporal logic for micro- and macro-step-based real-time systems: foundations and applications (2016)
  7. Zhan, Bohua: AUTO2, A saturation-based heuristic prover for higher-order logic (2016)
  8. Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)
  9. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: A user-friendly library of real analysis for Coq (2015)
  10. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  11. de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob: The Lean theorem prover (system description) (2015)
  12. Fedyukovich, Grigory; Sharygina, Natasha: Towards completeness in bounded model checking through automatic recursion depth detection (2015)
  13. Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
  14. Muñoz, César A.: Formal methods in air traffic management: the case of unmanned aircraft systems (invited lecture) (2015)
  15. 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)
  16. Paraskevopoulou, Zoe; Hriţcu, Cătălin; Dénès, Maxime; Lampropoulos, Leonidas; Pierce, Benjamin C.: Foundational property-based testing (2015)
  17. Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
  18. 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)
  19. Bertran, Miquel; Babot, Francesc; Climent, August: Formal communication elimination and sequentialization equivalence proofs for distributed system models (2014)
  20. Cavalcanti, Ana; King, Steve; O’Halloran, Colin; Woodcock, Jim: Test-data generation for control coverage by proof (2014)

1 2 3 ... 24 25 26 next