Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers (Programming and Software Engineering)

This volume constitutes the thoroughly refereed post-conference proceedings of the 11th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2019, held in New York City, NY, USA, in July 2019. The 9 full papers presented were carefully revised and selected from 17 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. Preface 6 Organization 7 Abstract of Invited Talks 9 Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer 10 Uncertainty, Modeling and Safety Assurance: Towards a Unified Framework 11 Verifying Network Control Planes 12 Quantifying Information Leakage Using Model Counting Constraint Solvers 13 Contents 14 Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer 16 1 Introduction 16 2 Unified Extensible Language 19 3 Dynamic Expression Rewriting 20 4 Domain Combination 23 5 Implementation and Applications 26 5.1 C Analysis 26 5.2 C Stub Modeling 28 5.3 Python Analysis 29 6 Conclusion 31 References 32 Uncertainty, Modeling and Safety Assurance: Towards a Unified Framework 34 1 Motivation and Overview 34 2 The Lane Management System Example 35 3 Identifying Uncertainty 36 4 Assessing Uncertainty 38 5 Addressing Uncertainty 39 6 Challenges 41 References 43 Quantifying Information Leakage Using Model Counting Constraint Solvers 45 1 Quantitative Program Analysis 45 2 Automata-Based Model Counting 46 3 Side-Channel Analysis 47 4 Attack Synthesis 47 5 Conclusions and Future Directions 48 References 49 Verifiable Homomorphic Tallying for the Schulze Vote Counting Scheme 51 1 Introduction 51 2 Verifiable Homomorphic Tallying 53 3 Realisation in a Theorem Prover 58 4 Correctness by Construction and Verification 61 5 Extraction and Experiments 63 6 Analysis 66 References 67 Incremental Minimization of Symbolic Automata 69 1 Introduction 69 2 Preliminaries 70 3 Incremental Minimization of Symbolic Automata 72 4 Evaluation 77 5 Related Work 80 6 Conclusion and Future Work 81 References 82 Seamless Interactive Program Verification 83 1 Setting the Stage: Interactive Program Verification 84 1.1 Verification Task 84 1.2 Interaction Styles 86 2 User Activities Revealed in User Studies 87 3 Seamless Interaction Concept 89 3.1 Projections: Multiple Views onto the Proof Problem 90 3.2 Relations Between Proof Artifacts 93 4 Realization of the Concept 94 5 Related Work 97 6 Conclusion and Future Work 98 References 99 Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain 102 1 Introduction 102 2 Overview 104 2.1 Workbench Application Policy 104 2.2 Workbench Application Smart Contract 105 2.3 Semantic Conformance Verification 106 3 Semantic Conformance Checking 107 3.1 Formalization of Workbench Application Policies 107 3.2 Semantic Conformance 108 3.3 Instrumentation for Semantic Conformance Checking 109 4 Formal Verification Using VeriSol 110 4.1 General Methodology 110 4.2 Overview 111 4.3 Solidity to Boogie Translation 112 4.4 Invariant Generation 115 4.5 Bounded Model Checking 116 5 Evaluation 116 6 Related Work 118 7 Conclusion 119 References 119 Ghost Code in Action: Automated Verification of a Symbolic Interpreter 122 1 Introduction 122 2 Presentation of the IMP Language 125 2.1 Formal Semantics 125 2.2 Concrete Execution 127 3 Symbolic Execution 129 3.1 Correctness Properties of a Symbolic Interpreter 130 3.2 Implementation of the Symbolic Interpreter 131 3.3 Proofs of the Symbolic Properties 135 3.4 Execution and Test of the Symbolic Interpreter 136 4 Conclusions, Related Work and Future Work 137 References 138 DCSynth: Guided Reactive Synthesis with Soft Requirements 139 1 Introduction 139 2 Quantified Discrete Duration Calculus (QDDC) Logic 142 3 Supervisor and Controller 143 4 DCSynth Specification and Controller Synthesis 145 4.1 Invariance Properties and Maximally Permissive Supervisor 145 4.2 Maximally Permissive H-Optimal Supervisor (MPHOS) 146 4.3 From Supervisor to Controller 147 4.4 DCSynth Specification and Controller Synthesis 148 5 Case Studies and Experiments 149 5.1 Types of Controller Specification 149 5.2 Performance Metrics: Measuring Quality of Controllers 150 5.3 Case Studies: Mine-Pump and Arbiter Specifications 151 5.4 Experimental Evaluation 152 6 Discussion Along with Related Work 154 7 Conclusions 155 References 155 Refinement Type Contracts for Verification of Scientific Investigative Software 158 1 Introduction 158 2 Motivating Examples 160 3 Package Summary 163 3.1 Refinement Types 163 3.2 Entry and Exit Conditions 163 3.3 Syntax 164 3.4 Automated Testing 164 4 Performance Evaluation 165 5 Case Study 166 5.1 Detecting Errors in PyDDM 166 5.2 Detecting Errors Using Traditional Methodology 167 5.3 Detecting Errors in User Code 168 6 Limitations 168 7 Related Work 169 8 Conclusions and Future Directions 170 References 172 solc-verify: A Modular Verifier for Solidity Smart Contracts 176 1 Introduction 176 2 Background 178 3 Overview and Features 179 4 Translation Details and Properties 181 5 Examples and Experiments on Real World Contracts 184 5.1 Language Coverage 185 5.2 Unannotated Contracts 185 5.3 Annotated Contracts 188 6 Related Work 190 7 Conclusion 191 References 191 Intersection and Rotation of Assumption Literals Boosts Bug-Finding 195 1 Introduction 195 2 Preliminaries 197 2.1 SAT with Assumptions 197 2.2 Complementary Approximate Reachability 198 3 Algorithm and Proposed Heuristics 198 3.1 Algorithm Description 198 3.2 Intersection and Rotation Heuristics 200 4 Performance Evaluation 201 4.1 Experiment Set-Up 202 4.2 Experimental Results 203 5 Discussion and Future Work 204 References 206 Author Index 208