Verification, Model Checking, and Abstract Interpretation

Abstract Interpretation of Non-monotone Bi-inductive Semantic Definitions.- CTL as an Intermediate Language.- Multi-valued Logics, Automata, Simulations, and Games.- Verification of Register Allocators.- Program Analysis and Programming Languages for Security.- An Improved Tight Closure Algorithm for Integer Octagonal Constraints.- Handling Parameterized Systems with Non-atomic Global Conditions.- Abstract Interpretation of the Physical Inputs of Embedded Programs.- Diagnostic Information for Realizability.- Approximation Refinement for Interpolation-Based Model Checking.- Abstract Interpretation of Cellular Signalling Networks.- Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?.- Model Checking for Action Abstraction.- On Bridging Simulation and Formal Verification.- Extending Model Checking with Dynamic Analysis.- Deriving Bisimulations by Simplifying Partitions.- Precise Set Sharing Analysis for Java-Style Programs.- Sufficient Preconditions for Modular Assertion Checking.- Runtime Checking for Separation Logic.- Decision Procedures for Multisets with Cardinality Constraints.- All You Need Is Compassion.- A Forward-Backward Abstraction Refinement Algorithm.- Internal and External Logics of Abstract Interpretations.- From LTL to Symbolically Represented Deterministic Automata.- Monitoring Temporal Properties of Stochastic Systems.- A Hybrid Algorithm for LTL Games.