Boogie
From MaRDI portal
swMATH7714MaRDI QIDQ19731FDOQ19731
Author name not available (Why is that?)
Official website: http://research.microsoft.com/en-us/projects/boogie/
Source code repository: https://github.com/boogie-org/boogie
Cited In (only showing first 100 items - show all)
- Regression verification for unbalanced recursive functions
- Faster and more complete extended static checking for the Java modeling language
- Automating Induction with an SMT Solver
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Boolector
- HOL-Boogie
- IMP++
- ACSL
- SMT-LIB
- distcc
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- cvc3
- Spec#
- LLVM
- Dagger
- SIMPLIFY
- z3
- ProMoVer
- Atelier B
- Rodin
- ESC/Java
- ESC4
- Scala
- PathCrawler
- Pex
- VCC
- JACK
- AURA
- ACL2s
- Chalice
- KRATOS
- CompCertTSO
- VeriFast
- cminor
- HighSpec
- HIP
- InvGen
- Checkfence
- HMC
- CCured
- Smallfoot
- NaCl
- KeY
- SLAB
- FixBag
- KIV
- WhyML
- BWare
- VeriCool
- Viper
- GPUVerify
- jStar
- NModel
- VerCors
- SpecExplorer
- Jahob
- BAP
- GKLEE
- Traffic 4
- Mechanized Semantic Library
- CFML
- CSPsim
- SymDiff
- YOGI
- Bixie
- Lingva
- FunArray
- Grasshopper
- Joogie
- VERL
- BVD
- DynaMate
- raSAT
- THOR
- coreStar
- SeaHorn
- Atoment
- CoqMT
- c2i
- ExplainHoudini
- Houdini
- Looper
- OpenJML
- Goblint
- HAVOC
- Kilim
- LOCKSMITH
- RELAY
- Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Valigator: A Verification Tool with Bound and Invariant Generation
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Dafny: an automatic program verifier for functional correctness
- Why3 -- where programs meet provers
- Zeno: an automated prover for properties of recursive data structures
- Verification of concurrent systems with VerCors
This page was built for software: Boogie
