Vol. 23 (2009): Automated Verification of Critical Systems 2009

DOI: https://doi.org/10.14279/tuj.eceasst.23

Published: 2010-01-24

Articles

High-level Proofs about Low-level Programs

Holger Gast, Julia Trieflinger
- PDF
Automatically Generating CSP Models for Communicating Haskell Processes

Neil Brown
- PDF
Mobile CSP||B

Beeta Vajar, Steve Schneider, Helen Treharne
- PDF
A coinductive approach to verified exact real number computation

Ulrich Berger, Sion Lloyd
- PDF
Towards SMV Model Checking of Signal (multi-clocked) Specifications

Julio Peralta, Thierry Gautier
- PDF
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS

Reynald Affeldt, David Nowak, Kiyoshi Yamada
- PDF
A workbench for preprocessor design and evaluation: toward benchmarks for parity games

Michael Huth, Nir Piterman, Huaxin Wang
- PDF
Proofs-as-Programs in Computable Analysis

Ulrich Berger
- PDF
A decidable class of verification conditions for programs with higher order store

Nathaniel Charlton, Bernhard Reus
- 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
Verification of safety requirements for program code using data abstraction

Frank Stappers, Michel Reniers
- PDF
An Extension of the Inverse Method to Probabilistic Timed Automata

Étienne André, Jeremy Sproston, Laurent Fribourg
- PDF
Faster FDR Counterexample Generation Using SAT-Solving

Hristina Palikareva, Joel Ouaknine, Bill Roscoe
- PDF
User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?

Christoph Lüth
- PDF

Preface

Preface

Markus Roggenbach
- PDF

Vol. 23 (2009): Automated Verification of Critical Systems 2009

Articles

High-level Proofs about Low-level Programs

Automatically Generating CSP Models for Communicating Haskell Processes

Mobile CSP||B

A coinductive approach to verified exact real number computation

Towards SMV Model Checking of Signal (multi-clocked) Specifications

Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS

A workbench for preprocessor design and evaluation: toward benchmarks for parity games

Proofs-as-Programs in Computable Analysis

A decidable class of verification conditions for programs with higher order store

Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form

Verification of safety requirements for program code using data abstraction

An Extension of the Inverse Method to Probabilistic Timed Automata

Faster FDR Counterexample Generation Using SAT-Solving

User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?

Preface

Preface

Information

Usage Statistics Information