FMCAD15 PROGRAM
Days: Sunday, September 27th Monday, September 28th Tuesday, September 29th Wednesday, September 30th
Sunday, September 27th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:15 Session 34: Tutorial by André Platzer (joint with SAT 2015)
| 09:00 | Proving Hybrid Systems ( abstract ) |
10:15-10:30Coffee Break
10:30-11:45 Session 35: Tutorial by Priyank Kalla (joint with SAT 2015)
| 10:30 | Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation ( abstract ) |
11:45-13:45Lunch Break
13:45-15:15 Session 36: Tutorial by Roderick Bloem (joint with SAT 2015)
| 13:45 | Reactive Synthesis ( abstract ) |
15:15-15:45Coffee Break
15:45-17:15 Session 37: Tutorial by Isil Dillig (joint with SAT 2015)
| 15:45 | Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis ( abstract ) |
Monday, September 28th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:00-10:30Coffee Break
10:30-12:00 Session 40: Invariant Generation
Chair:
| 10:30 | Compositional Safety Verification with Max-SMT ( abstract ) |
| 11:00 | Accelerating Invariant Generation ( abstract ) |
| 11:30 | Compositional Recurrence Analysis ( abstract ) |
12:00-13:30Lunch Break
15:30-16:00Coffee Break
16:00-17:30 Session 42: Use of SMT Solvers & Decision Procedures
Chair:
| 16:00 | Theory-Aided Model Checking of Concurrent Transition Systems ( abstract ) |
| 16:30 | Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays ( abstract ) |
| 17:00 | Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs ( abstract ) |
Tuesday, September 29th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:00-10:30Coffee Break
10:30-12:30 Session 45: SAT, SMT, QBF: Development
Chair:
| 10:30 | Better Lemmas with Lambda Extraction ( abstract ) |
| 11:00 | A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas ( abstract ) |
| 11:30 | CAQE: A Certifying QBF Solver ( abstract ) |
| 12:00 | Universal Boolean Functional Vectors ( abstract ) |
12:30-14:00Lunch Break
14:00-16:00 Session 46: (a) IC3 (b) Applications and Case Studies
Chair:
| 14:00 | Pushing to the Top ( abstract ) |
| 14:30 | IC3 Software Model Checking on Control Flow Automata ( abstract ) |
| 15:00 | Comparing Different Functional Allocations in Automated Air Traffic Control Design ( abstract ) |
| 15:30 | Compositional Reasoning Gotchas in Practice ( abstract ) |
16:00-16:30Coffee Break
Wednesday, September 30th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-11:00 Session 48: Concurrency and Multi-Agent Protocols
Chair:
| 09:00 | Pattern-based Synthesis of Synchronization for the C++ Memory Model ( abstract ) |
| 09:30 | An SMT-based Approach to Fair Termination Analysis ( abstract ) |
| 10:00 | Verification of Cache Coherence Protocols wrt. Trace Filters ( abstract ) |
| 10:30 | Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols ( abstract ) |
11:00-11:30Coffee Break
13:00-14:30Lunch Break
15:00-16:30 Session 51: Circuit Verification and Synthesis
Chair:
| 15:00 | Template-based Synthesis of Instruction-Level Abstractions for SoC Verification ( abstract ) |
| 15:30 | Reverse Engineering with Simulation Graphs ( abstract ) |
| 16:00 | Formal Verification of Automatic Circuit Transformations for Fault-Tolerance ( abstract ) |