Call for Presentations
The seL4 Summit gathers the seL4 community to learn, share and connect. The program committee solicits talks on a wide range of seL4-related topics, as well as lightning talks on seL4 deployment.
Important Dates
- Abstracts due:
21 April 20252 May 2025 - Notification of decisions: 6 June 2025
- Summit: 3 - 5 September 2025
Overview
The seL4 Summit aims at gathering the seL4 community to learn, share, and connect:
- learn about the seL4 technology, its latest progress, use, successes, challenges, plans;
- share exciting seL4 development, research, experience, applications in the real world;
- connect with other seL4 developers, users, providers, supporters, potential partners, and enthusiasts.
The seL4 Summit covers the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people.
The seL4 Summit 2025 will be in Prague, Czech Republic.
Topics
The Program Committee solicits proposals on any seL4-related topic, in particular in the areas of:
-
seL4 on-going and planned R&D, mature or early stage:
- seL4 research efforts
- seL4 development efforts
- work-in-progress seL4 development
- student work on seL4
- new/missing/next-gen kernel mechanisms
- seL4-related roadmaps: what you plan to work on and when
- seL4 grand challenges
- OS frameworks and services
- seL4 userland with programming language support beyond C
- high performance systems based on seL4: pushing the boundaries
- early work/new ideas/initial experiments with seL4
-
seL4 experience reports
- experience with deploying seL4 in the field, in commercial/deployed products
- experience with teaching seL4
- experience with seL4 in certification schemes and application of industry standards
- experience with “building a business case for using a verified kernel”
- experience with porting software from other OSes
-
seL4 and hardware
- ports to new hardware platforms or architectures
- multicore systems
- virtualisation
- new/proposed hardware features or architectures, which could also enable or broaden the scope of formal reasoning (e.g. about time protection)
- seL4 in embedded processors on FPGAs, and impact of assured separation
- IOMMU solutions for various hardware architectures and impact for seL4
- device driver development, porting, reuse, frameworks, verification
-
seL4 and assurance:
- application-level verification leveraging seL4 proofs
- correctness, spatial separation, temporal separation, and real-time proofs
- formalised interface between or composition of kernel-level proofs and user-level proofs
- verification engineering at scale, scaling verification productivity
- security/safety impact/assurance/certification for an seL4-based system
Submissions
If you would like to propose a talk, please upload an abstract of
one page or less for your proposed talk by 21
April 2025 2 May 2025 on the submission
portal. Abstracts should indicate why the talk fits the scope
of the seL4 Summit. Notifications of accepted presentations will be made
by 6 June 2025.
If you'd love to hear about some specific work from other people in the community, we encourage you to reach out to them to incite them to submit a proposal. :-) Alternatively, let us know at summit@sel4.systems.
seL4 Deployment
Open invitation for a 5-minute slot to talk about your seL4 deployment
The community loves to hear about the deployment of seL4. So, if you:
- are selling an end-user product that has seL4 embedded within, or
- have integrated an seL4-based system/component into a deployed system,
you are welcome to a 5-min slot at the summit to talk about it, regardless of whether you are submitting an
abstract
for a full presentation. Simply send a short description by email to summit@sel4.systems by 21 April 2025 2 May 2025.
Contact
If you have questions, please do not hesitate to contact the seL4 Foundation summit team at summit@sel4.systems.