PROGRAM
Days: Monday, September 21st Tuesday, September 22nd Wednesday, September 23rd Thursday, September 24th Friday, September 25th Saturday, September 26th Sunday, September 27th Monday, September 28th Tuesday, September 29th Wednesday, September 30th Thursday, October 1st Friday, October 2nd
Monday, September 21st
View this program: with abstractssession overviewtalk overview
10:00-10:30Coffee Break
10:30-12:00 Session 4: Distributed Systems and Concurrency (MEMOCODE'15)
| 10:30 | Local and Global Fairness in Concurrent Systems ( abstract ) |
| 11:00 | SCEst: Sequentially Constructive Esterel ( abstract ) |
| 11:30 | Design and Verification of Multi-Rate Distributed Systems ( abstract ) |
12:00-12:30 Session 5: Short Papers (MEMOCODE'15)
| 12:00 | Optimized Distributed Implementations of Timed Component-based Systems ( abstract ) |
| 12:10 | Towards Refinement Types for Time-Dependent Data-Flow Networks ( abstract ) |
| 12:20 | C-To-Verilog Translation Validation ( abstract ) |
12:30-14:00Lunch Break
14:00-15:00 Session 6: Design Contest (MEMOCODE'15)
Peter Milder. MEMOCODE 2015 Design Contest: Continuous Skyline Computation
First Place: Kenichi Koizumi, Mary Inaba, Kei Hiraki, University of Tokyo. Efficient Implementation of Continuous Skyline Computation on a Multi-Core Processor
Second Place: Armin Ahmadzadeh, Ehsan Montahaie, Milad Ghafouri, Reza Mirzaei, Saied Rahmani, Farzad Sharif Bakhtiar, Mohsen Gavahi, Rashid Zamanshoar, Hanie Ghasemi, Kianoush Jafari, Saeid Gorgin, Inst. for Research in Fundamental Sciences (IPM), Iran. Efficient Continuous Skyline Computation on Multi-Core Processors Based on Manhattan Distance
15:00-15:30Coffee Break
15:30-17:00 Session 7: Panel -- Formal Methods: How Can We Increase Usage in Practice? (MEMOCODE'15)
Tuesday, September 22nd
View this program: with abstractssession overviewtalk overview
10:00-10:30Coffee Break
10:30-12:00 Session 10: System and Software Modeling and Verification (MEMOCODE'15)
| 10:30 | Modeling and verifying context-aware non-monotonic reasoning agents ( abstract ) |
| 11:00 | Metric Interval Temporal Logic Specification Elicitation and Debugging ( abstract ) |
| 11:30 | Formal validation and verification of a medical software critical component ( abstract ) |
12:00-12:30 Session 11: Short Papers (MEMOCODE'15)
| 12:00 | Hierarchical Multi-Formalism Proofs of Cyber Physical Systems ( abstract ) |
| 12:10 | Modeling Resource Sharing using FSM-SADF ( abstract ) |
| 12:20 | Logic analysis and optimization with quick identification of invariants through one time frame analysis ( abstract ) |
12:30-14:00Lunch Break
14:00-15:30 Session 12: Hardware Design and Test (MEMOCODE'15)
| 14:00 | Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL ( abstract ) |
| 14:30 | Compositional design of asynchronous circuits from behavioural concepts ( abstract ) |
| 15:00 | A Generic Synthesisable Test Bench ( abstract ) |
15:00-15:30Coffee Break
16:00-17:30 Session 13: System and Software Testing, Repair, and Deployment (MEMOCODE'15)
| 16:00 | Passive testing of production systems based on model inference ( abstract ) |
| 16:30 | Model and Program Repair via SAT Solving ( abstract ) |
| 17:00 | On the Deployment Problem of Embedded Systems ( abstract ) |
18:00-21:30 Session : Conference Dinner: Lambert's Downtown Barbecue (MEMOCODE'15)
Bus departs for conference dinner at 18:00
Conference Banquet begins at 18:30, Lambert's Downtown Barbecue, 401 West 2nd St, Austin, TX 78701
Bus returns at 21:30
Wednesday, September 23rd
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 15B: SAT solver analysis (POS15)
Chair:
| 09:00 | Evaluating CDCL Restart Schemes ( abstract ) |
| 09:30 | Predicting SAT Solver Performance on Heterogeneous Hardware ( abstract ) |
09:00-10:00 Session 15C: Invited Talk (QBF 2015)
| 09:00 | Dependency Schemes for Quantified Boolean Formulas ( abstract ) |
10:00-10:30Coffee Break
10:30-12:30 Session 17A: Hardware and Architecture Design and Analysis (MEMOCODE'15)
| 10:30 | Reducing power with activity trigger analysis ( abstract ) |
| 11:00 | Implementing Latency-Insensitive Dataflow Blocks ( abstract ) |
| 11:30 | Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays ( abstract ) |
| 12:00 | Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics ( abstract ) |
10:30-12:00 Session 17B: Work in progress presentations (POS15)
Chair:
| 10:30 | Amoeba-inspired Spatiotemporal Dynamics for Physically Implemented Satisfiability Problem Solvers ( abstract ) |
| 11:00 | Proposal and Application of Search Similarity Index for SAT solver ( abstract ) |
| 11:30 | Model Counting with Arbitrary Alphabets ( abstract ) |
10:30-12:00 Session 17C: Contributed Presentations (QBF 2015)
| 10:30 | Feasible Interpolation for QBF Resolution Calculi ( abstract ) |
| 10:55 | Skolem functions computation for CEGAR based QBF solvers ( abstract ) |
| 11:20 | Reducing Satisfiability and Reachability to DQBF ( abstract ) |
| 11:45 | Discussion ( abstract ) |
12:00-14:00Lunch Break
14:00-15:00 Session 18A: Runtime Verification (MEMOCODE'15)
| 14:00 | Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers ( abstract ) |
| 14:30 | From Signal Temporal Logic to FPGA Monitors ( abstract ) |
14:00-15:00 Session 18B: Unsat proofs and MaxSAT (POS15)
Chair:
| 14:00 | Applications of MaxSAT in Data Analysis ( abstract ) |
| 14:30 | Checking Unsatisfiability Proofs in Parallel ( abstract ) |
15:00-15:30Coffee Break
15:30-17:00 Session 20A: Hybrid Systems Verification (MEMOCODE'15)
| 15:30 | From Non-Zenoness Verification to Termination ( abstract ) |
| 16:00 | Verification Condition Generation for Hybrid Systems ( abstract ) |
| 16:30 | Towards Verification of Hybrid Systems in a Foundational Proof Assistant ( abstract ) |
Thursday, September 24th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 21: Invited Talk (SAT 2015)
Chair:
| 09:00 | Pragmatic Approach to Formal Verification ( abstract ) |
10:00-10:15Coffee Break
10:15-12:15 Session 22: Parallel SAT and #SAT Solving (SAT 2015)
Chair:
| 10:15 | Projected Model Counting ( abstract ) |
| 10:45 | Search-Space Partitioning for Parallelizing SMT Solvers ( abstract ) |
| 11:15 | HordeSat: A Massively Parallel Portfolio SAT Solver ( abstract ) |
| 11:45 | Laissez-Faire Caching for Parallel #SAT Solving ( abstract ) |
12:15-13:45Lunch Break
13:45-15:15 Session 23: CDCL Solving (SAT 2015)
Chair:
| 13:45 | Hints Revealed ( abstract ) |
| 14:15 | Between SAT and UNSAT: The Fundamental Difference in CDCL SAT ( abstract ) |
| 14:45 | Evaluating CDCL Variable Scoring Schemes ( abstract ) |
15:15-15:30Coffee Break
15:30-16:15 Session 24: Competitions and Evaluations (SAT 2015)
Chair:
| 15:30 | SAT Race 2015 ( abstract ) |
| 15:45 | Pseudo-Boolean Evaluation 2015 ( abstract ) |
| 16:00 | Max-SAT Evaluation 2015 ( abstract ) |
Friday, September 25th
View this program: with abstractssession overviewtalk overview
09:00-10:00 Session 25: Invited Talk (SAT 2015)
Chair:
| 09:00 | Applying Satisfiability to the Analysis of Cryptography ( abstract ) |
10:00-10:15Coffee Break
10:30-12:00 Session 26: Structure (SAT 2015)
Chair:
| 10:30 | Using Community Structure to Detect Relevant Learnt Clauses ( abstract ) |
| 11:00 | Community Structure Inspired Algorithms for SAT and #SAT ( abstract ) |
| 11:30 | Recognition of Nested Gates in CNF Formulas ( abstract ) |
12:00-13:30Lunch Break
13:30-14:40 Session 27: Tool Presentations (SAT 2015)
Chair:
| 13:30 | SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers ( abstract ) |
| 13:40 | SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ( abstract ) |
| 13:50 | SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers ( abstract ) |
| 14:00 | PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF ( abstract ) |
| 14:10 | CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability ( abstract ) |
| 14:20 | Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances ( abstract ) |
| 14:30 | Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ( abstract ) |
14:40-15:30Tool Demonstrations and Coffee Break
15:30-17:00 Session 28: MaxSAT and Maximal Autarkies (SAT 2015)
Chair:
| 15:30 | Exploiting Resolution-based Representations for MaxSAT Solving ( abstract ) |
| 16:00 | Computing maximal autarkies with few and simple oracle queries ( abstract ) |
| 16:30 | Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP ( abstract ) |
Saturday, September 26th
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 30: Invited Talk (SAT 2015)
Chair:
| 09:00 | Random Formulas are Irrelevant, Right? ( abstract ) |
| 10:00 | Constructing SAT filters with a quantum annealer ( abstract ) |
10:30-10:45Coffee Break
10:45-12:00 Session 31: Reformulation (SAT 2015)
Chair:
| 10:45 | On Compiling CNFs into Structured Deterministic DNNFs ( abstract ) |
| 11:15 | Mining Implied Literals for Incremental SAT ( abstract ) |
| 11:45 | SAT-Based Formula Simplification ( abstract ) |
12:00-13:30Lunch Break
13:30-15:15 Session 32: Minimal Unsatisfiable Cores (SAT 2015)
Chair:
| 13:30 | A New Approach to Partial MUS Enumeration ( abstract ) |
| 14:00 | Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing ( abstract ) |
| 14:30 | Speeding up MUS Extraction with Preprocessing and Chunking ( abstract ) |
| 15:00 | SAT-Based Horn Least Upper Bounds ( abstract ) |
15:15-15:30Coffee Break
15:30-16:30 Session 33: Quantified Boolean Formulas (SAT 2015)
Chair:
| 15:30 | QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ( abstract ) |
| 16:00 | Preprocessing for DQBF ( abstract ) |
Sunday, September 27th
View this program: with abstractssession overviewtalk overview
09:00-10:15 Session 34: Tutorial by André Platzer (FMCAD15 and SAT 2015)
| 09:00 | Proving Hybrid Systems ( abstract ) |
10:15-10:30Coffee Break
10:30-11:45 Session 35: Tutorial by Priyank Kalla (FMCAD15 and 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 (FMCAD15 and SAT 2015)
| 13:45 | Reactive Synthesis ( abstract ) |
15:15-15:45Coffee Break
15:45-17:15 Session 37: Tutorial by Isil Dillig (FMCAD15 and 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 overview
10:00-10:30Coffee Break
10:30-12:00 Session 40: Invariant Generation (FMCAD15)
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
13:30-15:30 Session 41: Student Forum (FMCAD15)
Chair:
| 13:30 | The FMCAD 2015 Graduate Student Forum ( abstract ) |
15:30-16:00Coffee Break
16:00-17:30 Session 42: Use of SMT Solvers & Decision Procedures (FMCAD15)
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 overview
10:00-10:30Coffee Break
10:30-12:30 Session 45: SAT, SMT, QBF: Development (FMCAD15)
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 (FMCAD15)
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 overview
09:00-11:00 Session 48: Concurrency and Multi-Agent Protocols (FMCAD15)
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 (FMCAD15)
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 ) |
Thursday, October 1st
View this program: with abstractssession overviewtalk overview
09:10-10:30 Session 53 (ACL2-2015)
| 09:10 | Invited Talk: Lessons Learned over 45 Years in Theorem Proving ( abstract ) |
| 10:10 | A Brief Introduction to Oracle’s Use of ACL2 ( abstract ) |
11:00-12:30 Session 54 (ACL2-2015)
| 11:00 | Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning ( abstract ) |
| 11:30 | Second-Order Functions and Theorems in ACL2 ( abstract ) |
| 12:00 | R1 ( abstract ) |
13:30-14:30 Session 55: (PANEL) Industrial Use of ACL2: Present and Future (ACL2-2015)
Panelists: Jo Ebergen, Oracle
David Hardin, Rockwell Collins;
David Russinoff, Intel;
Rob Sumners, AMD;
Sol Swords, Centaur
15:00-16:15 Session 56 (ACL2-2015)
| 15:00 | Fourier Series Formalization in ACL2(r) ( abstract ) |
| 15:30 | Perfect Numbers in ACL2 ( abstract ) |
| 16:00 | R2 ( abstract ) |
16:45-18:00 Session 57 (ACL2-2015)
| 16:45 | R3 ( abstract ) |
Friday, October 2nd
View this program: with abstractssession overviewtalk overview
09:00-10:30 Session 58 (ACL2-2015)
| 09:00 | Invited Talk: Verification in the Age of Integration ( abstract ) |
| 10:00 | Extending ACL2 with SMT Solvers ( abstract ) |
11:00-12:30 Session 59 (ACL2-2015)
| 11:00 | Reasoning about LLVM code using Codewalker ( abstract ) |
| 11:30 | Stateman: Using Metafunctions to Manage Large Terms Representing Machine States ( abstract ) |
| 12:00 | Proving Skipping Refinement with ACL2s ( abstract ) |
13:30-15:00 Session 60 (ACL2-2015)
| 13:30 | R4 ( abstract ) |
| 14:00 | What's New in the Community Books ( abstract ) |
| 14:30 | What's New in ACL2 ( abstract ) |
15:30-17:00 Session 61 (ACL2-2015)
| 15:30 | R5 ( abstract ) |
| 16:00 | Business Meeting ( abstract ) |