On the public citation graph
Timing Analysis of a Protected Operating System Kernel
0 signed · 86 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/11925040_10openalex-snapshot
Static Timing Analysis of Real-Time Operating System Code
inferredcites →https://doi.org/10.1007/s11241-006-9205-5openalex-snapshot
Modeling out-of-order processors for WCET analysis
inferredcites →https://doi.org/10.1016/j.scico.2007.01.014openalex-snapshot
Chronos: A timing analyzer for embedded software
inferredcites →https://doi.org/10.1109/cse.2009.82openalex-snapshot
WCET Analysis of the mC/OS-II Real-Time Kernel
inferredcites →https://doi.org/10.1109/emrts.2001.934029openalex-snapshot
Worst-case execution time analysis of the RTEMS real-time operating system
inferredcites →https://doi.org/10.1109/icess.2009.24openalex-snapshot
A Survey of WCET Analysis of Real-Time Operating Systems
inferredcites →https://doi.org/10.1109/real.1995.495219openalex-snapshot
Efficient microarchitecture modeling and path analysis for real-time software
inferredcites →https://doi.org/10.1109/real.2002.1181568openalex-snapshot
Cost and benefit of separate address spaces in real-time operating systems
inferredcites →https://doi.org/10.1109/rtas.2011.27openalex-snapshot
Scope-Aware Data Cache Analysis for WCET Estimation
inferredcites →https://doi.org/10.1145/1375581.1375603openalex-snapshot
Certifying low-level programs with hardware interrupts and preemptive threads
inferredcites →https://doi.org/10.4230/oasics.wcet.2007.1188openalex-snapshot
Measurements or Static Analysis or Both?
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1002/cpe.4081openalex-snapshot
Studying shadow page cache to improve isolated drivers' performance
inferred← citeshttps://doi.org/10.1007/978-3-030-25543-5_28openalex-snapshot
Integrating Formal Schedulability Analysis into a Verified OS Kernel
inferred← citeshttps://doi.org/10.1007/978-3-030-30446-1_17openalex-snapshot
Efficient Formal Verification for the Linux Kernel
inferred← citeshttps://doi.org/10.1007/978-3-319-02726-5_2openalex-snapshot
VTOS: Research on Methodology of “Light-Weight” Formal Design and Verification for Microkernel OS
inferred← citeshttps://doi.org/10.1007/978-3-319-06410-9_2openalex-snapshot
Proof Engineering Considered Essential
inferred← citeshttps://doi.org/10.1007/978-3-642-38601-5_10openalex-snapshot
Towards a Time-Composable Operating System
inferred← citeshttps://doi.org/10.1007/978-3-662-58096-7_7openalex-snapshot
SWAN: Systemweite statische Laufzeitanalyse echtzeitfähiger Betriebssysteme
inferred← citeshttps://doi.org/10.1007/s11241-017-9286-3openalex-snapshot
High-assurance timing analysis for a high-assurance real-time operating system
inferred← citeshttps://doi.org/10.1007/s11241-024-09419-3openalex-snapshot
Priority-based concurrency and shared resource access mechanisms for nested intercomponent requests in CAmkES
inferred← citeshttps://doi.org/10.1016/j.sysarc.2020.101729openalex-snapshot
A thread synchronization model for the PREEMPT_RT Linux kernel
inferred← citeshttps://doi.org/10.1093/comjnl/bxv035openalex-snapshot
Research on Algorithms to Capture Drivers’ Write Operations
inferred← citeshttps://doi.org/10.1109/etfa.2017.8247611openalex-snapshot
Automata-based modeling of interrupts in the Linux PREEMPT RT kernel
inferred← citeshttps://doi.org/10.1109/hpcc-smartcity-dss.2016.0104openalex-snapshot
Towards Fault-Tolerant Real-Time Scheduling in the seL4 Microkernel
inferred← citeshttps://doi.org/10.1109/iccps54341.2022.00029openalex-snapshot
T-SYS: Timed-Based System Security for Real-Time Kernels
inferred← citeshttps://doi.org/10.1109/icse.2012.6227120openalex-snapshot
Large-scale formal verification in practice: A process perspective
inferred← citeshttps://doi.org/10.1109/milcom52596.2021.9652903openalex-snapshot
vCDS: A Virtualized Cross Domain Solution Architecture
inferred← citeshttps://doi.org/10.1109/rtas.2013.6531083openalex-snapshot
Sequoll: A framework for model checking binaries
inferred← citeshttps://doi.org/10.1109/rtas.2014.6926000openalex-snapshot
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
inferred← citeshttps://doi.org/10.1109/rtas.2016.7461326openalex-snapshot
Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis
inferred← citeshttps://doi.org/10.1109/rtas.2017.37openalex-snapshot
SysWCET: Whole-System Response-Time Analysis for Fixed-Priority Real-Time Systems (Outstanding Paper)
inferred← citeshttps://doi.org/10.1109/rtas.2019.00015openalex-snapshot
Chaos: a System for Criticality-Aware, Multi-Core Coordination
inferred← citeshttps://doi.org/10.1109/rtas.2019.00034openalex-snapshot
Proving Real-Time Capability of Generic Operating Systems by System-Aware Timing Analysis
inferred← citeshttps://doi.org/10.1109/rtas52030.2021.00009openalex-snapshot
Practical Principle of Least Privilege for Secure Embedded Systems
inferred← citeshttps://doi.org/10.1109/rtas54340.2022.00012openalex-snapshot
Compiler-Directed High-Performance Intermittent Computation with Power Failure Immunity
inferred← citeshttps://doi.org/10.1109/rtas54340.2022.00016openalex-snapshot
The Thundering Herd: Amplifying Kernel Interference to Attack Response Times
inferred← citeshttps://doi.org/10.1109/rtas61025.2024.00014openalex-snapshot
Safe and Secure? On the Timing Analysability of Cryptographic Implementations
inferred← citeshttps://doi.org/10.1109/rtas61025.2024.00024openalex-snapshot
Core-Local Reasoning and Predictable Cross-Core Communication with M3
inferred← citeshttps://doi.org/10.1109/rtcsa52859.2021.00018openalex-snapshot
A generic approach for the certified schedulability analysis of software systems
inferred← citeshttps://doi.org/10.1109/rtcsa55878.2022.00007openalex-snapshot
A Concurrency Framework for Priority-Aware Intercomponent Requests in CAmkES on seL4
inferred← citeshttps://doi.org/10.1109/rtss.2012.76openalex-snapshot
Increasing Memory Utilization with Transient Memory Scheduling
inferred← citeshttps://doi.org/10.1109/rtss.2013.21openalex-snapshot
Integrated Timing Analysis of Application and Operating Systems Code
inferred← citeshttps://doi.org/10.1109/rtss62706.2024.00034openalex-snapshot
Interference-free Operating System: A 6 Years’ Experience in Mitigating Cross-Core Interference in Linux
inferred← citeshttps://doi.org/10.1109/rtss66672.2025.00041openalex-snapshot
Dynamic Fuzzing-Based Whole-System Timing Analysis
inferred← citeshttps://doi.org/10.1109/socc58585.2023.10256735openalex-snapshot
A Runtime Security Monitoring Architecture for Embedded Hypervisors
inferred← citeshttps://doi.org/10.1109/sp.2013.35openalex-snapshot
seL4: From General Purpose to a Proof of Information Flow Enforcement
inferred← citeshttps://doi.org/10.1109/trustcom/bigdatase.2019.00014openalex-snapshot
MicroTEE: Designing TEE OS Based on the Microkernel Architecture
inferred← citeshttps://doi.org/10.1145/2168836.2168869openalex-snapshot
Improving interrupt response time in a verifiable protected microkernel
inferred← citeshttps://doi.org/10.1145/2349896.2349904openalex-snapshot
To preempt or not to preempt, that is the question
inferred← citeshttps://doi.org/10.1145/2509136.2509513openalex-snapshot
Code optimizations using formally verified properties
inferred← citeshttps://doi.org/10.1145/2517349openalex-snapshot
Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles
inferred← citeshttps://doi.org/10.1145/2517349.2522720openalex-snapshot
From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
inferred← citeshttps://doi.org/10.1145/2544173.2509513openalex-snapshot
Code optimizations using formally verified properties
inferred← citeshttps://doi.org/10.1145/2544350.2544352openalex-snapshot
Towards a user-mode approach to partitioned scheduling in the seL4 microkernel
inferred← citeshttps://doi.org/10.1145/2560537openalex-snapshot
Comprehensive formal verification of an OS microkernel
inferred← citeshttps://doi.org/10.1145/3126517openalex-snapshot
Formal Verification of a Timing Enforcer Implementation
inferred← citeshttps://doi.org/10.1145/3190508.3190539openalex-snapshot
Scheduling-context capabilities
inferred← citeshttps://doi.org/10.1145/3230627openalex-snapshot
Formally verified software in the real world
inferred← citeshttps://doi.org/10.1145/3277506openalex-snapshot
Efficient Fine-grained Processor-logic Interactions on the Cache-coherent Zynq Platform
inferred← citeshttps://doi.org/10.1145/3371088openalex-snapshot
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation
inferred← citeshttps://doi.org/10.1145/3373400.3373410openalex-snapshot
Modeling the behavior of threads in the PREEMPT_RT Linux kernel using automata
inferred← citeshttps://doi.org/10.1145/3460120.3484782openalex-snapshot
Aion: Enabling Open Systems through Strong Availability Guarantees for Enclaves
inferred← citeshttps://doi.org/10.1145/3461648.3463847openalex-snapshot
Annotate once – analyze anywhere: context-aware WCET analysis by user-defined abstractions
inferred← citeshttps://doi.org/10.1145/3591235openalex-snapshot
Performal: Formal Verification of Latency Properties for Distributed Systems
inferred← citeshttps://doi.org/10.1145/3760387openalex-snapshot
Wasm-IO: Enabling Low-Level Device Interaction in WebAssembly for Industry Automation
inferred← citeshttps://doi.org/10.1145/3765736openalex-snapshot
Virtualization Technology for Dependable Embedded Systems: A Survey for Transportation and Industrial Domains
inferred← citeshttps://doi.org/10.1587/transinf.2024icp0004openalex-snapshot
MicroTEE: Designing and Implementing TEE OS with Rich Trusted Computing Features Based on Microkernel
inferred← citeshttps://doi.org/10.23940/ijpe.19.03.p16.872883openalex-snapshot
Time-Oriented Modeling and Analysis for Real-Time System under Variability
inferred← citeshttps://doi.org/10.26190/unsworks/16384openalex-snapshot
Towards verified microkernels for real-time mixed-criticality systems
inferred← citeshttps://doi.org/10.3389/fbuil.2024.1424721openalex-snapshot
Towards a concurrency platform for scalable multi-axial real-time hybrid simulation
inferred← citeshttps://doi.org/10.48550/arxiv.1808.04239openalex-snapshot
A Spin-based model checking for the simple concurrent program on a preemptive RTOS
inferred← citeshttps://doi.org/10.55162/mcet.05.177openalex-snapshot
Measurement of Kernel Preemption Time of Real Time Operating Systems
inferred← citeshttps://doi.org/10.5555/2685048.2685062openalex-snapshot
Ironclad apps: end-to-end security via automated full-system verification
inferred← citeshttps://doi.org/10.6092/unibo/amsdottorato/6597openalex-snapshot
Operating System Contribution to Composable Timing Behaviour in High-Integrity Real-Time Systems
inferred← citeshttps://doi.org/10.70675/43adeeecz02d3z4c27zab4ez0373161078a9openalex-snapshot
Certified Tools for Schedulability Analyses
inferred← citeshttps://doi.org/10.70675/ff7e6932z2ddaz4ccdza476z5172eb71c091openalex-snapshot
Evaluation of a multiple criticality real-time virtual machine system and configuration of an RTOS's resources allocation techniques
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.