Explore
From Formal Semantics to Verified Slicing
Daniel Wasserrab
2011
0 Ungluers have
Faved this Work
Login to Fave
This book presents a modular framework for slicing in the proof assistant Isabelle/HOL which is based on abstract control flow graphs. Building on such abstract structures renders the correctness results language-independent. To prove that they hold for a specific language, it remains to instantiate the framework with this language, which requires a formal semantics of this language in Isabelle/HOL. We show that formal semantics even for sophisticated high-level languages are realizable.
This book is included in DOAB.
Why read this book? Have your say.
You must be logged in to comment.
Rights Information
Are you the author or publisher of this work? If so, you can claim it as yours by registering as an Unglue.it rights holder.Downloads
This work has been downloaded 40 times via unglue.it ebook links.
- 40 - pdf (CC BY-NC-ND) at Unglue.it.
Keywords
- formal semantics
- Language Based Security
- modularity
- Slicing
- theorem proving