| Description |
1 online resource (xiii, 211 pages) : illustrations |
| Series |
Lecture Notes in Computer Science, 0302-9743 ; 10712 |
|
LNCS sublibrary. SL 2, Programming and software engineering |
|
Lecture notes in computer science ; 10712. 0302-9743
|
|
LNCS sublibrary. SL 2, Programming and software engineering.
|
| 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 |
| Notes |
Includes author index |
|
Online resource; title from PDF title page (SpringerLink, viewed December 26, 2017) |
| Subject |
Computer software -- Verification -- Congresses
|
|
Computer software -- Quality control -- Congresses
|
|
Compilers (Computer programs) -- Congresses
|
|
Computer science.
|
|
Programming & scripting languages: general.
|
|
Computer modelling & simulation.
|
|
Artificial intelligence.
|
|
Information technology: general issues.
|
|
Software Engineering.
|
|
Computers -- Computer Science.
|
|
Computers -- Programming Languages -- General.
|
|
Computers -- Computer Simulation.
|
|
Computers -- Intelligence (AI) & Semantics.
|
|
Computers -- General.
|
|
Computers -- Software Development & Engineering -- General.
|
|
Compilers (Computer programs)
|
|
Computer software -- Quality control
|
|
Computer software -- Verification
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Paskevich, Andrei, editor.
|
|
Wies, Thomas, editor
|
| ISBN |
9783319723082 |
|
3319723081 |
|
3319723073 |
|
9783319723075 |
