Proving the correctness of client/server software

DOI10.1007/s12046-009-0004-2zbMath1177.68045OpenAlexW2022983134MaRDI QIDQ1040009

Eyad Alkassar, Wolfgang J. Paul, Sebastian Bogan

Publication date: 23 November 2009

Published in: Sādhanā (Search for Journal in Brave)

Full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0145-0191

zbMATH Keywords

software verificationnon-interferenceIsabelle/HOLoperating system correctnessremote procedure callingVerisoft

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Balancing the load. Leveraging a semantics stack for systems verification, Social processes, program verification and all that

Uses Software

• veriSoft

Cites Work

• Unnamed Item
• A new fault-tolerant algorithm for clock synchronization
• A mini challenge: build a verifiable filesystem
• Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification
• Synchronizing clocks in the presence of faults
• Reduction
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Formal Pervasive Verification of a Paging Mechanism
• Logic for Programming, Artificial Intelligence, and Reasoning
• Mechanizing Mathematical Reasoning