Why3

swMATH4438MaRDI QIDQ16614FDOQ16614

Author name not available (Why is that?)

Described by source

• Why3 — Where Programs Meet Provers

Cited In (only showing first 100 items - show all)

• Tool-Based Verification of a Relational Vertex Coloring Program
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Faster, higher, stronger: E 2.3
• Inferring Loop Invariants Using Postconditions
• From Sets to Bits in Coq
• Imperative Functional Programming with Isabelle/HOL
• Formal verification of a Java component using the RESOLVE framework
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Efficient verification of imperative programs using auto2
• EthVer: formal verification of randomized Ethereum smart contracts
• Faster and more complete extended static checking for the Java modeling language
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Wombit: a portfolio bit-vector solver using word-level propagation
• Automating Induction with an SMT Solver
• Dafny: An Automatic Program Verifier for Functional Correctness
• A Dynamic Logic for Unstructured Programs with Embedded Assertions
• WhyMP, a formally verified arbitrary-precision integer library
• WhyMP, a formally verified arbitrary-precision integer library
• Contract-based verification of MATLAB-style matrix programs
• A set solver for finite set relation algebra
• Tests and proofs for custom data generators
• Hypermap Specification and Certified Linked Implementation Using Orbits
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings
• A Coq library for verification of concurrent programs
• Automated verification of functional correctness of race-free GPU programs
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• A semi-automatic proof of strong connectivity
• How to get an efficient yet verified arbitrary-precision integer library
• Verifying branch-free assembly code in Why3
• Ivor, a Proof Engine
• A framework for the verification of certifying computations
• Automatic decidability and combinability
• Simpler proofs with decentralized invariants
• A program logic for resources
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Building program construction and verification tools from algebraic principles
• One Logic to Use Them All
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Automating deductive verification for weak-memory programs
• Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
• Classification of alignments between concepts of formal mathematical systems
• A non-linear arithmetic procedure for control-command software verification
• Modular inference of subprogram contracts for safety checking
• Polynomial function intervals for floating-point software verification
• Implementing geometric algebra products with binary trees
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Multi-Prover Verification of Floating-Point Programs
• Verification conditions for source-level imperative programs
• Deciding local theory extensions via E-matching
• Secure distributed programming with value-dependent types
• Matching Logic: An Alternative to Hoare/Floyd Logic
• MUNCH - Automated Reasoner for Sets and Multisets
• Expressing Polymorphic Types in a Many-Sorted Language
• Doomed program points
• Reasoning about memory layouts
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• A system for compositional verification of asynchronous objects
• CPBPV: a constraint-programming framework for bounded program verification
• Automating the verification of floating-point programs
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• A generic framework for symbolic execution: a coinductive approach
• SMT proof checking using a logical framework
• A formally verified interpreter for a shell-like programming language
• Matching Logic
• Static Contract Checking with Abstract Interpretation
• Verification of the Schorr-Waite Algorithm – From Trees to Graphs
• Proving fairness and implementation correctness of a microkernel scheduler
• Encoding Monomorphic and Polymorphic Types
• Correct Code Containing Containers
• Hammer for Coq: automation for dependent type theory
• Relational cost analysis in a functional-imperative setting
• TASS: the toolkit for accurate scientific software
• Title not available (Why is that?)
• Title not available (Why is that?)
• The spirit of ghost code
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Hammering towards QED
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Modular Verification of Higher-Order Functional Programs
• An assertional proof of red-black trees using Dafny
• Verifying Whiley programs with Boogie
• Formal verification of side-channel countermeasures using self-composition
• Title not available (Why is that?)
• Practical Realisation and Elimination of an ECC-Related Software Bug Attack
• A Refinement Methodology for Object-Oriented Programs
• Combining Top-Down and Bottom-Up Techniques in Program Derivation
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• TIP: Tools for Inductive Provers
• Invariants Synthesis over a Combined Domain for Automated Program Verification
• Soundly Proving B Method Formulæ Using Typed Sequent Calculus
• LCF-style Platform based on Multiway Decision Graphs
• Deductive verification of floating-point Java programs in KeY
• Assumption propagation through annotated programs
• Making higher-order superposition work
• Hardware-Dependent Proofs of Numerical Programs
• On Formal Specification of Maple Programs
• Towards the Formal Specification and Verification of Maple Programs
• Complete instantiation-based interpolation
• A Generic Intermediate Representation for Verification Condition Generation

This page was built for software: Why3