seL4

swMATH15222MaRDI QIDQ27113FDOQ27113

Author name not available (Why is that?)

Official website: http://dl.acm.org/citation.cfm?id=1629596

Described by source

• Experience report: seL4, formally verifying a high-performance microkernel

Cited In (only showing first 100 items - show all)

• A synthesis of the procedural and declarative styles of interactive theorem proving
• Title not available (Why is that?)
• GeneSyst
• MizarMode
• Isabelle/jEdit
• PIDE
• HOL-Omega
• Limmat
• Rodin
• VCC
• CompCertTSO
• LCF
• CakeML
• FABRIK
• CERES
• CertiCrypt
• TRX
• DESUMA
• GIDDES
• CompCert
• Toolchain
• PhoX
• VeriSmall
• Paco
• Nighthawk
• SPARK Pro
• Poly/ML
• Coquelicot
• Locales
• BAP
• Ynot
• Eisbach
• Mtac
• ConfiChair
• Rtac
• QuickChick
• FreeRTOS
• Vellvm
• VeriML
• TCT
• Yampa
• CodeSonar
• Jif
• Klockwork
• NAT2TEST
• CoSMed
• EXPLODE
• Ur/Web
• Cogent
• HALO
• Matrix Operations
• ARMor
• AUSPICE-R
• Coverity
• Caper
• Infer
• Lifting
• Delphin
• CertiKOS
• BoogiePL
• Complx
• Transfer
• Teyjus
• CertiCoq
• Charge!
• CSimpl
• EROS
• GRASShopper
• kepler98
• ModelPlex
• GitLab
• DeltaJ
• JBMC
• DarwinSPL
• DeltaEcore
• Klocwork
• JOANA
• SCCharts
• SCEst
• Gallina
• Coinductive
• Cayley-Hamilton
• Echelon Form
• Barrelfish
• Gauss-Jordan
• Graph Theory
• CAVA LTL Modelchecker
• Kami
• QR Decomposition
• List Update Algorithms
• Piton
• Jinja not Java
• Coccinelle
• JSetL
• Tame Graphs
• Rank Nullity
• Maximum Cardinality Matching
• Isabelle/DOF
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code

This page was built for software: seL4