LEADER 09472nam 22008295 450 001 9910484522803321 005 20251225205538.0 010 $a3-319-72308-1 024 7 $a10.1007/978-3-319-72308-2 035 $a(CKB)4100000001381781 035 $a(DE-He213)978-3-319-72308-2 035 $a(MiAaPQ)EBC6295218 035 $a(MiAaPQ)EBC5591428 035 $a(Au-PeEL)EBL5591428 035 $a(OCoLC)1017096735 035 $a(PPN)222227850 035 $a(EXLCZ)994100000001381781 100 $a20171215d2017 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aVerified Software. Theories, Tools, and Experiments $e9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers /$fedited by Andrei Paskevich, Thomas Wies 205 $a1st ed. 2017. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2017. 215 $a1 online resource (XIII, 211 p. 69 illus.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v10712 300 $aIncludes index. 311 08$a3-319-72307-3 327 $aIntro -- 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. 327 $aReferences -- 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. 327 $a3 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 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. 327 $a5.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. 330 $aThis 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. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v10712 606 $aSoftware engineering 606 $aComputer science 606 $aCompilers (Computer programs) 606 $aComputer simulation 606 $aArtificial intelligence 606 $aComputers 606 $aProfessions 606 $aSoftware Engineering 606 $aTheory of Computation 606 $aCompilers and Interpreters 606 $aComputer Modelling 606 $aArtificial Intelligence 606 $aThe Computing Profession 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aCompilers (Computer programs). 615 0$aComputer simulation. 615 0$aArtificial intelligence. 615 0$aComputers. 615 0$aProfessions. 615 14$aSoftware Engineering. 615 24$aTheory of Computation. 615 24$aCompilers and Interpreters. 615 24$aComputer Modelling. 615 24$aArtificial Intelligence. 615 24$aThe Computing Profession. 676 $a005.13 702 $aPaskevich$b Andrei$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aWies$b Thomas$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484522803321 996 $aVerified Software. Theories, Tools and Experiments$93004619 997 $aUNINA