Hardware and Software: Verification and Testing

1. Front Matter

   Pages I-XXII

   PDF

2. Full Papers

   1. Front Matter

      Pages 1-1

      PDF

   2. A Framework for Asynchronous Circuit Modeling and Verification in ACL2

      • Cuong Chau, Warren A. Hunt Jr., Marly Roncken, Ivan Sutherland

      Pages 3-18

   3. Modeling Undefined Behaviour Semantics for Checking Equivalence Across Compiler Optimizations

      • Manjeet Dahiya, Sorav Bansal

      Pages 19-34

   4. Deferrability Analysis for JavaScript

      • Johannes Kloos, Rupak Majumdar, Frank McCabe

      Pages 35-50

   5. A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models

      • Tatsuya Abe

      Pages 51-66

   6. Trace-based Analysis of Memory Corruption Malware Attacks

      • Zhixing Xu, Aarti Gupta, Sharad Malik

      Pages 67-82

   7. Trace-Based Run-Time Analysis of Message-Passing Go Programs

      • Martin Sulzmann, Kai Stadtmüller

      Pages 83-98

   8. Software Verification: Testing vs. Model Checking

      • Dirk Beyer, Thomas Lemberger

      Pages 99-114

   9. A Supervisory Control Algorithm Based on Property-Directed Reachability

      • Koen Claessen, Jonatan Kilhamn, Laura Kovács, Bengt Lennartson

      Pages 115-130

   10. SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems

       • Fedor Shmarov, Nicola Paoletti, Ezio Bartocci, Shan Lin, Scott A. Smolka, Paolo Zuliani

       Pages 131-146

   11. A Symbolic Approach to Safety ltl Synthesis

       • Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi

       Pages 147-162

   12. An Interaction Concept for Program Verification Systems with Explicit Proof Object

       • Bernhard Beckert, Sarah Grebing, Mattias Ulbrich

       Pages 163-178

   13. PRuning Through Satisfaction

       • Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere

       Pages 179-194

   14. LRA Interpolants from No Man’s Land

       • Leonardo Alt, Antti E. J. Hyvärinen, Natasha Sharygina

       Pages 195-210

3. Tool Papers

   1. Front Matter

      Pages 211-211

      PDF

   2. ACAT: A Novel Machine-Learning-Based Tool for Automating Android Application Testing

      • Ariel Rosenfeld, Odaya Kardashov, Orel Zang

      Pages 213-216

   3. MicroTESK: Specification-Based Tool for Constructing Test Program Generators

      • Mikhail Chupilko, Alexander Kamkin, Artem Kotsynyak, Andrei Tatarnikov

      Pages 217-220

   4. Embedded Functions for Test Design Automation

      • George B. Sherwood

      Pages 221-224

   5. KERIS: A CT Tool of the Linux Kernel with Dynamic Memory Analysis Capabilities

      • Bernhard Garn, Fabian Würfl, Dimitris E. Simos

      Pages 225-228

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.

• Model checking
• Coverage metrics
• Equivalence checking
• Semi-formal verification
• Simulation and emulation
• Transaction-level verification
• Theorem proving and SAT solving
• Assertion checking
• Software testing and debugging
• Formal software verification

• Technion - Israel Institute of Technology, Haifa, Israel

  Ofer Strichman

• IBM Research Lab, Haifa, Israel

  Rachel Tzoref-Brill

Policies and ethics