Why3 - Where Programs Meet Provers

No abstract is available for this paper.

• Publication year

  2013

• Venue

  European Symposium on Programming

• Publication date

  2013-03-16

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-37036-6_8
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Formal Methods for Components and Objects: 10th International Symposium FMCO 2011, revised selected papers

  2012cited by this paper
• Expressing Polymorphic Types in a Many-Sorted Language

  2011cited by this paper
• Why3: Shepherd Your Herd of Provers

  2011cited by this paper
• Why Hi-Lite Ada?

  2011cited by this paper
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs

  2005cited by this paper
• Fast Pattern Matching in Strings

  1977cited by this paper

• Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic

  2026cites this paper
• Design of Safe C Language for Program Verification

  2026cites this paper
• Automated Theorem Proving for Prolog Verification

  2026cites this paper
• Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles

  2026cites this paper
• Type Congruence, Duality and Iso-Recursive Binary Session Types

  2026cites this paper
• Verifying Floating-Point Programs in Stainless

  2026cites this paper
• Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

  2026cites this paper
• RustyDL: A Program Logic for Rust

  2026cites this paper
• A Recipe for Modular Verification of Generic Tree Traversals

  2026cites this paper
• Weakening Goals in Logical Specifications

  2025cites this paper
• Forall-Exists Relational Verification by Filtering to Forall-Forall

  2025cites this paper
• Heterogeneous Dynamic Logic: Provability Modulo Program Theories

  2025cites this paper
• Towards Richer Challenge Problems for Scientific Computing Correctness

  2025cites this paper
• Internal and External Performance Fuzzing of Well-Defined Constraints for the B Method

  2025cites this paper
• coma, an Intermediate Verification Language with Explicit Abstraction Barriers

  2025cites this paper
• Neural Network Verification is a Programming Language Challenge

  2025cites this paper
• SMT-Based Automation for Overwhelming Truth

  2025cites this paper
• Safe-ROS: An Architecture for Autonomous Robots in Safety-Critical Domains

  2025cites this paper
• Automated SysML v2 System Model to Memory-Safe Language Code Generation for Avionics Applications

  2025cites this paper
• Usability Barriers for Liquid Types

  2025cites this paper
• Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM

  2025cites this paper
• Proof Scores: A Survey

  2025cites this paper
• Static Coverage in Deductive Software Verification

  2025cites this paper
• Construction of verifier combinations from off-the-shelf components

  2025cites this paper
• Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

  2025cites this paper
• Generic Refinement Types

  2025cites this paper
• Automatic Inference of Synchronous Regular Invariants

  2025cites this paper
• A Framework for Hybrid Set-Theoretic and Numerical Problem Solving

  2025cites this paper
• Fifteen Years of Viper

  2025cites this paper
• Logika: the Sireum verification framework

  2025cites this paper
• FO-Complete Program Verification for Heap Logics

  2025influential citation
• Agentic Specification Generator for Move Programs

  2025cites this paper
• Interactive Bitvector Reasoning using Verified Bit-Blasting

  2025cites this paper
• First-Class Verification Dialects for MLIR

  2025cites this paper
• Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust

  2025cites this paper
• Compositional Symbolic Execution for the Next 700 Memory Models

  2025cites this paper
• Try-Mopsa: Relational Static Analysis in Your Pocket

  2025cites this paper
• Refinement-Types Driven Development: A study

  2025cites this paper
• SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks

  2025cites this paper
• Thrust: A Prophecy-Based Refinement Type System for Rust

  2025cites this paper
• Inferring multiple helper Dafny assertions with LLMs

  2025cites this paper
• Reducing Hallucinations in LLM-Generated Code via Semantic Triangulation

  2025cites this paper
• Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic

  2025cites this paper
• Raven: An SMT-Based Concurrency Verifier

  2025cites this paper
• Accelerating Automated Program Verifiers by Automatic Proof Localization

  2025cites this paper
