Sciweavers

VMCAI
2005
Springer
14 years 4 months ago
Generalized Typestate Checking for Data Structure Consistency
Abstract. We present an analysis to verify abstract set specifications for programs that use object field values to determine the membership of objects in abstract sets. In our a...
Patrick Lam, Viktor Kuncak, Martin C. Rinard
VMCAI
2005
Springer
14 years 4 months ago
On the Complexity of Error Explanation
When a system fails to satisfy its specification, the model checker produces an error trace (or counter-example) that demonstrates an undesirable behavior, which is then used in d...
Nirman Kumar, Viraj Kumar, Mahesh Viswanathan
VMCAI
2005
Springer
14 years 4 months ago
Cryptographic Protocol Analysis on Real C Code
Abstract. Implementations of cryptographic protocols, such as OpenSSL for example, contain bugs affecting security, which cannot be detected by just analyzing abstract protocols (e...
Jean Goubault-Larrecq, Fabrice Parrennes
VMCAI
2005
Springer
14 years 4 months ago
Information Flow Analysis for Java Bytecode
Abstract. We present a context-sensitive compositional analysis of information flow for full (mono-threaded) Java bytecode. Our idea consists in transforming the Java bytecode int...
Samir Genaim, Fausto Spoto
VMCAI
2005
Springer
14 years 4 months ago
Model Checking of Systems Employing Commutative Functions
Abstract. The paper presents methods for model checking a class of possibly infinite state concurrent programs using various types of bi-simulation reductions. The proposed method...
A. Prasad Sistla, Min Zhou, Xiaodong Wang
VMCAI
2005
Springer
14 years 4 months ago
The Arithmetic-Geometric Progression Abstract Domain
Domain VMCAI 2005 Jérôme Feret Laboratoire d’Informatique de l’École Normale Supérieure INRIA, ÉNS, CNRS ØØÔ »»ÛÛÛº º Ò׺ Ö»∼ Ö Ø December, 2008.
Jérôme Feret
VMCAI
2005
Springer
14 years 4 months ago
Minimizing Counterexample with Unit Core Extraction and Incremental SAT
Abstract. It is a hotly researching topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. K Ravi proposes a two-stages counterexample min...
ShengYu Shen, Ying Qin, Sikun Li
VMCAI
2005
Springer
14 years 4 months ago
Scalable Analysis of Linear Systems Using Mathematical Programming
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Man...
VMCAI
2005
Springer
14 years 4 months ago
Automata as Abstractions
Dennis Dams, Kedar S. Namjoshi