Haifa Verification Conference 2012 (HVC 2012)

Nov 6
• David Harel On Behavioral Programming

Session 1: Software Testing and Verification
• Vasco Pessanha, Ricardo Dias, and João Lourenço Precise Detection of Atomicity Violations
• Dima Elenbogen, Shmuel Katz, and Ofer Strichman Proving Mutual Termination of Programs
• Saddek Bensalem, Marius Bozga, Doron Peled, and Jean Quilbeuf Knowledge-Based Transactional Behavior

Session 2: Software Testing and Verification, Poster Promos
• 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
• Robert Koenighofer and Roderick Bloem Repair with on-the-fly Program Analysis

Session 3: SAT
• Alexander Ivrii, Arie Matsliah, and Hana Chockler Computing Interpolants without Proofs
• Antonio Morgado, Mark Liffiton, and João Marques-Silva MaxSAT-Based MCS Enumeration
• Norbert Manthey, Marijn Heule, and Armin Biere Automated Reencoding of Boolean Formulas
• Phillip James, Arnold Beckmann and Markus Roggenbach Using Domain Specific Languages to Support Verification in the Railway Domain
• Guillermo Rodriguez-Navas, Patrick Graydon and Iain Bate From Fault Injection to Mutant Injection: the Next Step for Safety Analysis?
• Magdalena Widl Test Case Generation by Grammar-based Fuzzing for Model-driven Engineering

Nov 7
• Edward Lee Verifying Real-Time Software Is Not Reasonable (Today)

Session 4: Hardware Verification and Validation
• John Paul, Elena Guralnik, Anatoly Koyfman, Amir Nahir, and Subrat K Panda Leveraging Accelerated Simulation for Floating-Point Regression
• Shucheng Zhu, Georg Weissenbacher, and Sharad Malik Coverage-based Trace Signal Selection for Fault Localisation in Post-Silicon Validation
• Yoav Katz, Michal Rimon, and Avi Ziv A Novel Approach for Implementing Microarchitectural Verification Plans in Processor Designs
• Marcela Simkova and Ondrej Lengal Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures

Session 5: Systems Engineering
• Youngjoo Kim, Moonzoo Kim, and Taihyo Kim Statistical Model Checking for Safety Critical Hybrid Systems: An Empirical Evaluation
• 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
• Orna Raz Reducing Costs While Increasing Quality

Nov 8
• Nikolaj Bjorner SMT in Verification, Modeling, and Testing at Microsoft

Session on Security Verification
• Ofer Maor A Vulnerability or a Bug? What's the Difference Anyway? Security Software Verification as Part of the Development Lifecycle
• Jamil Mazzawi Formal Analysis of Security Data Paths in RTL Design
• Ryan Kastner Simultaneous Information Flow Security and Circuit Redundancy in Boolean Gates

Session 6: Formal Methods
• Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin Rinard Word Equations with Length Constraints: What's Decidable?
• Orna Kupferman and Sigal Weiner Environment-Friendly Safety
• Kristin Yvonne Rozier and Moshe Vardi Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking