Verification, Model Checking, and Abstract Interpretation

5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings

344 Seiten, Taschenbuch

Kurzbeschreibung des Verlags

Tutorial.- Security, Protocols, and Trust.- Security.- Security Types Preserving Compilation.- History-Dependent Scheduling for Cryptographic Processes.- Formal Methods I.- Construction of a Semantic Model for a Typed Assembly Language.- Rule-Based Runtime Verification.- On the Expressive Power of Canonical Abstraction.- Boolean Algebra of Shape Analysis Constraints.- Approximate Probabilistic Model Checking.- Completeness and Complexity of Bounded Model Checking.- Model Checking for Object Specifications in Hidden Algebra.- Formal Methods II.- Model Checking Polygonal Differential Inclusions Using Invariance Kernels.- Checking Interval Based Properties for Reactive Systems.- Widening Operators for Powerset Domains.- Type Inference for Parameterized Race-Free Java.- Certifying Temporal Properties for Compiled C Programs.- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking.- Static Analysis versus Software Model Checking for Bug Finding.- Automatic Inference of Class Invariants.- Liveness with Invisible Ranking.- A Complete Method for the Synthesis of Linear Ranking Functions.- Symbolic Implementation of the Best Transformer.- Formal Methods III.- Constructing Quantified Invariants via Predicate Abstraction.- Analysis of Recursive Game Graphs Using Data Flow Equations.- Applying Jlint to Space Exploration Software.- Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone.- A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal.

• Reihe: Lecture Notes in Computer Science
• Themen: Informatik und Informationstechnologie Informatik Theoretische Informatik
• ISBN: 9783540208037
• Sprache: Englisch
• Erscheinungsdatum: 07.01.2004
• Größe: 235 x 155 mm
• Verlag: Springer
• Herausgegeben von: Giorgio Levi, Bernhard Steffen