IronFleet Verification and Model Checking
Explore the importance of verification and model checking in software development through IronFleet's approach. Learn about the history, techniques, and experiences of ensuring correct software implementation using machine-checked proofs and manual verification. Discover the significance of proof automation and modular handling in IronFleet's processes.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
IronFleet background
Verification History We ve wanted correct software forever. Testing shows the presence, not the absence of bugs [Dijkstra, 1969] If you want more effective programmers, you will discover that they should not waste their time debugging, they should not introduce the bugs to start with. [Dijkstra 1972] Machine-checked proofs require rigorous detail verification used for small proofs,
Model checking: TLC Coq proof assistant Manual proofs
Our experience Techniques Fidelity Model checking: TLC Protocol vs implementation Coq proof assistant Degree of abstraction Manual proofs Mechanical verification
Ironclad Single-machine application Verified for safety Verified to assembly code
Spec: TLA+ (embedded in Dafny) refines Implementation: Dafny (Hoare logic) refines compile link Verifiable assembly verified GC Executable: BoogieX86
Look for... What is proof automation, and why do we care? What new challenges does IronFleet attack? What aspects does IronFleet abandon? Why? In Verdi: how is modularity handled? how is automation achieved?
