VMCAI 2003
25 papers
- A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution
- Abstract Interpretation-Based Certification of Assembly Code
- Abstraction of Expectation Functions Using Gaussian Distributions
- Action Refinement from a Logical Point of View
- Automatic Verification by Abstract Interpretation
- Behavior-Based Model Construction
- Bisimulation and Unwinding for Verifying Possibilistic Security Properties
- CHASE: A Static Checker for JML's Assignable Clause
- Complexity of Nesting Analysis in Mobile Ambients
- Domain Compression for Complete Abstractions
- Efficient Computation of Recurrence Diameters
- Efficient Verification of Timed Automata with BDD-Like Data-Structures
- Formal Verification of the Horn-Preneel Micropayment Protocol
- Lifting Temporal Proofs through Abstractions
- Model-Checking and Abstraction to the Aid of Parameterized Systems
- On the Expressiveness of 3-Valued Models
- Optimized Live Heap Bound Analysis
- Properties of a Type Abstract Interpreter
- Property Checking Driven Abstract Interpretation-Based Static Analysis
- Reasoning about Layered Message Passing Systems
- Shape Analysis through Predicate Abstraction and Model Checking
- Software Model Checking with Abstraction Refinement
- Symmetry Reductions in Model-Checking
- Types for Evolving Communication in Safe Ambients
- Using Simulated Execution in Verifying Distributed Algorithms