Sciweavers

VMCAI
2005
Springer
15 years 2 months ago
Optimizing Bounded Model Checking for Linear Hybrid Systems
Bounded model checking (BMC) is an automatic verification method that is based on a finite unfolding of the system’s transition relation. BMC has been successfully applied, in ...
Erika Ábrahám, Bernd Becker, Felix K...
VMCAI
2005
Springer
15 years 2 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
15 years 2 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
15 years 2 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
Software Engineering
Top of PageReset Settings