• C*: Unifying Programming and Verification in C

  2025cites this paper
• Iso-Recursive Multiparty Sessions and their Automated Verification - Technical Report

  2025influential citation
• MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

  2025cites this paper
• Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities

  2025cites this paper
• Tunable Automation in Automated Program Verification

  2025cites this paper
• What Challenges Do Developers Face When Using Verification-Aware Programming Languages?

  2025cites this paper
• Verified VCG and Verified Compiler for Dafny

  2025cites this paper
• Detecting speculative data flow vulnerabilities using weakest precondition reasoning

  2025cites this paper
• A Proof-Producing Compiler for Blockchain Applications

  2025cites this paper
• Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics

  2025cites this paper
• Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml

  2025cites this paper
• Condition Sequence Coverage Criterion and Automatic Test Case Generation for Testing-Based Formal Verification

  2025cites this paper
• The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification

  2025cites this paper
• iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns

  2024cites this paper
• Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly

  2024cites this paper
• Dependent Ghosts Have a Reflection for Free

  2024cites this paper
• Formal Foundations for Translational Separation Logic Verifiers

  2024cites this paper
• Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report)

  2024cites this paper
• Inductive Predicate Synthesis Modulo Programs (Extended)

  2024cites this paper
• Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language

  2024cites this paper
• Certification of Tail Recursive Bubble-Sort in Theorema and Coq

  2024cites this paper
• On SMT Theory Design: The Case of Sequences

  2024cites this paper
• Automatic Bit- and Memory-Precise Verification of eBPF Code

  2024cites this paper
• StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs

  2024influential citation
• Verification Algorithms for Automated Separation Logic Verifiers

  2024cites this paper
• Verifying Functional Correctness Properties at the Level of Java Bytecode

  2024cites this paper
• Hypra: A Deductive Program Verifier for Hyper Hoare Logic

  2024cites this paper
• Laurel: Unblocking Automated Verification with Large Language Models

  2024cites this paper
• From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert

  2024cites this paper
• A comprehensive survey of smart contract security: State of the art and research directions

  2024cites this paper
• Co-Developing Programs and Their Proof of Correctness

  2024cites this paper
• Saturating Sorting without Sorts

  2024cites this paper
• Formally Verifying an Efficient Sorter

  2024cites this paper
• Practical Deductive Verification of OCaml Programs

  2024cites this paper
• Verifying Solutions to Semantics-Guided Synthesis Problems

  2024cites this paper
• A Formalization of Core Why3 in Coq

  2024influential citation
• Real-Time Monitoring and Trace Based on Nested COBS

  2024cites this paper
• Reasoning About Exceptional Behavior At the Level of Java Bytecode with ByteBack

  2024cites this paper
• Certification of Insert-Sort and Merge-Sort in Coq

  2024cites this paper
• Deductive Verification of Sparse Sets in Why3

  2024cites this paper
• Extending DRAT to SMT

  2024cites this paper
• Reasoning about Interior Mutability in Rust using Library-Defined Capabilities

  2024cites this paper
• Fuzzing Processing Pipelines for Zero-Knowledge Circuits

  2024cites this paper
• Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation

  2024cites this paper
• Translating meaning representations to behavioural interface specifications

  2024cites this paper
• Comparing EventB, log and Why3 Models of Sparse Sets

  2023cites this paper
• A Toolkit for Automated Testing of Dafny

  2023cites this paper
• A Dafny-based approach to thread-local information flow analysis

  2023cites this paper
• Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation

  2023cites this paper
• Finding Specification Blind Spots via Fuzz Testing

  2023cites this paper
• Efficient computation of arbitrary control dependencies

  2023cites this paper
• Automatic Benchmark Generation for Object Constraint Language

  2023cites this paper
• Mostly Automated Proof Repair for Verified Libraries

  2023cites this paper
• Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

  2023cites this paper
• Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY

  2023cites this paper