VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
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...
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
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...
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
Abstract. Implementations of cryptographic protocols, such as OpenSSL for example, contain bugs affecting security, which cannot be detected by just analyzing abstract protocols (e...
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
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...
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
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...
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
Domain VMCAI 2005 Jérôme Feret Laboratoire d’Informatique de l’École Normale Supérieure INRIA, ÉNS, CNRS ØØÔ »»ÛÛÛº º Ò׺ Ö»∼ Ö Ø December, 2008.
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
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...
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer
VMCAI
2005
Springer
13 years 10 months ago
2005
Springer