Steffen / Levi Verification, Model Checking, and Abstract Interpretation

5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings
Erscheinungsjahr 2003
ISBN: 978-3-540-24622-0
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 2937, 325 Seiten, eBook

Reihe: Lecture Notes in Computer Science

Zielgruppe

Research

Autoren/Hrsg.

Steffen, Bernhard

Levi, Giorgio

Inhaltsverzeichnis

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.