Date: Thursday 21 March 2013
Time: 11:00 - 12:30
Location / Room: Chartreuse

Chair:
Fahim Rahim, Atrenta, FR

Co-Chair:
Julian Schmaltz, Open University of the Netherlands, NL

Automatically computing abstractions of large circuits combined with powerful SAT and SMT solvers is key to the success of formal verification techniques. The papers of this session present significant improvements in abstraction techniques and SAT/SMT-based optimizations. SAT- and SMT-abstractions are guided by unsatisfiable cores. Three papers address the issue of reducing the size of interpolants generated during the construction of abstractions. The second paper proposes a new abstraction technique demonstrating a significant improvement in gate-level abstractions.

Time	Label	Presentation Title Authors
11:00	10.4.1	(Best Paper Award Candidate) GLA: GATE-LEVEL ABSTRACTION REVISITED Authors: Alan Mishchenko1, Niklas Een1, Robert Brayton1, Jason Baumgartner2, Hari Mony2 and Pradeep Nalla3 1University of California, Berkeley, US; 2IBM, US; 3IBM, IN Abstract
11:30	10.4.2	LEMMA LOCALIZATION: A PRACTICAL METHOD FOR DOWNSIZING SMT-INTERPOLANTS Authors: Florian Pigorsch and Christoph Scholl, University of Freiburg, DE Abstract
12:00	10.4.3	CORE MINIMIZATION IN SAT-BASED ABSTRACTION Authors: Anton Belov1, Huan Chen1, Alan Mishchenko2 and Joao Marques-Silva1 1University College Dublin, IE; 2University of California, Berkeley, US Abstract
12:15	10.4.4	OPTIMIZATION TECHNIQUES FOR CRAIG INTERPOLANT COMPACTION IN UNBOUNDED MODEL CHECKING Authors: Gianpiero Cabodi, Carmelo Loiacono and Danilo Vendraminetto, Politecnico di Torino, IT Abstract
12:30	IP5-3, 654	FORMAL ANALYSIS OF STEADY STATE ERRORS IN FEEDBACK CONTROL SYSTEMS USING HOL-LIGHT Authors: Osman Hasan and Muhammad Ahmad, National University of Sciences and Technology, PK Abstract
12:31	IP5-4, 734	A NOVEL CONCURRENT CACHE-FRIENDLY BINARY DECISION DIAGRAM CONSTRUCTION FOR MULTI-CORE PLATFORMS Authors: Mahmoud El-Bayoumi1, Michael Hsiao1 and Mustafa ElNainay2 1Virginia Tech, US; 2Alexanderia University, EG Abstract
12:30		End of session Lunch Break in Ecrins Buffet lunch (Eat early for Smart Cities and Communities Keynote - Room Oisans at 1330; http://www.date-conference.com/conference/session/11.0)