Abstract is missing.
- A Formally Verified Interpreter for a Shell-Like Programming LanguageNicolas Jeannerod, Claude Marché, Ralf Treinen. 1-18 [doi]
- A Formal Analysis of the Compact Position Reporting AlgorithmAaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz. 19-34 [doi]
- Proving JDK's Dual Pivot Quicksort CorrectBernhard Beckert, Jonas Schiffl, Peter H. Schmitt, Mattias Ulbrich. 35-48 [doi]
- A Semi-automatic Proof of Strong ConnectivityRan Chen, Jean-Jacques Lévy. 49-65 [doi]
- Verifying Branch-Free Assembly Code in Why3Marc Schoolderman. 66-83 [doi]
- How to Get an Efficient yet Verified Arbitrary-Precision Integer LibraryRaphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. 84-101 [doi]
- Automating the Verification of Floating-Point ProgramsClément Fumex, Claude Marché, Yannick Moy. 102-119 [doi]
- Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash FunctionsSaeed Nejati, Jia Hui Liang, Catherine H. Gebotys, Krzysztof Czarnecki, Vijay Ganesh. 120-131 [doi]
- Practical Void SafetyAlexander Kogtenkov. 132-151 [doi]
- Memory-Efficient Tactics for Randomized LTL Model CheckingKim G. Larsen, Doron Peled, Sean Sedwards. 152-169 [doi]
- Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency ModelsTatsuya Abe 0001, Tomoharu Ugawa, Toshiyuki Maeda. 170-190 [doi]
- An Abstraction Technique for Describing Concurrent Program BehaviourWytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, Marina Zaharieva-Stojanovski. 191-209 [doi]