Wolfgang Reif

Latest

• Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems
• Adding Concurrency to a Sequential Refinement Tower
• A Relational Encoding for a Clash-Free Subset of ASMs
• Development of a Verified Flash File System
• Modular Refinement for Submachines of ASMs