Accepted Papers

  • Youngjoo Kim, Moonzoo Kim and Taihyo Kim. Statistical Model Checking for Safety Critical Hybrid Systems: An Empirical Evaluation
  • Dima Elenbogen, Shmuel Katz and Ofer Strichman. Proving Mutual Termination of Programs
  • John Paul, Elena Guralnik, Anatoly Koyfman, Amir Nahir and Subrat K Panda. Leveraging Accelerated Simulation for Floating-Point Regression
  • Alexander Ivrii, Arie Matsliah and Hana Chockler. Computing Interpolants without Proofs
  • Marcela Simkova and Ondrej Lengal. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures
  • Saddek Bensalem, Marius Bozga, Doron Peled and Jean Quilbeuf. Knowledge Based Transactional Behavior
  • Vijay Ganesh, Mia Minnes, Armando Solar-Lezama and Martin Rinard. Word equations with length constraints: what's decidable?
  • Norbert Manthey, Marijn Heule and Armin Biere. Automated Reencoding of Boolean Formulas
  • Vasco Pessanha, Ricardo Dias and João Lourenço. Precise Detection of Atomicity Violations
  • Yoav Katz, Michal Rimon and Avi Ziv. A Novel Approach for Implementing Microarchitectural Verification Plans in Processor Designs
  • Roderick Bloem, Rolf Drechsler, Goerschwin Fey, Alexander Finder, Georg Hofferek, Robert Koenighofer, Jaan Raik, Urmas Repinski and Andre Suelflow. FoREnSiC - An Automatic Debugging Environment for C Programs
  • Shucheng Zhu, Georg Weissenbacher and Sharad Malik. Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation
  • Tamer Salman, Allon Adir, Alex Goryachev, Lev Greenberg and Gil Shurek. A New Test-Generation Methodology for System-Level Verification of Production Processes
  • Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider and Helen Treharne. Defining and Model Checking Abstractions of Complex Railway Models using CSP||B
  • Antonio Morgado, Mark Liffiton and Joao Marques-Silva. MaxSAT-Based MCS Enumeration
  • Orna Kupferman and Sigal Weiner. Environment-Friendly Safety
  • Robert Koenighofer and Roderick Bloem. Repair with On-The-Fly Program Analysis
  • Kristin Yvonne Rozier and Moshe Vardi. Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking

play gallery

HVC 2012 Photo gallery

Keynote speakers

Previous Conferences

As in previous years, the post-conference proceedings will be published in Springer's Lecture Notes in Computer Science series (LNCS).

HVC 2012 Poster

HVC 2012 Poster

See us on Linked In See us on Facebook