{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":1,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":32,"n_cols":5,"rows_kept":32,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[3,2,3,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[21,2,21,3],[22,2,22,3],[25,2,25,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNINA9910484522803321"]
[null,null,"Titolo",null,"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"]
[null,null,"Pubbl/distr/stampa",null,"Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017"]
[null,null,"ISBN",null,"3-319-72308-1"]
[null,null,"Edizione",null,"[1st ed. 2017.]"]
[null,null,"Descrizione fisica",null,"1 online resource (XIII, 211 p. 69 illus.)"]
[null,null,"Collana",null,"Programming and Software Engineering, , 2945-9168 ; ; 10712"]
[null,null,"Disciplina",null,"005.13"]
[null,null,"Soggetti",null,"Software engineering"]
[{"$nulls":4},"Computer science"]
[{"$nulls":4},"Compilers (Computer programs)"]
[{"$nulls":4},"Computer simulation"]
[{"$nulls":4},"Artificial intelligence"]
[{"$nulls":4},"Computers"]
[{"$nulls":4},"Professions"]
[{"$nulls":4},"Software Engineering"]
[{"$nulls":4},"Theory of Computation"]
[{"$nulls":4},"Compilers and Interpreters"]
[{"$nulls":4},"Computer Modelling"]
[{"$nulls":4},"Artificial Intelligence"]
[{"$nulls":4},"The Computing Profession"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Note generali","Includes index."]
[null,null,"Nota di contenuto",null,"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 "]
[{"$nulls":4},"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."]
[{"$nulls":4},"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 -- 3.4 Statistics on the Proof Effort -- 4 Benchmarks -- 5 Related Work -- 6 Conclusions -- References -- Automating the Verification of Floating-Point Programs -- 1 Introduction -- 2 Quick Introduction to SPARK and Why3 -- 3 VC Generation for Floating-Point Computations -- 3.1 Signature for a Generic Theory of IEEE FP Arithmetic -- 3.2 Theory Clones and FP Literals -- 3.3 Interpreting FP Computations in Ada -- 3.4 Proving VCs Using Native Support for SMT-LIB FP -- 3.5 Axiomatization for Provers Without Native Support -- 3.6 Consistency and Faithfulness -- 4 Experiments -- 4.1 Small Representative Examples -- 4.2 A Case Study -- 5 Conclusions and Perspectives -- References -- Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions -- 1 Introduction -- 2 Background on Cryptographic Hash Functions -- 2.1 SHA-1."]
[{"$nulls":4},"3 Architecture of MapleCrypt -- 3.1 SAT Encoding -- 3.2 CEGAR Loop Design -- 3.3 Multi-armed Bandit Restart -- 4 Experimental Results -- 4.1 Experimental Setup -- 4.2 CEGAR and MABR -- 4.3 Partial Preimage -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Practical Void Safety -- 1 Introduction -- 2 Motivating Examples -- 3 Overview -- 3.1 Language Conventions and Terminology -- 3.2 Solution Outline -- 4 Related Work -- 5 Formalization -- 5.1 Initialization State -- 5.2 Safe Uses of Current -- 5.3 Detection of Qualified Feature Calls -- 5.4 Validity Predicate -- 6 Practical Results -- 7 Conclusion -- References -- Memory-Efficient Tactics for Randomized LTL Model Checking -- 1 Introduction -- 2 Preliminaries -- 3 Monte Carlo Model Checking -- 4 Variants of the GS Tactic -- 5 Token-Based Tactics Without Hashing -- 6 Experimental Results -- 6.1 "]
[{"$nulls":4},"Dining Philosophers -- 6.2 Shared Memory Consensus Protocol -- 6.3 Pathological Linear Model -- 7 Conclusions and Further Work -- References -- Reordering Control Approaches to State Explosion in Model Checking with Memory Consistency Models -- 1 Introduction -- 2 Preliminaries -- 2.1 Instructions and Concurrent Programs -- 2.2 Reorderings of Instructions Under Relaxed MCMs -- 2.3 Representations of Memory Consistency Models -- 3 Reordering Control -- 3.1 Restriction of the Number of Issued Instructions -- 3.2 Restriction of Separations of Specified Instructions -- 3.3 Reordering-Oriented Explorations -- 4 Implementation for a Model Checker McSPIN -- 4.1 PROMELA Code Generated by McSPIN -- 4.2 Implementation of Local Restrictions -- 4.3 Implementation of Global Restrictions -- 4.4 Implementation of the Increasing and Decreasing Exploration Strategies -- 5 Case Studies of Various Concurrent Programs -- 5.1 MCMs, Programs, and the Experimental Environment."]
[{"$nulls":4},"5.2 How to Read the Tables of Experiments -- 5.3 Experimental Results -- 5.4 Other Results Obtained Besides the Comparisons -- 6 Related Work and Discussion -- 7 Conclusion and Future Work -- References -- An Abstraction Technique for Describing Concurrent Program Behaviour -- 1 Introduction -- 2 Background -- 2.1 Dynamic Locking -- 2.2 Process Algebra Terms -- 3 Motivating Example -- 4 Program Logic -- 4.1 Assertion Language -- 4.2 Proof System -- 5 Applications of the Logic -- 5.1 Concurrent Counting -- 5.2 Lock Specification -- 5.3 Other Verification Examples -- 6 Related Work -- 7 Conclusion -- References -- Author Index."]
[null,null,null,"Sommario/riassunto","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."]