The Logic of Software. A Tasting Menu of Formal Methods

I can see clearly now: Clairvoyant Assertions for Deadlock Checking.- When COSTA met KeY: Verified Cost Bounds.- Lifelong Learning of Reactive Systems in Practice.- A Case Study in Information Flow Re nement for Low Level Systems.- Re-CorC-ing KeY: Correct-by-Construction Software Development based on KeY.- Specifying the boundary between unverified and verified code.- Programming legal contracts - a beginners guide to Stipula.- Towards a Modular and Variability-aware Aerodynamic Simulator.- Reasoning about Active Objects: A Sound and Complete Assertional Proof Method.- Improving Automatic Complexity Analysis of Integer Programs.- Alice in Wineland: A Fairy Tale with Contracts.- Teaching Design by Contract using Snap.- On the Notion of Naturalness in Formal Modeling.- The Karlsruhe Java Verification Suite.- Further Lessons from the JML Project.- Inference in MaxSAT and MinSAT.- Implications of Deductive Verification on Research Quality.- Computing in Lukasiewicz logic and AF-algebras.-Speaking about Wine: Another Case Study in Bridging the Gap between Formal and Informal Knowledge.- Software & System Verification with KIV.- A Note on Idleness Detection of Actor Systems.- Symbolic Execution: Foundations, Techniques, Applications, and Future Perspectives.- Locally Abstract Globally Concrete Semantics of Time and Resource Aware Active Objects.- Transparent Treatment of for-Loops in Proofs.