Geodesic

Volume 18 (2011) no. 4

Sommaire

From the editors of the special issue
p. 5-6
Typical examples of Atoment language using
p. 7-20
Attribute annotations and their use in C program deductive verification
p. 21-33
Approximating bisimulation in one-counter nets
p. 33-44
LLVM-based static analysis tool using type and effect systems
p. 45-55
Optimization procedures in affine model checking
p. 56-67
The use of dependencies for improving the precision of program static analysis
p. 68-79
Inhibitor Petri net that executes an arbitrary given Markov normal algorithm
p. 80-93
Automatic data race error detection in systemC models
p. 94-105
A simple algorithm for solving the coverability problem for monotonic counter systems
p. 106-117
A formal requirements model, used in the process of application code and test code generation
p. 118-130
A SPIN-based approach for detecting vulnerabilities in С~programs
p. 131-143
Verification of telecommunication systems specified by communicating finite automata with the help of coloured Petri nets
p. 144-156
C program verification: VC explanation and the standard library
p. 157-167
Verification of backtracking and branch and bound design templates
p. 168-180