HVC 2011
Haifa Verification Conference 2011
December 6-8, 2011
Tutorials: December 5, 2011
Organized by IBM R&D Labs in Israel
Conference program PDF version for printing, day 1 (68 KB) Conference program PDF version for printing, day 2 (62 KB) Conference program PDF version for printing, day 3 (65 KB)
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
Proceedings Publication
Springer Lecture Notes in Computer Science
HVC 2011 Poster
