Verified Software. Theories, Tools, and Experiments

1. Front Matter

   Pages I-XVI

   PDF

2. A Tree-Based Approach to Data Flow Proofs

   • Jochen Hoenicke, Alexander Nutz, Andreas Podelski

   Pages 1-16

3. Executable Counterexamples in Software Model Checking

   • Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz

   Pages 17-37

4. Extending VIAP to Handle Array Programs

   • Pritom Rajkhowa, Fangzhen Lin

   Pages 38-49

5. Lattice-Based Refinement in Bounded Model Checking

   • Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina

   Pages 50-68

6. Verified Certificate Checking for Counting Votes

   • Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish

   Pages 69-87

7. 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

8. TWAM: A Certifying Abstract Machine for Logic Programs

   • Rose Bohrer, Karl Crary

   Pages 112-134

9. A Java Bytecode Formalisation

   • Patryk Czarnik, Jacek Chrząszcz, Aleksy Schubert

   Pages 135-154

10. Formalising Executable Specifications of Low-Level Systems

    • Paolo Torrini, David Nowak, Narjes Jomaa, Mohamed Sami Cherif

    Pages 155-176

11. A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars

    • Alessandro Coglio

    Pages 177-195

12. Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components

    • Robin Adams, Sibylle Schupp

    Pages 196-214

13. SideTrail: Verifying Time-Balancing of Cryptosystems

    • Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCarthaigh, Daniel Schwartz-Narbonne, Serdar Tasiran

    Pages 215-228

14. Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity

    • Jakub Zakrzewski

    Pages 229-247

15. Relational Equivalence Proofs Between Imperative and MapReduce Algorithms

    • Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich, Alexander Weigl

    Pages 248-266

16. Practical Methods for Reasoning About Java 8’s Functional Programming Features

    • David R. Cok, Serdar Tasiran

    Pages 267-278

17. Verification of Binarized Neural Networks via Inter-neuron Factoring

    • Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, Harald Ruess

    Pages 279-290

18. The Map Equality Domain

    • Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski

    Pages 291-308

19. Loop Detection by Logically Constrained Term Rewriting

    • Naoki Nishida, Sarah Winkler

    Pages 309-321

20. Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment

    • Jonas Oberhauser

    Pages 322-344

This volume constitutes the thoroughly refereed post-conference proceedings of the 10th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018, held in Oxford, UK, in July 2018.

The 19 full papers presented were carefully revised and selected from 24 submissions. The papers describe large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge as well as novel experiments and case studies evaluating verification techniques and technologies.

• artificial intelligence
• embedded systems
• first order logic
• formal logic
• formal methods
• hardware
• java
• logic programming
• model checking
• parallel processing systems
• program compilers
• program verification
• programming language
• programming languages
• semantics
• software engineering
• software evaluation
• specifications
• theorem proving
• verification

• Yale University, New Haven, USA

  Ruzica Piskac

• Uppsala University, Uppsala, Sweden

  Philipp Rümmer

Policies and ethics