Date: Wednesday 20 March 2013
Time: 14:30 - 16:00
Location / Room: Belle-Etoile

Chair:
Christoph Scholl, University of Freiburg, DE

Co-Chair:
Jason Baumgartner, IBM, US

The session covers an application of formal methods to the verification of Transactional Memories as well as techniques to broaden the scope of modern core verification techniques. The first paper presents a formal model for Hybrid Transactional Memories and a correctness proof based on this formalization. The second paper extends IC3 / PDR (a recent, highly successful method for model checking by incrementally building inductive invariants) from Boolean formulas to quantifier-free formulas with bit vectors. Finally, the third paper presents a method for semi-canonical labeling And Inverter Graphs which aims at speeding-up sequential verification by identifying isomorphic structures.

Time	Label	Presentation Title Authors
14:30	7.2.1	VERIFYING SAFETY AND LIVENESS FOR THE FLEXTM HYBRID TRANSACTIONAL MEMORY Authors: Parosh Abdulla1, Sandhya Dwarkadas2, Ahmed Rezine3, Arrvindh Shriraman4 and Yunyun Zhu1 1Uppsala University, SE; 2Rochester University, US; 3Linköping University, SE; 4Simon Fraser University, CA Abstract
15:00	7.2.2	QF_BV MODEL CHECKING WITH PROPERTY DIRECTED REACHABILITY Authors: Tobias Welp1 and Andreas Kuehlmann2 1University of California, Berkeley, US; 2Coverity, US Abstract
15:30	7.2.3	A SEMI-CANONICAL FORM FOR SEQUENTIAL AIGS Authors: Alan Mishchenko1, Niklas Een1, Robert Brayton1, Michael Case2, Pankaj Chauhan2 and Nikhil Sharma2 1University of California, Berkeley, US; 2Calypto Design Systems, US Abstract
16:00	IP3-8, 651	FAST CONE-OF-INFLUENCE COMPUTATION AND ESTIMATION IN PROBLEMS WITH MULTIPLE PROPERTIES Authors: Carmelo Loiacono1, Marco Palena1, Paolo Pasini1, Denis Patti1, Stefano Quer1, Stefano Ricossa1, Danilo Vendraminetto1 and Jason Baumgartner2 1Politecnico di Torino, IT; 2IBM Research, US Abstract
16:01	IP3-9, 488	USING CUBES OF NON-STATE VARIABLES WITH PROPERTY DIRECTED REACHABILITY Authors: John Backes and Marc Riedel, University of Minnesota, US Abstract
16:02	IP3-10, 214	BRIDGING THE GAP BETWEEN DUAL PROPAGATION AND CNF-BASED QBF SOLVING Authors: Alexandra Goultiaeva1, Martina Seidl2 and Armin Biere2 1University of Toronto, CA; 2Johannes Kepler University, AT Abstract
16:00		End of session Coffee Break in Exhibition Hall Monday and Friday morning and afternoon coffee breaks will be located in the Salle de Reception. On Tuesday-Thursday the breaks will be located in the Exhibition Hall. Morning and afternoon (with the exception of Thursday afternoon which is a 30 minute break) coffee breaks on Tuesday-Thursday are extended breaks and will run for 60 minutes (coffee points will be open for the first 30 minutes only) from the start time indicated in the programme.