Volume 23: Automated Verification of Critical Systems 2009

DOI: http://dx.doi.org/10.14279/tuj.eceasst.23

Table of Contents

Preface

Preface
Markus Roggenbach
PDF

Articles

Proofs-as-Programs in Computable Analysis
Ulrich Berger
PDF
User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?
Christoph Lüth
PDF
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS
Reynald Affeldt, David Nowak, Kiyoshi Yamada
PDF
An Extension of the Inverse Method to Probabilistic Timed Automata
Étienne André, Jeremy Sproston, Laurent Fribourg
PDF
A coinductive approach to verified exact real number computation
Ulrich Berger, Sion Lloyd
PDF
Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form
Loïc Besnard, Thierry Gautier, Matthieu Moy, Jean-Pierre Talpin, Kenneth Johnson, Florence Maraninchi
PDF
Automatically Generating CSP Models for Communicating Haskell Processes
Neil Christopher Charles Brown
PDF
A decidable class of verification conditions for programs with higher order store
Nathaniel Charlton, Bernhard Reus
PDF
High-level Proofs about Low-level Programs
Holger Gast, Julia Trieflinger
PDF
A workbench for preprocessor design and evaluation: toward benchmarks for parity games
Michael Huth, Nir Piterman, Huaxin Wang
PDF
Faster FDR Counterexample Generation Using SAT-Solving
Hristina Palikareva, Joel Ouaknine, Bill Roscoe
PDF
Towards SMV Model Checking of Signal (multi-clocked) Specifications
Julio C. Peralta, Thierry Gautier
PDF
Verification of safety requirements for program code using data abstraction
Frank Stappers, Michel Reniers
PDF
Mobile CSP||B
Beeta Vajar, Steve Schneider, Helen Treharne
PDF