Abstract is missing.
- A Proof-Sensitive Approach for Small Propositional InterpolantsLeonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina. 1-18 [doi]
- Recursive Games for Compositional Program SynthesisTewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko. 19-39 [doi]
- Testing the IPC Protocol for a Real-Time Operating SystemAchim D. Brucker, Oto Havle, Yakoub Nemouchi, Burkhart Wolff. 40-60 [doi]
- Pseudo-Random Number Generator Verification: A Case StudyFelix Dörre, Vladimir Klebanov. 61-72 [doi]
- Inside a Verified Flash File System: Transactions and Garbage CollectionGidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif. 73-93 [doi]
- How to Avoid Proving the Absence of Integer OverflowsMartin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich. 94-109 [doi]
- Machine-Checked Proofs for Realizability Checking AlgorithmsAndreas Katis, Andrew Gacek, Michael W. Whalen. 110-123 [doi]
- Dynamic Frames Based Verification Method for Concurrent Java ProgramsWojciech Mostowski. 124-141 [doi]
- A Simpler Reduction Theorem for x86-TSOJonas Oberhauser. 142-164 [doi]
- Moving Around: Lipton's Reduction for TSO - (Regular Submission)Ali Sezgin, Serdar Tasiran. 165-182 [doi]
- Android Platform Modeling and Android App Verification in the ACL2 Theorem ProverEric Smith, Alessandro Coglio. 183-201 [doi]
- AUSPICE: Automatic Safety Property Verification for Unmodified ExecutablesJiaqi Tan, Hui Jun Tay, Rajeev Gandhi, Priya Narasimhan. 202-222 [doi]