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 600 articles , 4 standard articles )

Showing results 541 to 560 of 600.
Sorted by year (citations)

previous 1 2 3 ... 26 27 28 29 30 next

  1. Roychoudhury, Abhik; Kumar, K. Narayan; Ramakrishnan, C. R.; Ramakrishnan, I. V.; Smolka, Scott A.: Verification of parameterized systems using logic program transformations (2000)
  2. Rushby, John: Verification diagrams revisited: Disjunctive invariants for easy verification (2000)
  3. Rusinowitch, Michaël; Stratulat, Sorin; Klay, Francis: Mechanical verification of an ideal incremental ABR conformance algorithm (2000)
  4. Shankar, Natarajan: Combining theorem proving and model checking through symbolic analysis (2000)
  5. Shankar, Natarajan; Owre, Sam: Principles and pragmatics of subtyping in PVS (2000)
  6. Sorge, Volker: Non-trivial symbolic computations in proof planning (2000)
  7. Traoré, Issa: An outline of PVS semantics for UML statecharts (2000)
  8. Traverso, Paolo; Bertoli, Piergiorgio: Mechanized result verification: An industrial application (2000)
  9. van den Berg, Joachim; Huisman, Marieke; Jacobs, Bart; Poll, Erik: A type-theoretic memory model for verification of sequential Java programs (2000)
  10. Abdulla, Parosh Aziz; Annichini, Aurore; Bensalem, Saddek; Bouajjani, Ahmed; Habermehl, Peter; Lachnech, Yassine: Verification of infinite-state systems by combining abstraction and reachability analysis (1999)
  11. Adams, A. A.; Gottliebsen, H.; Linton, S. A.; Martin, U.: VSDITLU: A verifiable symbolic definite integral table look-up (1999)
  12. Aitken, William E.; Constable, Robert L.; Underwood, Judith L.: Metalogical frameworks. II: Developing a reflected decision procedure (1999)
  13. Berghofer, Stefan; Wenzel, Markus: Inductive datatypes in HOL -- lessons learned in formal-logic engineering (1999)
  14. Bolignano, Dominique: Using abstract interpretation for the safe verification of security protocols (1999)
  15. Bowen, Jonathan P. (ed.); Hinchey, Michael G. (ed.): High-integrity system specification and design (1999)
  16. Dellacherie, S.; Devulder, S.; Lambert, J.-L.: Software verification based on linear programming (1999)
  17. Filliâtre, Jean-Christophe: Proof of imperative programs in type theory (1999)
  18. Gärtner, Felix C.: Transformational approaches to the specification and verification of fault-tolerant systems: Formal background and classification (1999)
  19. Goerigk, Wolfgang; Gaul, Thilo; Zimmermann, Wolf: Correct programs without proof? On checker-based program verification (1999)
  20. Hensel, Ulrich; Jacobs, Bart: Coalgebraic theories of sequences in PVS (1999)

previous 1 2 3 ... 26 27 28 29 30 next