دانلود کتاب Verified Software. Theories, Tools, and Experiments: 10th International Conference, VSTTE 2018, Oxford, UK, July 18–19, 2018, Revised Selected Papers

فهرست مطالب :

Front Matter ....Pages I-XVI
A Tree-Based Approach to Data Flow Proofs (Jochen Hoenicke, Alexander Nutz, Andreas Podelski)....Pages 1-16
Executable Counterexamples in Software Model Checking (Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz)....Pages 17-37
Extending VIAP to Handle Array Programs (Pritom Rajkhowa, Fangzhen Lin)....Pages 38-49
Lattice-Based Refinement in Bounded Model Checking (Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina)....Pages 50-68
Verified Certificate Checking for Counting Votes (Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish)....Pages 69-87
Program Verification in the Presence of I/O (Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho)....Pages 88-111
TWAM: A Certifying Abstract Machine for Logic Programs (Brandon Bohrer, Karl Crary)....Pages 112-134
A Java Bytecode Formalisation (Patryk Czarnik, Jacek Chrząszcz, Aleksy Schubert)....Pages 135-154
Formalising Executable Specifications of Low-Level Systems (Paolo Torrini, David Nowak, Narjes Jomaa, Mohamed Sami Cherif)....Pages 155-176
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars (Alessandro Coglio)....Pages 177-195
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components (Robin Adams, Sibylle Schupp)....Pages 196-214
SideTrail: Verifying Time-Balancing of Cryptosystems (Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCarthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran)....Pages 215-228
Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity (Jakub Zakrzewski)....Pages 229-247
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms (Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich, Alexander Weigl)....Pages 248-266
Practical Methods for Reasoning About Java 8’s Functional Programming Features (David R. Cok, Serdar Tasiran)....Pages 267-278
Verification of Binarized Neural Networks via Inter-neuron Factoring (Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess)....Pages 279-290
The Map Equality Domain (Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski)....Pages 291-308
Loop Detection by Logically Constrained Term Rewriting (Naoki Nishida, Sarah Winkler)....Pages 309-321
Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment (Jonas Oberhauser)....Pages 322-344
Back Matter ....Pages 345-345