Radhia Cousot
Proceedings of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2005.

@proceedings{VMCAI-2005,
	address       = "Paris, France",
	editor        = "Radhia Cousot",
	isbn          = "3-540-24297-X",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 3385,
	year          = 2005,
}

Contents (30 items)

6 ×#source code
5 ×#abstraction
5 ×#analysis
5 ×#model checking
4 ×#verification
3 ×#abstract interpretation
3 ×#linear
3 ×#performance
2 ×#automaton
2 ×#bound

VMCAI-2005-Cousot #abstraction #parametricity #programming #proving #termination

Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming (PC), pp. 1–24.

VMCAI-2005-SankaranarayananSM #analysis #linear #programming #scalability #using

Scalable Analysis of Linear Systems Using Mathematical Programming (SS, HBS, ZM), pp. 25–41.

VMCAI-2005-Feret #abstract domain #geometry

The Arithmetic-Geometric Progression Abstract Domain (JF), pp. 42–58.

VMCAI-2005-Martel #overview #semantics #source code #validation

An Overview of Semantics for the Validation of Numerical Programs (MM), pp. 59–77.

VMCAI-2005-Hoare #challenge #compilation #research #verification

The Verifying Compiler, a Grand Challenge for Computing Research (CARH), p. 78.

VMCAI-2005-Muller-OlmRS

Checking Herbrand Equalities and Beyond (MMO, OR, HS), pp. 79–96.

VMCAI-2005-Bertrane #abstract interpretation #composition #source code #static analysis

Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous Programs (JB), pp. 97–112.

VMCAI-2005-BradleyMS #polynomial #source code #termination

Termination of Polynomial Programs (ARB, ZM, HBS), pp. 113–129.

VMCAI-2005-BurckhardtAM #composition #implementation #parametricity #refinement #safety #verification

Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement (SB, RA, MMKM), pp. 130–145.

VMCAI-2005-Pnueli #abstraction #liveness

Abstraction for Liveness (AP), p. 146.

VMCAI-2005-ChangL #abstract interpretation

Abstract Interpretation with Alien Expressions and Heap Structures (BYEC, KRML), pp. 147–163.

VMCAI-2005-BalabanPZ #abstraction #analysis

Shape Analysis by Predicate Abstraction (IB, AP, LDZ), pp. 164–180.

VMCAI-2005-ManevichYRS #abstraction #canonical

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists (RM, EY, GR, SS), pp. 181–198.

VMCAI-2005-SalcianuR #analysis #java #source code

Purity and Side Effect Analysis for Java Programs (AS, MCR), pp. 199–215.

VMCAI-2005-DamsN #abstraction #automaton

Automata as Abstractions (DD, KSN), pp. 216–232.

VMCAI-2005-GrumbergLLS #calculus

Don’t Know in the µ-Calculus (OG, ML, ML, SS), pp. 233–249.

VMCAI-2005-SistlaZW #commutative #model checking

Model Checking of Systems Employing Commutative Functions (APS, MZ, XW), pp. 250–266.

VMCAI-2005-Lange #automaton #calculus #linear

Weak Automata for the Linear Time µ-Calculus (ML), pp. 267–281.

VMCAI-2005-Bozzelli #model checking #process #term rewriting

Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties (LB), pp. 282–297.

VMCAI-2005-ShenQL #incremental #satisfiability

Minimizing Counterexample with Unit Core Extraction and Incremental SAT (SS, YQ, SL), pp. 298–312.

VMCAI-2005-JabbarE #model checking #performance

I/O Efficient Directed Model Checking (SJ, SE), pp. 313–329.

VMCAI-2005-Hymans #abstract interpretation #fault #verification

Verification of an Error Correcting Code by Abstract Interpretation (CH), pp. 330–345.

VMCAI-2005-GenaimS #analysis #bytecode #data flow #java

Information Flow Analysis for Java Bytecode (SG, FS), pp. 346–362.

VMCAI-2005-Goubault-LarrecqP #analysis #c #encryption #protocol

Cryptographic Protocol Analysis on Real C Code (JGL, FP), pp. 363–379.

VMCAI-2005-LatvalaBHJ #bound #ltl #model checking #performance

Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.

VMCAI-2005-AbrahamBKS #bound #hybrid #linear #model checking #optimisation

Optimizing Bounded Model Checking for Linear Hybrid Systems (EÁ, BB, FK, MS), pp. 396–412.

VMCAI-2005-Siegel #performance #source code #verification

Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives (SFS), pp. 413–429.

VMCAI-2005-LamKR #consistency #data type #type system

Generalized Typestate Checking for Data Structure Consistency (PL, VK, MCR), pp. 430–447.

VMCAI-2005-KumarKV #complexity #fault #on the

On the Complexity of Error Explanation (NK, VK, MV), pp. 448–464.

VMCAI-2005-AttieC #concurrent #scalability #source code

Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs (PCA, HC), pp. 465–481.