Matches in DBpedia 2016-04 for { <http://dbpedia.org/resource/Verve_(operating_system)> ?p ?o }
Showing triples 1 to 89 of
89
with 100 triples per page.
- Verve_(operating_system) abstract "Verve is a research operating system developed by Microsoft Research. Verve is verified end-to-end for type safety and memory safety.Because of their complexity, a holy grail of software verification has been to verify properties of operating systems. Operating systems are usually written in low-level languages, such as C, that provide very few guarantees. The Singularity project took the approach of writing an operating system in C#, a type-safe, memory-safe language. A weakness of this approach is that operating systems necessarily need to call lower-level code to, for instance, move the stack pointer. Verve addresses this problem by partitioning the operating system into verified assembly that is required to be low-level and a trusted interface to rest of the operating system, written in C#. There is a trusted specification that guarantees the low-level assembly code does not mess with the heap and that the high-level C# code does not mess with the stacks.Verve consists of a small Nucleus, which acts as a minimal hardware abstraction layer, and a Kernel, which uses primitives provided by the Nucleus to expose a more traditional interface to applications. All components of the system other than the Nucleus are written in managed C# and compiled by Bartok (originally developed for the Singularity project) into typed assembly language, which is verified by a TAL checker.The Nucleus implements a memory allocator and garbage collection, support for stack switching, and managing interrupt handlers.It is written in BoogiePL, which serves as input to MSR's Boogie verifier, which proves the Nucleus correct using the Z3 SMT solver. The Nucleus relies on the Kernel to implement threads, scheduling, synchronization, and to provide most interrupt handlers. Even though the Kernel is not formally verified, so, for example, a bug in scheduling could cause the system to hang, it cannot violate type or memory safety, and thus cannot directly cause undefined behavior. If it attempts to make invalid requests to the Nucleus, formal verification guarantees that the Nucleus handles the situation in a controlled manner.Verve's trusted computing base is limited to: Boogie/Z3 for verifying the Nucleus's correctness; BoogieASM for translating it into x86 assembly; the BoogiePL specification of how the Nucleus should behave; the TAL verifier; the assembler and linker; and the bootloader. Notably, neither the C# compiler/runtime nor the Bartok compiler are part of the TCB.".
- Verve_(operating_system) developer Microsoft_Research.
- Verve_(operating_system) latestReleaseDate "2013-11-10".
- Verve_(operating_system) latestReleaseVersion "r73999".
- Verve_(operating_system) programmingLanguage C_Sharp_(programming_language).
- Verve_(operating_system) programmingLanguage Common_Intermediate_Language.
- Verve_(operating_system) status "Under development by Microsoft Research".
- Verve_(operating_system) wikiPageExternalLink fulltext.
- Verve_(operating_system) wikiPageExternalLink fulltext.
- Verve_(operating_system) wikiPageExternalLink Verve-A-Type-Safe-Operating-System.
- Verve_(operating_system) wikiPageExternalLink singularity.
- Verve_(operating_system) wikiPageExternalLink pldi117-yang.pdf.
- Verve_(operating_system) wikiPageExternalLink verve-msft.
- Verve_(operating_system) wikiPageExternalLink Verve_A_Type_Safe_Operating_System.
- Verve_(operating_system) wikiPageID "33809690".
- Verve_(operating_system) wikiPageLength "5167".
- Verve_(operating_system) wikiPageOutDegree "31".
- Verve_(operating_system) wikiPageRevisionID "655380066".
- Verve_(operating_system) wikiPageWikiLink Assembly_language.
- Verve_(operating_system) wikiPageWikiLink Automated_theorem_proving.
- Verve_(operating_system) wikiPageWikiLink BoogiePL.
- Verve_(operating_system) wikiPageWikiLink C++.
- Verve_(operating_system) wikiPageWikiLink C_Sharp_(programming_language).
- Verve_(operating_system) wikiPageWikiLink Category:Microkernel-based_operating_systems.
- Verve_(operating_system) wikiPageWikiLink Category:Microkernels.
- Verve_(operating_system) wikiPageWikiLink Category:Microsoft_Research.
- Verve_(operating_system) wikiPageWikiLink Category:Microsoft_operating_systems.
- Verve_(operating_system) wikiPageWikiLink Category:Nanokernels.
- Verve_(operating_system) wikiPageWikiLink Common_Intermediate_Language.
- Verve_(operating_system) wikiPageWikiLink Formal_verification.
- Verve_(operating_system) wikiPageWikiLink Kernel_panic.
- Verve_(operating_system) wikiPageWikiLink Language-based_system.
- Verve_(operating_system) wikiPageWikiLink Memory_safety.
- Verve_(operating_system) wikiPageWikiLink Microkernel.
- Verve_(operating_system) wikiPageWikiLink Microsoft_Research.
- Verve_(operating_system) wikiPageWikiLink Operating_system.
- Verve_(operating_system) wikiPageWikiLink Satisfiability_modulo_theories.
- Verve_(operating_system) wikiPageWikiLink Shared_source.
- Verve_(operating_system) wikiPageWikiLink Singularity_(operating_system).
- Verve_(operating_system) wikiPageWikiLink Software_verification.
- Verve_(operating_system) wikiPageWikiLink Trusted_computing_base.
- Verve_(operating_system) wikiPageWikiLink Type_safety.
- Verve_(operating_system) wikiPageWikiLink Typed_assembly_language.
- Verve_(operating_system) wikiPageWikiLink X86.
- Verve_(operating_system) wikiPageWikiLinkText "Verve (operating system)".
- Verve_(operating_system) wikiPageWikiLinkText "Verve".
- Verve_(operating_system) developer Microsoft_Research.
- Verve_(operating_system) family Language-based_system.
- Verve_(operating_system) kernelType Language-based_system.
- Verve_(operating_system) kernelType Microkernel.
- Verve_(operating_system) latestReleaseDate "2013-11-10".
- Verve_(operating_system) latestReleaseVersion "r73999".
- Verve_(operating_system) license "Microsoft Research License".
- Verve_(operating_system) name "Verve".
- Verve_(operating_system) progLanguage "C#, other CIL languages".
- Verve_(operating_system) programmedIn "BoogiePL, C#; bootloader in assembly language, C++".
- Verve_(operating_system) sourceModel Shared_source.
- Verve_(operating_system) supportedPlatforms X86.
- Verve_(operating_system) wikiPageUsesTemplate Template:Infobox_OS.
- Verve_(operating_system) wikiPageUsesTemplate Template:Microsoft_Research.
- Verve_(operating_system) wikiPageUsesTemplate Template:Microsoft_operating_systems.
- Verve_(operating_system) wikiPageUsesTemplate Template:Notability.
- Verve_(operating_system) wikiPageUsesTemplate Template:Operating-system-stub.
- Verve_(operating_system) wikiPageUsesTemplate Template:Other_uses_of.
- Verve_(operating_system) wikiPageUsesTemplate Template:Release_date.
- Verve_(operating_system) workingState "Under development by Microsoft Research".
- Verve_(operating_system) subject Category:Microkernel-based_operating_systems.
- Verve_(operating_system) subject Category:Microkernels.
- Verve_(operating_system) subject Category:Microsoft_Research.
- Verve_(operating_system) subject Category:Microsoft_operating_systems.
- Verve_(operating_system) subject Category:Nanokernels.
- Verve_(operating_system) hypernym Research.
- Verve_(operating_system) type Organisation.
- Verve_(operating_system) type Software.
- Verve_(operating_system) type Work.
- Verve_(operating_system) type Division.
- Verve_(operating_system) type Kernel.
- Verve_(operating_system) type CreativeWork.
- Verve_(operating_system) type Thing.
- Verve_(operating_system) type Q386724.
- Verve_(operating_system) type Q7397.
- Verve_(operating_system) comment "Verve is a research operating system developed by Microsoft Research. Verve is verified end-to-end for type safety and memory safety.Because of their complexity, a holy grail of software verification has been to verify properties of operating systems. Operating systems are usually written in low-level languages, such as C, that provide very few guarantees. The Singularity project took the approach of writing an operating system in C#, a type-safe, memory-safe language.".
- Verve_(operating_system) label "Verve (operating system)".
- Verve_(operating_system) sameAs Q7923009.
- Verve_(operating_system) sameAs m.0hhs5fg.
- Verve_(operating_system) sameAs Q7923009.
- Verve_(operating_system) wasDerivedFrom Verve_(operating_system)?oldid=655380066.
- Verve_(operating_system) isPrimaryTopicOf Verve_(operating_system).
- Verve_(operating_system) name "Verve".