Abstract is missing.
- Programming Inductive Proofs - A New Approach Based on Contextual TypesBrigitte Pientka. 1-16 [doi]
- Termination Graphs for Java BytecodeMarc Brockschmidt, Carsten Otto, Christian von Essen, Jürgen Giesl. 17-37 [doi]
- Specifying and Verifying Organizational Security Properties in First-Order LogicChristoph Brandt, Jens Otten, Christoph Kreitz, Wolfgang Bibel. 38-53 [doi]
- Change Management for Heterogeneous Development GraphsSerge Autexier, Dieter Hutter, Till Mossakowski. 54-80 [doi]
- The VATES-Diamond as a Verifier s Best FriendSabine Glesner, Björn Bartels, Thomas Göthel, Moritz Kleine. 81-101 [doi]
- Dynamic Rippling, Middle-Out Reasoning and Lemma DiscoveryMoa Johansson, Lucas Dixon, Alan Bundy. 102-116 [doi]
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)Christoph Benzmüller. 117-128 [doi]
- Second-Order Programs with PreconditionsMarkus Aderhold. 129-143 [doi]