Verification, model checking, and abstract interpretation

InhaltsverzeichnisAbstract 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.