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. |