Verifying Whiley programs with Boogie
type: Item
instance of: scholarly article
title: Verifying Whiley programs with Boogie
author: David Pearce
author: Mark Utting
author: Lindsay Groves
published in: Journal of Automated Reasoning
publication date: 2022-12-12T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7632091
zbMATH Keywords: Whiley
zbMATH Keywords: Boogie
zbMATH Keywords: verifying compiler
zbMATH Keywords: intermediate verification language
zbMATH Keywords: semantic translation
zbMATH Keywords: impedance mismatch
zbMATH Keywords: flow typing
zbMATH Keywords: verification conditions
describes a project that uses: Whiley
describes a project that uses: Nagini
describes a project that uses: z3
describes a project that uses: Crust
describes a project that uses: RustHorn
describes a project that uses: Frama-C
describes a project that uses: Toolchain
describes a project that uses: CBMC
describes a project that uses: cvc3
describes a project that uses: Caduceus
describes a project that uses: JMLAutoTest
describes a project that uses: Spec#
describes a project that uses: VerCors
describes a project that uses: Eiffel
describes a project that uses: Jahob
describes a project that uses: ACSL
describes a project that uses: Viper
describes a project that uses: Alt-Ergo
describes a project that uses: Boogie
describes a project that uses: KeY
describes a project that uses: OpenJML
describes a project that uses: AutoProof
describes a project that uses: WhyML
describes a project that uses: SMACK
describes a project that uses: GPUVerify
describes a project that uses: VeriFast
describes a project that uses: Chalice
describes a project that uses: VAMPIRE
describes a project that uses: JML
describes a project that uses: Scala
describes a project that uses: JUnit
describes a project that uses: BVD
describes a project that uses: ESC/Java
describes a project that uses: VCC
describes a project that uses: Coq
describes a project that uses: Whiteoak
describes a project that uses: Why3
describes a project that uses: JMLUnit
describes a project that uses: Dafny
describes a project that uses: Korat
describes a project that uses: AstraVer
describes a project that uses: KLEE
describes a project that uses: KRAKATOA
describes a project that uses: SIMPLIFY
describes a project that uses: VeriCool
describes a project that uses: RustBelt
describes a project that uses: Yices
describes a project that uses: Rust
describes a project that uses: SMT-LIB
describes a project that uses: CVC4
describes a project that uses: Joogie
MaRDI profile type: Publication
full work available at URL: s10817-022-09619-1
OpenAlex ID: W4220713823
cites work: Verification of Concurrent Systems with VerCors
cites work: Program Logics for Certified Compilers
cites work: Intersection and union types
cites work: Q4343983
cites work: The vectorization of ITPACK 2C
cites work: Towards verifying nonlinear integer arithmetic
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Q2721096

Verifying Whiley programs with Boogie (cites work)
cites work: Using First-Order Theorem Provers in the Jahob Data Structure Verification System

Verifying Whiley programs with Boogie (cites work)
cites work: Q4808834

Verifying Whiley programs with Boogie (cites work)
cites work: Q3046739

Verifying Whiley programs with Boogie (cites work)
cites work: Experimenting on solving nonlinear integer arithmetic with incremental linearization

Verifying Whiley programs with Boogie (cites work)
cites work: Computer Aided Verification

Verifying Whiley programs with Boogie (cites work)
cites work: Efficient E-Matching for SMT Solvers

Verifying Whiley programs with Boogie (cites work)
cites work: Simplify: a theorem prover for program checking

Verifying Whiley programs with Boogie (cites work)
cites work: Guarded commands, nondeterminacy and formal derivation of programs

Verifying Whiley programs with Boogie (cites work)
cites work: Why3 — Where Programs Meet Provers

Verifying Whiley programs with Boogie (cites work)
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

Verifying Whiley programs with Boogie (cites work)
cites work: The Multiple Assignment Statement

Verifying Whiley programs with Boogie (cites work)
cites work: Q3925859

