Verified Software. Theories, Tools, and Experiments: 10th International Conference, VSTTE 2018, Oxford, UK, July 18–19, 2018, Revised Selected PapersRuzica Piskac, Philipp Rümmer This volume constitutes the thoroughly refereed post-conference proceedings of the 10th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018, held in Oxford, UK, in July 2018. The 19 full papers presented were carefully revised and selected from 24 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. |
Contents
| 1 | |
| 17 | |
Extending VIAP to Handle Array Programs | 38 |
LatticeBased Refinement in Bounded Model Checking | 50 |
Verified Certificate Checking for Counting Votes | 69 |
Program Verification in the Presence of IO | 88 |
A Certifying Abstract Machine for Logic Programs | 112 |
A Java Bytecode Formalisation | 135 |
Verifying TimeBalancing of Cryptosystems | 215 |
A Formalization of Core of Solidity | 229 |
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms | 248 |
Practical Methods for Reasoning About Java 8s Functional Programming Features | 267 |
Verification of Binarized Neural Networks via Interneuron Factoring | 279 |
The Map Equality Domain | 291 |
Loop Detection by Logically Constrained Term Rewriting | 309 |
Store Buffer Reduction in the Presence of MixedSize Accesses and Misalignment | 322 |
Formalising Executable Specifications of LowLevel Systems | 155 |
A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars | 177 |
Constructing Independently Verifiable PrivacyCompliant Type Systems for Message Passing Between BlackBox Components | 196 |
Other editions - View all
Verified Software. Theories, Tools, and Experiments: 10th International ... Ruzica Piskac,Philipp Rümmer No preview available - 2018 |
Common terms and phrases
ABNF grammar abstract accesses ACL2 algorithm array bytecode bytes CakeML candidates certificate compiler computation constraints constructor control flow control flow graph correctness counterexample data flow graph data flow proofs data flow trees defined definition denote domain element example execution expressions file system first-order logic formal formalisation framework functional programming Heidelberg HMAC Hoare logic implementation induction input instruction integer Java Java bytecode Lemma LLVM Lmin LNCS logic loop machine MapReduce meet semilattice memory barrier model checking modifier natural numbers operational semantics operations output parse tree parser parsing pointer Programming Languages properties prove recursive result rewrite rules Sect semantics semilattice shallow embedding SideTrail smart contracts SMT solver specification Springer store buffer syntax term of type theorem thread time-balancing tool translation TWAM type system valid variables verification weak equivalence write