Balancing the load. Leveraging a semantics stack for systems verification
From MaRDI portal
Publication:835780
DOI10.1007/s10817-009-9123-zzbMath1191.68407OpenAlexW30213274MaRDI QIDQ835780
Artem Starostin, Norbert W. Schirmer, Alexandra Tsyban, Dirk C. Leinenbach, Eyad Alkassar, Mark A. Hillebrand
Publication date: 31 August 2009
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9123-z
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Proving fairness and implementation correctness of a microkernel scheduler, HOL-Boogie -- an interactive prover-backend for the verifying C compiler, Cogent: uniqueness types and certifying compilation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proving fairness and implementation correctness of a microkernel scheduler
- Operating system verification---an overview
- Proving the correctness of client/server software
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Hoare logic and auxiliary variables
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- Integration of a Software Model Checker into Isabelle
- Formal Pervasive Verification of a Paging Mechanism
- Theorem Proving in Higher Order Logics
- Correct Hardware Design and Verification Methods
- Logic for Programming, Artificial Intelligence, and Reasoning
- Types for Proofs and Programs
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Correct Hardware Design and Verification Methods
