SAT 2015: 18TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
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

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