Verifying Whiley programs with Boogie
From MaRDI portal
Publication:2102933
Recommendations
Cites work
- scientific article; zbMATH DE number 1612488 (Why is no real title available?)
- scientific article; zbMATH DE number 2089386 (Why is no real title available?)
- scientific article; zbMATH DE number 3740740 (Why is no real title available?)
- scientific article; zbMATH DE number 1031980 (Why is no real title available?)
- scientific article; zbMATH DE number 1956470 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- scientific article; zbMATH DE number 2090113 (Why is no real title available?)
- scientific article; zbMATH DE number 2090142 (Why is no real title available?)
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- A polymorphic intermediate verification language: design and logical encoding
- A verifying compiler for a multi-threaded object-oriented language
- Automating Induction with an SMT Solver
- Building high integrity applications with SPARK
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computer Aided Verification
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Dafny: an automatic program verifier for functional correctness
- Efficient E-Matching for SMT Solvers
- Efficient weakest preconditions
- Experimenting on solving nonlinear integer arithmetic with incremental linearization
- Fast Decision Procedures Based on Congruence Closure
- Fast congruence closure and extensions
- Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
- Guarded commands, nondeterminacy and formal derivation of programs
- How the design of JML accommodates both runtime assertion checking and formal verification
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Intersection and union types
- JMLUnit: the next generation
- Logical types for untyped languages
- Program logics for certified compilers
- Programming Languages and Systems
- Quantifier instantiation techniques for finite model finding in SMT
- RustHorn: CHC-based verification for Rust programs
- Simplify: a theorem prover for program checking
- Solving nonlinear integer arithmetic with MCSAT
- Sound and complete flow typing with unions, intersections and negations
- Stepwise refinement of heap-manipulating code in Chalice
- The Multiple Assignment Statement
- The dynamic frames theory
- The relationship between separation logic and implicit dynamic frames
- The vectorization of ITPACK 2C
- Typing local control and state using flow analysis
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Verification of concurrent systems with VerCors
- Verifying Whiley programs with Boogie
- Viper: a verification infrastructure for permission-based reasoning
- Why3 -- where programs meet provers
Cited in
(5)- Verifying Whiley programs with Boogie
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Leveraging compiler intermediate representation for multi- and cross-language verification
- A polymorphic intermediate verification language: design and logical encoding
Describes a project that uses
Uses Software
- RustHorn
- RustBelt
- Whiteoak
- JMLAutoTest
- Whiley
- Nagini
- Crust
- AutoProof
- Rust
- AstraVer
- SMACK
- OpenJML
- Viper
- BVD
- Joogie
- Jahob
- GPUVerify
- VerCors
- KeY
- VeriCool
- CBMC
- WhyML
- Toolchain
- CVC4
- Boogie
- VeriFast
- Chalice
- JUnit
- Korat
- VCC
- ESC/Java
- Scala
- SIMPLIFY
- KLEE
- Alt-Ergo
- z3
- cvc3
- Frama-C
- Caduceus
- Spec#
- JML
- Why3
- Yices
- ACSL
- SMT-LIB
- Eiffel
- KRAKATOA
- VAMPIRE
- JMLUnit
- Dafny
- Coq
This page was built for publication: Verifying Whiley programs with Boogie
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102933)
