Amazon cover image
Image from Amazon.com

Verified software : theories, tools, and experiments : 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised selected papers / edited by Andrei Paskevich, Thomas Wies.

By: Contributor(s): Material type: TextTextSeries: Lecture notes in computer science ; 10712. | LNCS sublibrary. SL 2, Programming and software engineering.Publisher: Cham, Switzerland : Springer, 2017Description: 1 online resource (xiii, 211 pages) : illustrationsContent type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9783319723082
  • 3319723081
  • 3319723073
  • 9783319723075
Other title:
  • VSTTE 2017
Subject(s): Genre/Form: Additional physical formats: Printed edition:: No titleDDC classification:
  • 005.1/4 23
LOC classification:
  • QA76.76.V47
Online resources:
Contents:
Intro -- Preface -- Organization -- Abstracts of Short Papers -- Everest: A Verified and High-Performance HTTPS Stack -- Design Principles of Automated Reasoning Systems -- Why Verification Cannot Ignore Resource Usage -- Constructing Correct Concurrent Programs Layer by Layer -- Contents -- A Formally Verified Interpreter for a Shell-Like Programming Language -- 1 Introduction -- 2 Language -- 2.1 Elements of Shell -- 2.2 Syntax of CoLiS -- 2.3 Semantics -- 2.4 Mechanised Version -- 3 Interpreter -- 3.1 Proof of Soundness -- 4 Proof of Completeness
4.1 Proving (or not Proving) Termination with Heights and Sizes -- 4.2 Proving Termination with Ghosts and Skeletons -- 4.3 Reproducibility -- 5 Related Work -- 6 Conclusion and Future Work -- References -- A Formal Analysis of the Compact Position Reporting Algorithm -- 1 Introduction -- 2 The Compact Position Reporting Algorithm -- 2.1 Number of Longitude Zones -- 2.2 Encoding -- 2.3 Local Decoding -- 2.4 Global Decoding -- 3 Practical Results -- 3.1 Decoding Requirements -- 3.2 Numerical Simplifications -- 4 Animation of the CPR Specification -- 5 Conclusion -- References
Proving JDK's Dual Pivot Quicksort Correct -- 1 Introduction -- 2 Dual Pivot Quicksort -- 2.1 The Abstract Algorithm -- 2.2 JDK's Implementation -- 3 Background -- 3.1 Java Modeling Language -- 3.2 The Program Verification System KeY -- 4 Specification and Verification -- 4.1 Proof Management by Gentle Problem Adaptation -- 4.2 The Sortedness Property -- 4.3 The Permutation Property -- 4.4 Absence of Integer Overflow -- 4.5 Sorting Pivot Candidates -- 5 Verification Effort -- 6 Invalid Invariant in Single Pivot Quicksort -- 7 Conclusions -- References
A Semi-automatic Proof of Strong Connectivity -- 1 Introduction -- 2 The Algorithm -- 3 Invariants -- 4 Pre-/Post-conditions -- 5 The Formal Proof -- 6 Conclusion -- References -- Verifying Branch-Free Assembly Code in Why3 -- 1 Introduction -- 1.1 The Why3 Verification Platform -- 1.2 Multiprecision Multiplication -- 2 Verification Approach -- 2.1 Validation of the Formal Model -- 2.2 Logical Partitioning -- 3 Modelling the AVR Instruction Set -- 3.1 Representing Multiprecision Integers -- 3.2 Using Ghost Code to Reduce Annotations -- 3.3 Model Validation -- 3.4 Underspecification
4 Verifying AVR Assembly Code -- 4.1 Operand-Scanning Multiplication -- 4.2 Karatsuba Multiplication -- 5 Related Work -- 6 Conclusion -- 6.1 Future Work -- References -- How to Get an Efficient yet Verified Arbitrary-Precision Integer Library -- 1 Introduction -- 2 From WhyML to C -- 2.1 Machine Words and Arithmetic Primitives -- 2.2 A Simple Model for C Pointers and Heap Memory -- 2.3 Extracting to Idiomatic C Code -- 3 Computing with Arbitrary-Precision Integers -- 3.1 Algorithm Specifications -- 3.2 Example of Proved Algorithm: Comparison -- 3.3 Trickier Example: Long Division
Summary: This volume constitutes the thoroughly refereed post-conference proceedings of the 9th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, held in Heidelberg, Germany, in July 2017. The 12 full papers presented were carefully revised and selected from 20 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.
Holdings
Item type Current library Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library eBook LNCS Available
Total holds: 0

