Automatic Data Refinement
From MaRDI portal
Publication:5327338
DOI10.1007/978-3-642-39634-2_9zbMath1317.68216OpenAlexW2206900256MaRDI QIDQ5327338
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_9
Related Items
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, Formalization and Execution of Linear Algebra: From Theorems to Algorithms, A verified ODE solver and the Lorenz attractor, Verified iptables firewall analysis and verification, A verified SAT solver framework with learn, forget, restart, and incrementality, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, CryptHOL: game-based proofs in higher-order logic, Refinement to Imperative/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, Unnamed Item, Refinement to imperative HOL, From LCF to Isabelle/HOL, Probabilistic Functions and Cryptographic Oracles in Higher Order Logic, Efficient verified (UN)SAT certificate checking, Autoref, Continuous and monotone machines, Trustworthy Graph Algorithms (Invited Talk), Formally verified certificate checkers for hardest-to-round computation
Uses Software
