Cited in
(only showing first 100 items - show all)- An assertional proof of the stability and correctness of Natural Mergesort
- A Coq formalization of the relational data model
- An assertional proof of red-black trees using Dafny
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Tool-Based Verification of a Relational Vertex Coloring Program
- Faster, higher, stronger: E 2.3
- Inferring Loop Invariants Using Postconditions
- Verifying Whiley programs with Boogie
- Formal verification of a Java component using the RESOLVE framework
- Product programs in the wild: retrofitting program verifiers to check information flow security
- From Sets to Bits in Coq
- Efficient verification of imperative programs using auto2
- Imperative Functional Programming with Isabelle/HOL
- EthVer: formal verification of randomized Ethereum smart contracts
- Formal verification of side-channel countermeasures using self-composition
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Towards the formal specification and verification of Maple programs
- On formal specification of Maple programs
- Wombit: a portfolio bit-vector solver using word-level propagation
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Automating Induction with an SMT Solver
- A formally proved, complete algorithm for path resolution with symbolic links
- Contract-based verification of MATLAB-style matrix programs
- A set solver for finite set relation algebra
- Tests and proofs for custom data generators
- WhyMP, a formally verified arbitrary-precision integer library
- WhyMP, a formally verified arbitrary-precision integer library
- Deductive verification of floating-point Java programs in KeY
- Automating theorem proving with SMT
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- LCF-style Platform based on Multiway Decision Graphs
- Automated verification of functional correctness of race-free GPU programs
- 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
- 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
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A framework for the verification of certifying computations
- Ivor, a Proof Engine
- Viper: a verification infrastructure for permission-based reasoning
- Assumption propagation through annotated programs
- Matching logic: an alternative to Hoare/Floyd logic
- Matching logic
- Automatic decidability and combinability
- Simpler proofs with decentralized invariants
- A program logic for resources
- Building program construction and verification tools from algebraic principles
- Expressing polymorphic types in a many-sorted language
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Making higher-order superposition work
- Combining top-down and bottom-up techniques in program derivation
- Hardware-Dependent Proofs of Numerical Programs
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Automating deductive verification for weak-memory programs
- Complete instantiation-based interpolation
- 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
- Modular inference of subprogram contracts for safety checking
- A non-linear arithmetic procedure for control-command software verification
- Instrumenting a weakest precondition calculus for counterexample generation
- Reasoning about assignments in recursive data structures
- Automated verification of the parallel Bellman-Ford algorithm
- Verifying the conversion into CNF in dafny
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Polynomial function intervals for floating-point software verification
- Apron
- ACL2
- Cocktail
- Coq
- CPBPV
- Dafny
- HOL-Boogie
- KeY-C
- RelView
- Alloy
- COMBINE
- IMP++
- RealLib
- TVOC
- KRAKATOA
- SPARK
- Eiffel
- ACSL
- Daikon
- distcc
- Caduceus
- JML
- Frama-C
- Omnibus
- Alt-Ergo
- cvc3
- Gappa
- ISP
- Spec#
- core 2
- SIMPLIFY
- Netsoft
- TASS_
This page was built for software: Why3