Verifying Whiley programs with Boogie (cites work)
cites work: Typing Local Control and State Using Flow Analysis

Verifying Whiley programs with Boogie (cites work)
cites work: Programming Languages and Systems

Verifying Whiley programs with Boogie (cites work)
cites work: Q4417801

Verifying Whiley programs with Boogie (cites work)
cites work: Solving Nonlinear Integer Arithmetic with MCSAT

Verifying Whiley programs with Boogie (cites work)
cites work: The dynamic frames theory

Verifying Whiley programs with Boogie (cites work)
cites work: A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic

Verifying Whiley programs with Boogie (cites work)
cites work: How the design of JML accommodates both runtime assertion checking and formal verification

Verifying Whiley programs with Boogie (cites work)
cites work: Efficient weakest preconditions

Verifying Whiley programs with Boogie (cites work)
cites work: Dafny: An Automatic Program Verifier for Functional Correctness

Verifying Whiley programs with Boogie (cites work)
cites work: Automating Induction with an SMT Solver

Verifying Whiley programs with Boogie (cites work)
cites work: A Polymorphic Intermediate Verification Language: Design and Logical Encoding

Verifying Whiley programs with Boogie (cites work)
cites work: Q5447372

Verifying Whiley programs with Boogie (cites work)
cites work: Stepwise refinement of heap-manipulating code in Chalice

Verifying Whiley programs with Boogie (cites work)
cites work: RustHorn: CHC-Based Verification for Rust Programs

Verifying Whiley programs with Boogie (cites work)
cites work: Building High Integrity Applications with SPARK

Verifying Whiley programs with Boogie (cites work)
cites work: Viper: A Verification Infrastructure for Permission-Based Reasoning

Verifying Whiley programs with Boogie (cites work)
cites work: Fast Decision Procedures Based on Congruence Closure

Verifying Whiley programs with Boogie (cites work)
cites work: Fast congruence closure and extensions

Verifying Whiley programs with Boogie (cites work)
cites work: Q4783297

Verifying Whiley programs with Boogie (cites work)
cites work: The Relationship between Separation Logic and Implicit Dynamic Frames

Verifying Whiley programs with Boogie (cites work)
cites work: Sound and Complete Flow Typing with Unions, Intersections and Negations

Verifying Whiley programs with Boogie (cites work)
cites work: Counterexample-guided quantifier instantiation for synthesis in SMT

Verifying Whiley programs with Boogie (cites work)
cites work: Quantifier Instantiation Techniques for Finite Model Finding in SMT

Verifying Whiley programs with Boogie (cites work)
cites work: Formalizing a Hierarchical Structure of Practical Mathematical Reasoning

Verifying Whiley programs with Boogie (cites work)
cites work: Q4808804

Verifying Whiley programs with Boogie (cites work)
cites work: Logical types for untyped languages

Verifying Whiley programs with Boogie (cites work)
cites work: Verifying Whiley programs with Boogie

Verifying Whiley programs with Boogie (cites work)
cites work: JMLUnit: The Next Generation

Verifying Whiley programs with Boogie (DOI)
DOI: 10.1007/S10817-022-09619-1

Verifying Whiley programs with Boogie (Recommended article)
Recommended article: Program verification by coinduction
Similarity Score: 0.84974355
Recommender Run: Recommender Run 3

Verifying Whiley programs with Boogie (Recommended article)
Recommended article: A Vindication of Program Verification
Similarity Score: 0.84699273
Recommender Run: Recommender Run 3

Verifying Whiley programs with Boogie (Recommended article)
Recommended article: Programmable Verifiers in Imperative Programming
Similarity Score: 0.8460107
Recommender Run: Recommender Run 3

Verifying Whiley programs with Boogie (Recommended article)
Recommended article: Q3012541
Similarity Score: 0.84430826
Recommender Run: Recommender Run 3

Verifying Whiley programs with Boogie (Recommended article)
Recommended article: Q2723932
Similarity Score: 0.8427895
Recommender Run: Recommender Run 3