Skip to main content
SpringerLink
Log in

Verified Software. Theories, Tools, and Experiments

10th International Conference, VSTTE 2018, Oxford, UK, July 18–19, 2018, Revised Selected Papers

  • Conference proceedings
  • © 2018

Overview

Editors:
  1. Ruzica Piskac

    1. Yale University, New Haven, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Philipp Rümmer

    1. Uppsala University, Uppsala, Sweden

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 11294)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: VSTTE 2018.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (19 papers)

  1. Front Matter

    Pages I-XVI
    Download chapter 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
Back to top

Other volumes

  1. Verified Software. Theories, Tools, and Experiments

Keywords

About this book

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.

Editors and Affiliations

  • Yale University, New Haven, USA

    Ruzica Piskac

  • Uppsala University, Uppsala, Sweden

    Philipp Rümmer

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation