Clarke Symposium on Model Checking 2014

Home | Schedule | Biography | Students, Post-Docs & Visitors | Ed's Website | Photos | Event Photos

Clarke Symposium 2014:
Celebrating 2⁵ Years of Model Checking

FRIDAY, 19 SEPTEMBER 2014, ASA Conference Room, 6115 Gates Hillman Center
8:00 am - 5:00 pm

8:00 - 8:45 Breakfast

8:45 - 9:00 Orna Grumberg: Opening Remarks

9:00 - 9:10 Frank Pfenning: Greetings

9:10 - 9:20 Pankaj Chauhan: Formal Verification in the Real World

9:20 - 9:30 Xiaoqing Jin: Verification and Validation Challenges in Automobiles (on behalf of Jim Kapinski)

9:30 - 9:40 Raj Rajkumar: Prof. Clarke's Impact on Automotive Systems

9:40 - 9:50 Yu-Fang Chen: Verifying Recursive Programs Using Intraprocedural Analyzers

9:50 - 10:00 Ming-Hsien Tsai (on behalf of Yih-Kuen Tsay) Verifying Curve25519 Software

10:00 - 10:10 Anvesh Komuravelli: Model Checking with Proofs and Counterexamples

10:10 - 10:20 Murali Talupur: Model Checking Distributed Protocols

10:20 - 11:00 Break

11:00 - 11:10 Daniel Kroening: Exploit-Generation with Acceleration

11:10 - 11:20 Azadeh Farzan

11:20 - 11:30 Ansgar Fehnker: The Moon and Sixpence

11:30 - 11:40 Yunshan Zhu & Yuan Lu: Assertion Synthesis

11:40 - 11:50 Rajeev Alur: Regular Functions

11:50 - 12:00 Marius Minea: Verifying Security of Web Applications and Services

12:00 - 12:10 Mike Browne: ITSPHUN demo

12:10 - 12:20 Karem Sakallah: Nobody Does It Better!

12:20 - 12:30 Xudong He: Bounded Model Checking of High Level Petri Nets

12:30 - 2:00 Lunch

2:00 - 2:10 Kenneth McMillan: Structured Decision Strategies

2:10 - 2:20 Armin Biere: SAT Based Model Checking

2:20 - 2:30 William Klieber: Solving QBF with Free Variables

2:30 - 2:40 Clark Barrett: Satisfiability Modulo Theories

2:40 - 2:50 Cesare Tinelli: SMT-Based Model Checking

2:50 - 3:00 Jeremy Avigad: The Lean Theorem Prover

3:00 - 3:40 Break

3:40 - 3:50 Natasha Sharygina: Verification of Software Upgrades

3:50 - 4:00 Somesh Jha: Some Reflections on Working with Ed Clarke

4:00 - 4:10 Natarajan Shankar: When Model Checking met Deduction

4:10 - 4:20 Sanjit A. Seshia: Integrating Induction and Deduction in Model Checking

4:20 - 4:30 Subash Shankar: A Tool for Integrating Abstract Interpretation, Model Checking, and Deductive Verification

4:30 - 4:40 Andreas Podelski: CEGAR for Black-Box System Verification

4:40 - 4:50 Aarti Gupta: Software Model Checking 4:50 - 5:00 Sagar Chaki: Model Checking Distributed Software

6:00 Dinner at local restaurants

SATURDAY, 20 SEPTEMBER 2014, ASA Conference Room, 6115 Gates Hillman Center
8:00 am - 5:00 pm

8:00 - 9:00 Breakfast

9:00 - 9:15 Helmut Veith: Opening Remarks

9:15 - 9:30 Randy Bryant: Greetings + Cloud BDDs: Mapping BDDs onto a distributed cluster

9:30 - 9:40 Gianfranco Ciardo: Unifying decision diagrams

9:40 - 9:50 Bing Liu: Parameter Identification Using Model Checking for Systems Biology

9:50 - 10:00 Jasmin Fisher: Computing Cancer

10:00 - 10:10 Michael Theobald: Formal verification of Anton, a special-purpose machine for molecular dynamics simulation

10:10 - 10:20 James R. Faeder: Model Checking Cell Decisions

10:20 - 11:00 Break

11:00 - 11:10 A. Prasad Sistla: Runtime and Static Verification of Probabilisitc Systems

11:10 - 11:20 P S Thiagarajan: Probabilistic Approximation and Verification of Hybrid Systems

11:20 - 11:30 Corina Pasareanu: On the Probabilistic Analysis of Programs

11:30 - 11:40 David Musliner & Robert P. Goldman: Probalistic Model Checking: A Decade of Uncertainty

11:40 - 11:50 Lei Bu: Online Hybrid Automata Verification of Dynamical Cyber-Physical System

11:50 - 12:00 Andre Platzer: Verified runtime validation of verified CPS models

12:00 - 12:10 Sicun Gao: Descriptive Control Theory

12:10 - 2:00 Lunch

2:00 - 2:30 Photo Session

2:30 - 2:40

Qinsi Wang: SReach: Combining SMT-based Model Checking and Statistical Tests

2:40 - 2:50 Rupak Majumdar: Language-theoretic Tools in Model Checking

2:50 - 3:00 Scott Smolka: Linear Model measurements with Application to Bird Flocking

3:00 - 3:30 Break

3:30 - 3:40 Patrice Godefroid: Dynamic Software Model Checking

3:40 - 3:50 Masahiro Fujita: Formal Analysis with Small Numbers of Test Vectors

3:50 - 4:00 David Brumley: Checking the World's Software for Exploitable Bugs

4:00 - 4:10 Rance Cleaveland: On-the-fly Model Checking

4:10 - 4:20 Karsten Wolf: Model Checking Petri Nets

4:20 - 4:30 Jin Song Dong: Event Analytics and Verification

4:30 - 4:40 Edmund M. Clarke: Concluding Remarks

6:30 - 9:30 Banquet at Wyndham Hotel