Note: All events are in the Trinity Room of the
Renaissance Austin Hotel unless stated otherwise.
|
Sunday, November 11 Conference, Day 1 |
||
| Tutorials Day, Chair: Natasha Sharygina (University of Lugano) | ||
| 8:15-8:45 | Breakfast | |
| 8:45-9:00 | Jason Baumgartner
and Mary Sheeran |
Welcome and Opening Remarks |
| 9:00-10:00 | Robert Brayton | The Synergy between Logic Synthesis and
Equivalence Checking [slides] |
| 10:00-10:30 | Break | |
| 10:30-12:00 | Farid Najm | Power Management for VLSI Circuits and the
Need for High-Level Power Modeling and Design Exploration
[slides] |
| 12:00-13:30 | Lunch
Location: Arbor Room (Renaissance Austin Hotel) | |
| 13:30-15:00 | Niklas Een | Practical SAT [slides] |
| 15:00-15:30 | Break | |
| 15:30-17:00 | Randal E. Bryant | Modeling Data in Formal Verification:
Bits, Bit Vectors, or Words [slides] |
| 17:00-17:30 | Break | |
| Panel Discussion, Moderator: Aarti Gupta (NEC) | ||
| 17:30-19:00 | Robert Kurshan, Hillel Miller, Rajeev Ranjan, Harry Foster, Husam Abu-Haimed, Prakash Narain | Formal Verification: A
Business Perspective [slides: Gupta, Kurshan, Ranjan, Foster, Abu-Haimed, Narain] |
| 19:00 | Reception Location: Sabine Room (Renaissance Austin Hotel) | |
| Monday,
November 12 Conference, Day 2 | ||
| 8:15-9:00 | Breakfast | |
| Invited Talk, Chair: Alan Hu (University of British Columbia) | ||
| 9:00-10:00 | Eli Singerman | Verification of Embedded Software in
Industrial Microprocessors [slides] |
| 10:00-10:30 | Break | |
| Session 1: SAT-Based Methods, Chair: Miroslav Velev (Consultant) | ||
| 10:30-11:00 | Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, and Marsha Chechik | Exploiting Resolution Proofs to
Speed Up LTL Vacuity Detection for BMC [slides] |
| 11:00-11:30 | Sean Safarpour, Mark Liffiton, Hratch Mangassarian, Andreas Veneris, and Karem Sakallah | Improved
Design Debugging using Maximum Satisfiability [slides] |
| 11:30-12:00 | Daher Kaiss, Marcelo Skaba, Ziyad Hanna, and Zurab Khasidashvili | Industrial Strength SAT-based
Alignability Algorithm for Hardware Equivalence Verification
[slides] |
| 12:00-12:30 | Frank Hutter, Domagoj Babic, Holger Hoos, and Alan Hu | Boosting Verification by Automatic
Tuning of Decision Procedures [slides] |
| 12:30-14:00 | Lunch Location: Arbor Room (Renaissance Austin Hotel) | |
| Session 2: High-Level System Analysis, Chair: Alper Sen (Freescale) | ||
| 14:00-14:30 | Ariel Cohen, John O'Leary, Amir Pnueli, Mark Tuttle, and Lenore Zuck | Verifying Correctness of
Transactional Memories [slides] |
| 14:30-15:00 | Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, and Richard Trefler | Algorithmic Analysis of Piecewise
FIFO Systems [slides] |
| 15:00-15:30 | Xiaofang Chen, Steven German, and Ganesh Gopalakrishnan | Transaction Based Modeling and
Verification of Hardware Protocol Implementations [slides] |
| 15:30-15:45 | Yogesh Mahajan and Sharad Malik | Automating Hazard
Checking in Transaction-Level Microarchitecture Models
[slides] |
| 15:45-16:15 | Break | |
| Session 3: Abstraction-Based Methods, Chair: Malay Ganai (NEC) | ||
| 16:15-16:45 | Roberto Cavada, Alessandro Cimatti, Anders Franzen, Kalyanasundaram Krishnamani, Marco Roveri, and R. K. Shyamasundar | Computing Abstractions by
integrating BDDs and SMT [slides] |
| 16:45-17:15 | Chao Wang, Aarti Gupta, and Franjo Ivancic |
Induction
in CEGAR for Detecting Counterexamples [slides] |
| 17:15-17:30 | Daniel Kroening and Georg Weissenbacher | Lifting
Propositional Interpolants to the Word-Level [slides] |
|
Tuesday, November 13 Conference, Day 3 |
||
| 8:15-9:00 | Breakfast | |
| Session 1: Software Analysis Methods, Chair: Kathi Fisler (WPI) | ||
| 9:00-9:30 | Fadi Zaraket, John Pape, Margarida Jacome, Adnan Aziz, and Sarfraz Khurshid | COSE: a Technique for
Co-optimizing Embedded Systems [slides] |
| 9:30-10:00 | Hana Chockler, Benny Godlin, Eitan Farchi, and Sergey Novikov | Cross-Entropy Based Testing
[slides] |
| 10:00-10:30 | Break | |
| Session 2: Panel Discussion, Moderator: William Joyner (SRC) | ||
| 10:30-12:30 | Robert Jones, Andreas Kuehlmann, Carl Pixley | FMCAD2027: Will the
'FM' Have a Real Impact on the 'CAD'? [slides: Joyner, Kuehlmann, Pixley] |
| 12:30-14:00 | Lunch
Location: Arbor Room (Renaissance Austin Hotel) |
|
| Session 3: Symbolic Trajectory Evaluation, Chair: Koen Claessen (Chalmers) | ||
| 14:00-14:30 | Yan Chen, Yujing He, Fei Xie, and Jin Yang | Automatic Abstraction Refinement
for Generalized Symbolic Trajectory Evaluation [slides] |
| 14:30-15:00 | Edward Smith | A Logic for GSTE [slides] |
| 15:00-15:30 | Sara Adams, Magnus Bjork, Tom Melham, and Carl-Johan Seger | Automatic Abstraction in Symbolic
Trajectory Evaluation [slides] |
| 15:30-16:00 | Break | |
| Session 4: Specification Theory, Chair: Tom Melham (Oxford University) | ||
| 16:00-16:30 | Koen Claessen | A Coverage Analysis for Safety
Property Lists [slides] |
| 16:30-17:00 | Orna Kupferman and Yoad Lustig | What triggers a
behavior? [slides] |
| 17:00-17:15 | Kathi Fisler | Two-Dimensional Regular Expressions
for Compositional Bus Protocols [slides] |
| 17:15-17:30 | Martin Oberkönig, Martin Schickel, and Hans Eveking | A Quantitative Completeness
Analysis for Property-Sets [slides] |
| 17:30-18:30 | All | Business Meeting |
| 19:00 | Conference Banquet Location: Ventana at Texas Culinary Academy 11400 Burnet Road Suite 2100, Austin, TX 78758 | |
|
Wednesday, November 14 Conference, Day 4 |
||
| 8:15-9:00 | Breakfast | |
| Invited Talk, Chair: Jeremy Levitt (Mentor) | ||
| 9:00-10:00 | Wolfgang Kunz | Formal Verification of Systems-on-Chip -
Industrial Experiences and Scientific
Perspectives [slides] |
| 10:00-10:30 | Break | |
| Session 1: Industrial-Strength Verification, Chair: Rajeev Ranjan (Jasper) | ||
| 10:30-11:00 | Michael Case, Alan Mishchenko, and Robert Brayton | Automated Extraction of Inductive
Invariants to Aid Model Checking [slides] |
| 11:00-11:30 | Aaron Bradley and Zohar Manna | Checking Safety by
Inductive Generalization of Counterexamples to Induction
[slides] |
| 11:30-12:00 | Aaron Hurst, Alan Mishchenko, and Robert Brayton | Fast Minimum Register Retiming Via
Binary Maximum-Flow [slides] |
| 12:00-12:15 | Adrian Seigler, Gary Van Huben, and Hari Mony | Formal Verification of Partial Good
Self-Test Fencing Structures [slides] |
| 12:15-12:30 | Alon Flaisher, Alon Gluska, and Eli Singerman | Case study: Integrating FV and DV
within the Verification of Intel(r) Core(TM)2
Microprocessor [slides] |
| 12:30-14:00 | Lunch
Location: Arbor Room (Renaissance Austin Hotel) |
|
| Session 2: Reasoning about Physical Systems, Chair: Daniel Kroenig (ETH Zurich) | ||
| 14:00-14:30 | Chao Yan and Mark Greenstreet | Circuit-Level
Verification of a High-Speed Toggle [slides] |
| 14:30-15:00 | Mohamed Zaki, Ghiath Al Sammane, Sofiene Tahar, and Guy Bois | Combining Symbolic Simulation and
Interval Arithmetic for the Verification of AMS Designs [slides] |
| 15:00-15:15 | Neha Rungta, Hyrum Carroll, Eric Mercer, Randall Roper, Mark Clement, and Quinn Snell | Analyzing
Gene Relationships for Down Syndrome with Labeled Transitions
Graphs [slides] |
| 15:15-15:45 | Break | |
| Session 3: Advanced Theorem-Proving Applications, Chair: Warren Hunt (University of Texas) | ||
| 15:45-16:15 | Julien Schmaltz | A Formal Model of Clock Domain
Crossing and Automated Verification of Time-Triggered
Hardware [slides] |
| 16:15-16:45 | Lee Pike | Modeling Time-Triggered Protocols and
Verifying their Real-Time Schedules [slides] |
| 16:45-17:00 | Sandip Ray and Jayanta Bhadra | A Mechanized Refinement
Framework for Analysis of Custom Memories [slides] |