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
• 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
• 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
• Viper: a verification infrastructure for permission-based reasoning
• Matching logic
• Matching logic: an alternative to Hoare/Floyd logic
• Automatic decidability and combinability
• Simpler proofs with decentralized invariants
• A program logic for resources
• Expressing polymorphic types in a many-sorted language
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Building program construction and verification tools from algebraic principles
• 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
• Static contract checking with abstract interpretation
• Verification conditions for source-level imperative programs
• Deciding local theory extensions via E-matching
• Correct code containing containers
• Encoding monomorphic and polymorphic types
• Secure distributed programming with value-dependent types
• 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
• Modular verification of higher-order functional programs
• 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
• Multi-prover verification of floating-point programs
• One logic to use them all
• A formally verified interpreter for a shell-like programming language
• Proving fairness and implementation correctness of a microkernel scheduler
• Dafny: an automatic program verifier for functional correctness
• MUNCH -- automated reasoner for sets and multisets
• A dynamic logic for unstructured programs with embedded assertions
• Hammer for Coq: automation for dependent type theory
• Relational cost analysis in a functional-imperative setting
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• 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
• Hypermap specification and certified linked implementation using orbits
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• An assertional proof of red-black trees using Dafny
• Verifying Whiley programs with Boogie
• Formal verification of side-channel countermeasures using self-composition
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Towards the formal specification and verification of Maple programs
• On formal specification of Maple programs
• A formally proved, complete algorithm for path resolution with symbolic links
• Automating theorem proving with SMT
• 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
• Combining top-down and bottom-up techniques in program derivation
• Hardware-Dependent Proofs of Numerical Programs
• Complete instantiation-based interpolation
• Instrumenting a weakest precondition calculus for counterexample generation
• Reasoning about assignments in recursive data structures
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Automated verification of the parallel Bellman-Ford algorithm
• Verifying the conversion into CNF in dafny

This page was built for software: Why3