Verifying Whiley programs with Boogie
From MaRDI portal
Publication:2102933
DOI10.1007/S10817-022-09619-1OpenAlexW4220713823MaRDI QIDQ2102933FDOQ2102933
Mark Utting, David Pearce, Lindsay Groves
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
Recommendations
semantic translationverification conditionsBoogieflow typingimpedance mismatchintermediate verification languageverifying compilerWhiley
Cites Work
- Automating Induction with an SMT Solver
- Dafny: An Automatic Program Verifier for Functional Correctness
- JMLUnit: The Next Generation
- Title not available (Why is that?)
- Simplify: a theorem prover for program checking
- Why3 — Where Programs Meet Provers
- Computer Aided Verification
- Verification of Concurrent Systems with VerCors
- The vectorization of ITPACK 2C
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Efficient E-Matching for SMT Solvers
- Title not available (Why is that?)
- Quantifier Instantiation Techniques for Finite Model Finding in SMT
- Title not available (Why is that?)
- Fast Decision Procedures Based on Congruence Closure
- Guarded commands, nondeterminacy and formal derivation of programs
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Efficient weakest preconditions
- Title not available (Why is that?)
- Title not available (Why is that?)
- The dynamic frames theory
- Title not available (Why is that?)
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
- Solving Nonlinear Integer Arithmetic with MCSAT
- Program Logics for Certified Compilers
- Fast congruence closure and extensions
- How the design of JML accommodates both runtime assertion checking and formal verification
- The Multiple Assignment Statement
- Programming Languages and Systems
- Intersection and union types
- Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
- Building High Integrity Applications with SPARK
- Experimenting on solving nonlinear integer arithmetic with incremental linearization
- A verifying compiler for a multi-threaded object-oriented language
- Stepwise refinement of heap-manipulating code in Chalice
- Title not available (Why is that?)
- Verifying Whiley programs with Boogie
- Towards verifying nonlinear integer arithmetic
- Sound and Complete Flow Typing with Unions, Intersections and Negations
- Typing Local Control and State Using Flow Analysis
- The Relationship between Separation Logic and Implicit Dynamic Frames
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- Title not available (Why is that?)
- RustHorn: CHC-Based Verification for Rust Programs
- Logical types for untyped languages
Cited In (1)
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
- JMLAutoTest
- Whiteoak
- RustBelt
- RustHorn
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)
