1. Theorem proving in technology transfer: the user’s point of view

   • Fausto Giunchiglia
   • Paolo Traverso

   Special section an theorem proving Pages: 1 - 12

2. Verification of Year 2000 conversion rules using the ACL2 theorem prover

   • Matt Kaufmann

   Special section an theorem proving Pages: 13 - 19

3. High-automation proofs for properties of requirements models

   • Ben L. Di Vito

   Special section an theorem proving Pages: 20 - 31

4. Using an induction prover for verifying arithmetic circuits

   • Deepak Kapur
   • Mahadevan Subramaniam

   Special section an theorem proving Pages: 32 - 65

5. VSE: formal methods meet industrial needs

   • Serge Autexier
   • Dieter Hutter
   • Andreas Wolpers

   Special section an theorem proving Pages: 66 - 77

6. Mechanized result verification: an industrial application

   • Paolo Traverso
   • Piergiorgio Bertoli

   Special section an theorem proving Pages: 78 - 92

7. Detecting races in Relay Ladder Logic programs

   • Alexander Aiken
   • Manuel Fähndrich
   • Zhendong Su

   Regular contribution Pages: 93 - 105