5. VMCAI 2004: Venice, Italy

Bernhard Steffen, Giorgio Levi (Eds.): Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings. Lecture Notes in Computer Science 2937 Springer 2004, ISBN 3-540-20803-8

@proceedings{DBLP:conf/vmcai/2004,
  editor    = {Bernhard Steffen and
               Giorgio Levi},
  title     = {Verification, Model Checking, and Abstract Interpretation, 5th
               International Conference, VMCAI 2004, Venice, January 11-13,
               2004, Proceedings},
  booktitle = {VMCAI},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2937},
  year      = {2004},
  isbn      = {3-540-20803-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Tutorial

Joshua D. Guttman:
Security, Protocols, and Trust. 1

Security

Gilles Barthe, Amitabh Basu, Tamara Rezk:
Security Types Preserving Compilation: (Extended Abstract). 2-15
Vincent Vanackère:
History-Dependent Scheduling for Cryptographic Processes. 16-29

Formal Methods I

Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu:
Construction of a Semantic Model for a Typed Assembly Language. 30-43
Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen:
Rule-Based Runtime Verification. 44-57

Invited Talk

Shmuel Sagiv:
On the Expressive Power of Canonical Abstraction. 58

Miscellaneous

Viktor Kuncak, Martin C. Rinard:
Boolean Algebra of Shape Analysis Constraints. 59-72

Model Checking

Thomas Hérault, Richard Lassaigne, Frédéric Magniette, Sylvain Peyronnet:
Approximate Probabilistic Model Checking. 73-84
Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman:
Completeness and Complexity of Bounded Model Checking. 85-96
Dorel Lucanu, Gabriel Ciobanu:
Model Checking for Object Specifications in Hidden Algebra. 97-109

Formal Methods II

Gordon J. Pace, Gerardo Schneider:
Model Checking Polygonal Differential Inclusions Using Invariance Kernels. 110-121
Pei Yu, Qiwen Xu:
Checking Interval Based Properties for Reactive Systems. 122-134
Roberto Bagnara, Patricia M. Hill, Enea Zaffanella:
Widening Operators for Powerset Domains. 135-148

Software Checking

Rahul Agarwal, Scott D. Stoller:
Type Inference for Parameterized Race-Free Java. 149-160
Songtao Xia, James Hook:
Certifying Temporal Properties for Compiled C Programs. 161-174
John Hatcliff, Robby, Matthew B. Dwyer:
Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. 175-190

Invited Talk

Dawson R. Engler, Madanlal Musuvathi:
Static Analysis versus Software Model Checking for Bug Finding. 191-210

Software Checking

Francesco Logozzo:
Automatic Inference of Class Invariants. 211-222

Liveness and Completeness

Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck:
Liveness with Invisible Ranking. 223-238
Andreas Podelski, Andrey Rybalchenko:
A Complete Method for the Synthesis of Linear Ranking Functions. 239-251
Thomas W. Reps, Shmuel Sagiv, Greta Yorsh:
Symbolic Implementation of the Best Transformer. 252-266

Formal Methods III

Shuvendu K. Lahiri, Randal E. Bryant:
Constructing Quantified Invariants via Predicate Abstraction. 267-281
Kousha Etessami:
Analysis of Recursive Game Graphs Using Data Flow Equations. 282-296
Cyrille Artho, Klaus Havelund:
Applying Jlint to Space Exploration Software. 297-308
Reinhard Wilhelm:
Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone. 309-322

Key Note

David Harel:
A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal. 323-324

Last update Fri May 25 08:46:15 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page