Abstract is missing.
- A Tree-Based Approach to Data Flow ProofsJochen Hoenicke, Alexander Nutz, Andreas Podelski. 1-16 [doi]
- Executable Counterexamples in Software Model CheckingJeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz. 17-37 [doi]
- Extending VIAP to Handle Array ProgramsPritom Rajkhowa, Fangzhen Lin. 38-49 [doi]
- Lattice-Based Refinement in Bounded Model CheckingKarine Even Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina. 50-68 [doi]
- Verified Certificate Checking for Counting VotesMilad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish. 69-87 [doi]
- Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified ApplicationsHugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho. 88-111 [doi]
- TWAM: A Certifying Abstract Machine for Logic ProgramsBrandon Bohrer, Karl Crary. 112-134 [doi]
- A Java Bytecode FormalisationPatryk Czarnik, Jacek Chrzaszcz, Aleksy Schubert. 135-154 [doi]
- Formalising Executable Specifications of Low-Level SystemsPaolo Torrini, David Nowak, Narjes Jomaa, Mohamed Sami Cherif. 155-176 [doi]
- A Formalization of the ABNF Notation and a Verified Parser of ABNF GrammarsAlessandro Coglio. 177-195 [doi]
- Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box ComponentsRobin Adams, Sibylle Schupp. 196-214 [doi]
- SideTrail: Verifying Time-Balancing of CryptosystemsKonstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran. 215-228 [doi]
- Towards Verification of Ethereum Smart Contracts: A Formalization of Core of SolidityJakub Zakrzewski 0001. 229-247 [doi]
- Relational Equivalence Proofs Between Imperative and MapReduce AlgorithmsBernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders 0001, Mattias Ulbrich, Alexander Weigl. 248-266 [doi]
- Practical Methods for Reasoning About Java 8's Functional Programming FeaturesDavid R. Cok, Serdar Tasiran. 267-278 [doi]
- Verification of Binarized Neural Networks via Inter-neuron Factoring - (Short Paper)Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess. 279-290 [doi]
- The Map Equality DomainDaniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski. 291-308 [doi]
- Loop Detection by Logically Constrained Term RewritingNaoki Nishida 0001, Sarah Winkler. 309-321 [doi]
- Store Buffer Reduction in the Presence of Mixed-Size Accesses and MisalignmentJonas Oberhauser. 322-344 [doi]