On the public citation graph

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation

https://doi.org/10.1145/3371088
0 signed · 48 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.
Claim with ORCID
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.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/11813040_31openalex-snapshot
Formal Verification of a C Compiler Front-End
inferredcites →https://doi.org/10.1007/978-1-4419-1539-9_10openalex-snapshot
Modeling and Security Analysis of a Commercial Real-Time Operating System Kernel
inferredcites →https://doi.org/10.1007/978-3-030-25543-5_28openalex-snapshot
Integrating Formal Schedulability Analysis into a Verified OS Kernel
inferredcites →https://doi.org/10.1007/978-3-319-41540-6_4openalex-snapshot
A Practical Verification Framework for Preemptive OS Kernels
inferredcites →https://doi.org/10.1007/978-3-319-43144-4_4openalex-snapshot
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency
inferredcites →https://doi.org/10.1007/978-3-662-46078-8_48openalex-snapshot
Trustworthy Virtualization of the ARMv7 Memory Subsystem
inferredcites →https://doi.org/10.1007/bfb0028759openalex-snapshot
A machine-checked proof of the optimality of a real-time scheduling policy
inferredcites →https://doi.org/10.1007/s11241-017-9286-3openalex-snapshot
High-assurance timing analysis for a high-assurance real-time operating system
inferredcites →https://doi.org/10.1007/s11704-016-4226-2openalex-snapshot
A survey on formal specification and verification of separation kernels
inferredcites →https://doi.org/10.1007/s12046-009-0002-4openalex-snapshot
Operating system verification—An overview
inferredcites →https://doi.org/10.1109/ecrts.2016.28openalex-snapshot
PROSA: A Case for Readable Mechanized Schedulability Analysis
inferredcites →https://doi.org/10.1109/mc.2016.271openalex-snapshot
Real-Time Computing on Multicore Processors
inferredcites →https://doi.org/10.1109/real.1989.63567openalex-snapshot
The rate monotonic scheduling algorithm: exact characterization and average case behavior
inferredcites →https://doi.org/10.1109/real.2000.896005openalex-snapshot
Formal analysis of the priority ceiling protocol
inferredcites →https://doi.org/10.1109/rtas.2015.7108445openalex-snapshot
Budgeted generalized rate monotonic analysis for the partitioned, yet globally scheduled uniprocessor model
inferredcites →https://doi.org/10.1109/rtss.2005.25openalex-snapshot
Hierarchical Fixed Priority Pre-Emptive Scheduling
inferredcites →https://doi.org/10.1109/rtss.2011.38openalex-snapshot
Timing Analysis of a Protected Operating System Kernel
inferredcites →https://doi.org/10.1109/sp.2013.35openalex-snapshot
seL4: From General Purpose to a Proof of Information Flow Enforcement
inferredcites →https://doi.org/10.1145/1538788.1538814openalex-snapshot
Formal verification of a realistic compiler
inferredcites →https://doi.org/10.1145/1629575.1629596openalex-snapshot
seL4
inferredcites →https://doi.org/10.1145/2491956.2462183openalex-snapshot
Translation validation for a verified OS kernel
inferredcites →https://doi.org/10.1145/2676726.2676975openalex-snapshot
Deep Specifications and Certified Abstraction Layers
inferredcites →https://doi.org/10.1145/2908080.2908100openalex-snapshot
End-to-end verification of information-flow security for C and assembly programs
inferredcites →https://doi.org/10.1145/2908080.2908101openalex-snapshot
Toward compositional verification of interruptible OS kernels and device drivers
inferredcites →https://doi.org/10.1145/3132747.3132748openalex-snapshot
Hyperkernel
inferredcites →https://doi.org/10.1145/3190508.3190539openalex-snapshot
Scheduling-context capabilities
inferredcites →https://doi.org/10.1145/3192366.3192381openalex-snapshot
Certified concurrent abstraction layers
inferredcites →https://doi.org/10.1145/321738.321743openalex-snapshot
Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
inferredcites →https://doi.org/10.1145/3302424.3303976openalex-snapshot
Time Protection
inferredcites →https://doi.org/10.21236/ada211344openalex-snapshot
Scheduling Sporadic and Aperiodic Events in a Hard Real-Time System
inferredcites →https://doi.org/10.4204/eptcs.196.2openalex-snapshot
Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System
inferredcites →https://doi.org/10.5555/1298455.1298481openalex-snapshot
Making information flow explicit in HiStar

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-3-031-27481-7_8openalex-snapshot
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems
inferred← citeshttps://doi.org/10.1007/s12652-021-03454-9openalex-snapshot
Formal design and verification of system task in intelligent transportation systems based on micro-kernel architecture
inferred← citeshttps://doi.org/10.1109/access.2020.3047411openalex-snapshot
Verification of Operating Systems for Internet of Things in Smart Cities From the Assembly Perspective Using Isabelle/HOL
inferred← citeshttps://doi.org/10.1109/rtas54340.2022.00013openalex-snapshot
Jumpstart: Fast Critical Service Resumption for a Partitioning Hypervisor in Embedded Systems
inferred← citeshttps://doi.org/10.1109/rtas68450.2026.00042openalex-snapshot
Scheduling Constraints: A Universal OS Mechanism for Managing Shared Resources
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/rtss66672.2025.00015openalex-snapshot
Partitioning Kernel With Capability Controlled Temporal and Spatial Partitioning
inferred← citeshttps://doi.org/10.1109/tits.2022.3224385openalex-snapshot
A Formal Approach to Design and Security Verification of Operating Systems for Intelligent Transportation Systems Based on Object Model
inferred← citeshttps://doi.org/10.1145/3477013openalex-snapshot
Towards an Integrated Vehicle Management System in DriveOS
inferred← citeshttps://doi.org/10.1145/3477132.3483560openalex-snapshot
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware
inferred← citeshttps://doi.org/10.1145/3498703openalex-snapshot
Layered and object-based game semantics
inferred← citeshttps://doi.org/10.1145/3563290openalex-snapshot
Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
inferred← citeshttps://doi.org/10.1145/3609703.3609714openalex-snapshot
Survey of the Formal Verification of Operating Systems in Power Monitoring System
inferred← citeshttps://doi.org/10.1145/3729249openalex-snapshot
RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers
inferred← citeshttps://doi.org/10.1145/3779212.3790171openalex-snapshot
Highly Automated Verification of Security Properties for Unmodified System Software
inferred← citeshttps://doi.org/10.70675/43adeeecz02d3z4c27zab4ez0373161078a9openalex-snapshot
Certified Tools for Schedulability Analyses
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.