Verification, Model Checking, and Abstract Interpretation

Inhaltsverzeichnis

• Closure Operators for ROBDDs.
• A CLP Method for Compositional and Intermittent Predicate Abstraction.
• Combining Shape Analyses by Intersecting Abstractions.
• A Complete Abstract Interpretation Framework for Coverability Properties of WSTS.
• Complexity Results on Branching-Time Pushdown Model Checking.
• A Compositional Logic for Control Flow.
• Detecting Non-cyclicity by Abstract Compilation into Boolean Functions.
• Efficient Strongly Relational Polyhedral Analysis.
• Environment Abstraction for Parameterized Verification.
• Error Control for Probabilistic Model Checking.
• Field Constraint Analysis.
• A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety.
• Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems.
• A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs.
• Monitoring Off-the-Shelf Components.
• Parallel External Directed Model Checking with Linear I/O.
• Piecewise FIFO Channels Are Analyzable.
• Ranking Abstraction of Recursive Programs.
• Relative Safety.
• Resource Usage Analysis for the ?-Calculus.
• Semantic Hierarchy Refactoring by Abstract Interpretation.
• Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation.
• Symbolic Methods to Enhance the Precision of Numerical Abstract Domains.
• Synthesis of Reactive(1) Designs.
• Systematic Construction of Abstractions for Model-Checking.
• Totally Clairvoyant Scheduling with Relative Timing Constraints.
• Verification of Well-Formed Communicating Recursive State Machines.
• What’s Decidable About Arrays?.