Sciweavers

TPHOL
2003
IEEE
16 years 19 hour ago
Using Coq to Verify Java Card Applet Isolation Properties
June Andronick, Boutheina Chetali, Olivier Ly
171
Voted
TPHOL
2003
IEEE
16 years 19 hour ago
Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover
Abstract. Model checking and theorem proving are two complementary approaches to formal verification. In this paper we show how binary decision diagram (BDD) based symbolic model ...
Hasan Amjad
TPHOL
2003
IEEE
16 years 19 hour ago
Click'n Prove: Interactive Proofs within Set Theory
Jean-Raymond Abrial, Dominique Cansell