Skip to main content

HVC 2011
Haifa Verification Conference 2011

Tutorial day: Monday, 5 December, 2011

9:00 Registration

9:30 Estimating and Modeling VVT Cost, Time and Risks of Engineered Systems (part 1),
Avner Engel

11:00 Break

11:30 Estimating and Modeling VVT Cost, Time and Risks of Engineered Systems (part 2), Avner Engel

13:00 Lunch

14:00 Regression Verification: Verifying the Equivalence of Similar Programs,
Ofer Strichman

15:30 Break

16:00 Combinatorial Test Design,
Rachel Tzoref-Brill

18:00 End of tutorial day


Day 1: Tuesday, 6 December, 2011

9:00 Registration

9:30 Openning

10:00 Invited Speaker: Pioneering the Future of Verification: A Spiral of Technological and Business Innovation,
Kathryn Kranen, President and Chief Executive Officer, Jasper Design Automation

11:00 Break

Technical Session 1 - Synthesis

11:30 Generalized Reactivity(1) Synthesis without a Monolithic Strategy,
Matthias Schlaipfer, Georg Hofferek, and Roderick Bloem IAIK, Graz University of Technology

12:00 Synthesis with Clairvoyance,
Orna Kupferman, Dorsa Sadigh, and Sanjit Seshia, Hebrew University and UC Berkeley

Experience & tools 1
12:30 Injecting Floating-Point Testing Knowledge into Test Generators,
Merav Aharoni, Emanuel Gofman, Elena Guralnik and Anatoly Koyfman, IBM

12:45 Poster Promos

13:00 Lunch

14:30 Invited Speaker: Automated Detection and Repair of Concurrency Bugs,
Ben Liblit, University of Wisconsin–Madison

15:30 Break

Technical Session 2 - Formal Verification 1

16:00 Predicting Serializability Violations: SMT-based Search vs. DPOR-based Search,
Arnab Sinha, Sharad Malik, Chao Wang, and Aarti Gupta, Princeton University, Virginia Polytechnic Institute and NEC Labs America

16:30 Implicative Simultaneous Satisfiability and Applications,
Zurab Khasidashvili and Alexander Nadel, Intel

17:00 Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads,
Marijn Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere, TU Delft, Swansea University, Aalto University, and Johannes Kepler University

17:30 Break

18:00 Student Posters Event & Cocktail


Day 2: Wednesday, 7 December, 2011

9:00 Registration

09:30 Invited Speaker: Verification Challenges of Workload Optimized Hardware Systems,
Klaus-Dieter Schubert, IBM Deutschland Research and Development GmbH

10:30 Break

Technical Session 3 - Software Quality

11:00 Concurrent Small Progress Measures,
Michael Huth, Jim Huan-Pu Kuo, and Nir Piterman, Imperial College London and University of Leicester

11:30 SAM: Self-adaptive Dynamic Analysis for Multithreaded Programs,
Qichang Chen, Liqiang Wang, and Zijiang Yang, University of Wyoming

12:00 Can File Level Characteristics Help Identify System Level Fault-Proneness?,
Elaine Weyuker and Thomas Ostrand, AT&T Labs - Research

12:30 Specification and Quantitative Analysis of Probabilistic Cloud Deployment Patterns,
Kenneth Johnson, Simon Reed, and Radu Calinescu, Aston University

13:00 Lunch

14:30 Excursion


Day 3: Thursday, 8 December, 2011

9:00 Registration

09:30 Invited Speaker: Preprocessing and Inprocessing Techniques in SAT,
Armin Biere, Johannes Kepler University, Linz

10:30 Break

Technical Session 4 - Testing and Coverage

11:00 Dynamic Test Data Generation for Data Intensive Applications,
Tamer Salman, Allon Adir, and Ronen Levy, IBM

11:30 Symbolic Testing of OpenCL Code,
Peter Collingbourne, Cristian Cadar, and Paul Kelly, Imperial College London

12:00 Reverse Coverage Analysis,
Ariel Birnbaum, Laurent Fournier, Steve Mittermaier, and Avi Ziv, IBM

Experience & tools 2
12:30 HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware,
Marcela Simkova, Ondrej Lengal and Michal Kajan, Brno University of Technology

12:45 Combining Theorem Proving and Symbolic Trajectory Evaluation in THM&STE,
Yongjian Li, Naiju Zeng, William Hung and Xiaoyu Song, Chinese Academy of Sciences, Synopsys Inc. and Portland State University

13:00 Lunch

14:30 HVC Award

15:30 Break

Technical Session 5 - Formal Verification 2

16:00 Liveness vs Safety - a practical viewpoint,
B. A. Krishna, Jonathan Michelson, Vigyan Singhal, and Alok Jain, Chelsio Communications Inc, Cisco Systems, Oski Technology, and Cadence Design Systems

16:30 IIS-Guided DFS For Efficient Bounded Reachability Analysis of Linear Hybrid Automata,
Lei Bu, Yang Yang, and Xuandong Li, Nanjing University

17:00 Interpolation-based Function Summaries in Bounded Model Checking,
Ondrej Sery, Grigory Fedyukovich, and Natasha Sharygina, University of Lugano

17:30 Best paper award + Closing

Contact Information

Proceedings Publication

Springer Lecture Notes in Computer Science

HVC 2011 Poster

HVC 2011 Poster