Verifying Whiley programs with Boogie
From MaRDI portal
Publication:2102933
DOI10.1007/s10817-022-09619-1MaRDI QIDQ2102933
Mark Utting, Lindsay Groves, David J. Pearce
Publication date: 12 December 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09619-1
semantic translation; verification conditions; Boogie; flow typing; impedance mismatch; intermediate verification language; verifying compiler; Whiley
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Uses Software
- Coq
- Dafny
- JMLUnit
- VAMPIRE
- KRAKATOA
- Eiffel
- SMT-LIB
- ACSL
- Yices
- Why3
- JML
- Spec#
- Caduceus
- Frama-C
- cvc3
- z3
- Alt-Ergo
- KLEE
- SIMPLIFY
- Scala
- ESC/Java
- VCC
- Korat
- JUnit
- Chalice
- VeriFast
- Boogie
- CVC4
- Toolchain
- WhyML
- CBMC
- VeriCool
- KeY
- VerCors
- GPUVerify
- Jahob
- Joogie
- BVD
- Viper
- OpenJML
- SMACK
- AstraVer
- Rust
- AutoProof
- Crust
- Nagini
- Whiley
- RustBelt
- RustHorn
- JMLAutoTest
- Whiteoak