Hardware and Software: Verification and Testing: 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, ProceedingsOfer Strichman, Rachel Tzoref-Brill This book constitutes the refereed proceedings of the 13th International Haifa Verification Conference, HVC 2017, held in Haifa, Israel in November 2017.The 13 revised full papers presented together with 4 poster and 5 tool demo papers were carefully reviewed and selected from 45 submissions. They are dedicated to advance the state of the art and state of the practice in verification and testing and are discussing future directions of testing and verification for hardware, software, and complex hybrid systems. |
Contents
1 A Framework for Asynchronous Circuit Modeling and Veri cation in ACL2 | 3 |
2 Modeling unde ned behaviour semantics for checking equivalence across compiler optimizations | 19 |
3 Deferrability Analysis for JavaScript | 35 |
4 A Veri er of Directed Acyclic Graphs for Model Checking with Memory Consistency Models | 51 |
5 Tracebased Analysis of Memory Corruption Malware Attacks | 67 |
6 TraceBased RunTime Analysis of MessagePassing Go Programs | 83 |
Testing vs Model Checking A Comparative Evaluation of the State of the Art | 99 |
8 A Supervisory Control Algorithm Based on PropertyDirected Reachability | 115 |
Tool Papers | 211 |
A Novel MachineLearningBased Tool For Automating Android Application Testing | 212 |
Speci cationBased Tool for Constructing Test Program Generators | 217 |
16 Embedded functions for test design automation | 221 |
A CT Tool of the Linux Kernel with Dynamic Memory Analysis Capabilities | 225 |
Relational Analysis Tool for Concurrent Programs | 229 |
Posters | 234 |
19 More adaptive does not imply less safe with formal verification | 235 |
9 SMTbased Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems | 131 |
10 A Symbolic Approach to Safety LTL Synthesis | 147 |
11 An Interaction Concept for Program Verification Systems with Explicit Proof Object | 163 |
12 PRuning Through Satisfaction? | 179 |
13 LRA Interpolants from No Mans Land | 195 |
a Light Weight Testing Tool for Protocols with Complex Messages | 241 |
21 Towards Veri cation of Robot Design for Selflocalization | 245 |
22 Probabilistic Model of ControlFlow Altering based Malicious Attacks Poster submission | 249 |
| 253 | |
Other editions - View all
Hardware and Software: Verification and Testing: 13th International Haifa ... Ofer Strichman,Rachel Tzoref-Brill No preview available - 2017 |
Common terms and phrases
Abstract alias analysis analysis application approach assignment assumptions asynchronous Asynchronous Circuits attack autarky automated automatically basic block behavior benchmark boolean bugs checkers compiler compiler optimizations Computer constraints construction corresponding debugging defer defined denote dynamic encoding equivalence evaluation event example finite formal framework function implementation input instructions interaction interpolation interpolation algorithm LLVM LNCS loading loop loop invariants LTL formula LTL synthesis malicious malware MCMs memory segments method model checking module nodes non-deterministic optimization output parameters PDRC performance PID controller pointer positive reduct PR clauses problem Proc program graphs program verification proof goals proof script RATCOP reachability safety game Safety LTL satisfies scripting language semantics sequence set-blocked SI-LRA simulation relation SMT solver software model checking solving specification Springer International Publishing strategy Strichman symbolic techniques Theorem thread transition undefined behaviour unit propagation validation variables vector clock VeriDAG wcon