Vol. 6 No. 1 (2013)

Articles

• Formal Verification of Language-Based Concurrent Noninterference

  Andrei Popescu, Johannes Hölzl, Tobias Nipkow

  1-30

  • PDF

• Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model

  Mauricio Ayala-Rincón, Yuri Santos Rego

  31-61

  • PDF

• A String of Pearls: Proofs of Fermat's Little Theorem

  Hing Lun Chan, Michael Norrish

  63-87

  • PDF

• A Formal Proof of Square Root and Division Elimination in Embedded Programs

  Pierre Neron

  89-111

  • PDF