Includes author index.

Online resource; title from PDF title page (SpringerLink, viewed December 26, 2017).

This volume constitutes the thoroughly refereed post-conference proceedings of the 9th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, held in Heidelberg, Germany, in July 2017. The 12 full papers presented were carefully revised and selected from 20 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.

Intro -- Preface -- Organization -- Abstracts of Short Papers -- Everest: A Verified and High-Performance HTTPS Stack -- Design Principles of Automated Reasoning Systems -- Why Verification Cannot Ignore Resource Usage -- Constructing Correct Concurrent Programs Layer by Layer -- Contents -- A Formally Verified Interpreter for a Shell-Like Programming Language -- 1 Introduction -- 2 Language -- 2.1 Elements of Shell -- 2.2 Syntax of CoLiS -- 2.3 Semantics -- 2.4 Mechanised Version -- 3 Interpreter -- 3.1 Proof of Soundness -- 4 Proof of Completeness

4.1 Proving (or not Proving) Termination with Heights and Sizes -- 4.2 Proving Termination with Ghosts and Skeletons -- 4.3 Reproducibility -- 5 Related Work -- 6 Conclusion and Future Work -- References -- A Formal Analysis of the Compact Position Reporting Algorithm -- 1 Introduction -- 2 The Compact Position Reporting Algorithm -- 2.1 Number of Longitude Zones -- 2.2 Encoding -- 2.3 Local Decoding -- 2.4 Global Decoding -- 3 Practical Results -- 3.1 Decoding Requirements -- 3.2 Numerical Simplifications -- 4 Animation of the CPR Specification -- 5 Conclusion -- References

Proving JDK's Dual Pivot Quicksort Correct -- 1 Introduction -- 2 Dual Pivot Quicksort -- 2.1 The Abstract Algorithm -- 2.2 JDK's Implementation -- 3 Background -- 3.1 Java Modeling Language -- 3.2 The Program Verification System KeY -- 4 Specification and Verification -- 4.1 Proof Management by Gentle Problem Adaptation -- 4.2 The Sortedness Property -- 4.3 The Permutation Property -- 4.4 Absence of Integer Overflow -- 4.5 Sorting Pivot Candidates -- 5 Verification Effort -- 6 Invalid Invariant in Single Pivot Quicksort -- 7 Conclusions -- References

A Semi-automatic Proof of Strong Connectivity -- 1 Introduction -- 2 The Algorithm -- 3 Invariants -- 4 Pre-/Post-conditions -- 5 The Formal Proof -- 6 Conclusion -- References -- Verifying Branch-Free Assembly Code in Why3 -- 1 Introduction -- 1.1 The Why3 Verification Platform -- 1.2 Multiprecision Multiplication -- 2 Verification Approach -- 2.1 Validation of the Formal Model -- 2.2 Logical Partitioning -- 3 Modelling the AVR Instruction Set -- 3.1 Representing Multiprecision Integers -- 3.2 Using Ghost Code to Reduce Annotations -- 3.3 Model Validation -- 3.4 Underspecification

4 Verifying AVR Assembly Code -- 4.1 Operand-Scanning Multiplication -- 4.2 Karatsuba Multiplication -- 5 Related Work -- 6 Conclusion -- 6.1 Future Work -- References -- How to Get an Efficient yet Verified Arbitrary-Precision Integer Library -- 1 Introduction -- 2 From WhyML to C -- 2.1 Machine Words and Arithmetic Primitives -- 2.2 A Simple Model for C Pointers and Heap Memory -- 2.3 Extracting to Idiomatic C Code -- 3 Computing with Arbitrary-Precision Integers -- 3.1 Algorithm Specifications -- 3.2 Example of Proved Algorithm: Comparison -- 3.3 Trickier Example: Long Division

Powered by Koha