Pages that link to "Item:Q1600086"
From MaRDI portal
The following pages link to Isabelle/HOL. A proof assistant for higher-order logic (Q1600086):
Displaying 50 items.
- Relational bytecode correlations (Q710672) (← links)
- Frame rule for mutually recursive procedures manipulating pointers (Q732009) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Optimising the ProB model checker for B using partial order reduction (Q736463) (← links)
- An operational semantics for object-oriented concepts based on the class hierarchy (Q736789) (← links)
- Test-data generation for control coverage by proof (Q736805) (← links)
- Analysis of a clock synchronization protocol for wireless sensor networks (Q764293) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- Formalization and implementation of modern SAT solvers (Q839035) (← links)
- Cones and foci: A mechanical framework for protocol verification (Q853730) (← links)
- Mathematical method and proof (Q857692) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- Verifying the SET purchase protocols (Q861698) (← links)
- Formal analysis of multiparty contract signing (Q861699) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Security types preserving compilation (Q865705) (← links)
- Verifying a signature architecture: a comparative case study (Q877156) (← links)
- Verification of FPGA layout generators in higher-order logic (Q877830) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- The axiomatization of override and update (Q975885) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- HasCasl: integrated higher-order specification and program development (Q1006648) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- The RISC ProofNavigator: a proving assistant for program verification in the classroom (Q1019024) (← links)
- Don't care words with an application to the automata-based approach for real addition (Q1028730) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Inductive proof search modulo (Q1037404) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- Nominal unification with atom-variables (Q1640638) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Verified iptables firewall analysis and verification (Q1663231) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
