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