Pages that link to "Item:Q5326280"
From MaRDI portal
The following pages link to Why3 — Where Programs Meet Provers (Q5326280):
Displaying 41 items.
- Why3 (Q16614) (← links)
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Polynomial function intervals for floating-point software verification (Q457251) (← links)
- A generic framework for symbolic execution: a coinductive approach (Q507361) (← links)
- The spirit of ghost code (Q518394) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Formal verification of a Java component using the RESOLVE framework (Q831953) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- The matrix reproved (verification pearl) (Q1703015) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- An automated deductive verification framework for circuit-building quantum programs (Q2233453) (← links)
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages (Q2237340) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- Assumption propagation through annotated programs (Q2628303) (← links)
- EthVer: formal verification of randomized Ethereum smart contracts (Q2670859) (← links)
- WhyMP, a formally verified arbitrary-precision integer library (Q2673999) (← links)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
- Proving Reachability-Logic Formulas Incrementally (Q2827839) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- Modular Verification of Higher-Order Functional Programs (Q2988670) (← links)
- Relational cost analysis in a functional-imperative setting (Q5020903) (← links)
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses (Q5038461) (← links)
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses (Q5098716) (← links)
- (Q5130751) (← links)
- (Q5195286) (← links)
- An Assertional Proof of the Stability and Correctness of Natural Mergesort (Q5277907) (← links)
- A Generic Intermediate Representation for Verification Condition Generation (Q5743596) (← links)
- Combining Top-Down and Bottom-Up Techniques in Program Derivation (Q5743597) (← links)
- (Q5875432) (← links)
- Making higher-order superposition work (Q5918403) (← links)
- Making higher-order superposition work (Q5918575) (← links)
- Analysis and Transformation of Constrained Horn Clauses for Program Verification (Q6063893) (← links)
- A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3 (Q6156936) (← links)
- Efficient computation of arbitrary control dependencies (Q6165552) (← links)
- Integrating ADTs in KeY and their application to history-based reasoning about collection (Q6185826) (← links)
