Cited in
(only showing first 100 items - show all)- Dafny: an automatic program verifier for functional correctness
- CVPP: a tool set for compositional verification of control-flow safety properties
- Faster and more complete extended static checking for the Java modeling language
- Verification of concurrent systems with VerCors
- Ynot: dependent types for imperative programs
- CVPP
- Dafny
- HOL-Boogie
- Valigator
- IMP++
- jContractor
- Ada95
- ArcAngel
- LARCH
- SCOOP
- TASC
- HOL-Z
- KRAKATOA
- SPARK
- Eiffel
- ACSL
- distcc
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- Alt-Ergo
- cvc3
- SIMPLIFY
- OptiML
- Rascal
- Zap
- Rodin
- ESC/Java
- JUnit
- Pex
- VCC
- JACK
- Boogie
- Chalice
- MAVEN
- VeriFast
- Leon
- Cyclone
- HighSpec
- Amphion
- Coquet
- Smallfoot
- KeY
- FixBag
- KIV
- WhyML
- VeriCool
- LOOP
- TVLA
- Viper
- jStar
- VerCors
- SpecExplorer
- Jahob
- Ynot
- CSPsim
- Contract
- Grasshopper
- BVD
- SmallEiffel
- Clara
- THOR
- Featherweight Java
- EventB2Dafny
- coreStar
- LCLint
- Atoment
- CacBDD
- Splint
- ExplainHoudini
- Houdini
- OpenJML
- DKAL
- MiniMaple
- Racket
- HAVOC
- C-Light
- TreatJS
- Verasco
- BoogiePL
- MarQ
- StaRVOOrS
- Rocksalt
- Cibai
- Nemerle
- Rust
- Kami
- POSIX Lexing
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- A parametric segmentation functor for fully automatic and scalable array content analysis
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Valigator: A Verification Tool with Bound and Invariant Generation
- Zeno: an automated prover for properties of recursive data structures
This page was built for software: Spec#
