[isabelle] Paper available

Dear all,

we are happy to announce our paper:

   D. Basin,  H. Kuruma, K. Miyazaki, K. Takaragi and B. Wolff: 
   Verifying a Signature Architecture - A Comparative Case Study.
   In Formal Aspects of Computing, 2006.
   To appear.

PDF: http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2006/fac.pdf

The paper reports on a substantial case study from the field of
computer security that had been done both with a model checking
approach and a theorem proving approach, such that empirical
data could be gained over what time had be invested to what
activity in both approaches.

The case-study gives some evidence, that theorem proving
isn't that ineffective after all, in particular if both
behavioral and data-modeling aspects are non-trivial and
if the modeling problem is open at the beginning (i.e. it 
is unclear how to formalize the intended properties.)
In our case, theorem proving did not use (significantly) more 
time, it used more expertise. And model-checking did have
a significant risc to prove valid, but inintended properties.


Best regards

Burkhart Wolff (and David Basin)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.